mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.instIsTriangulatedOppositeOpOp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C],
  (CategoryTheory.opOp C).IsTriangulated
-- Mathlib.Data.Set.Basic
Set.Subset.rfl : ∀ {α : Type u} {s : Set α}, s ⊆ s
-- ProofWidgets.Cancellable
/-- Cancel the request with ID `rid`.
Does nothing if `rid` is invalid.  -/
ProofWidgets.cancelRequest : ProofWidgets.RequestId → Lean.Server.RequestM (Lean.Server.RequestTask Unit)
-- Mathlib.RingTheory.OrderOfVanishing.Noetherian
Ring.ordMonoidHom_eq_ord : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsNoetherianRing R] [inst_2 : Ring.KrullDimLE 1 R]
  (x : ↥(nonZeroDivisors R)), ↑(Multiplicative.toAdd (Ring.ordMonoidHom x)) = Ring.ord R ↑x
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.mul_sup : ∀ {R : Type u_2} [inst : NonUnitalNonAssocSemiring R] {M N P : AddSubmonoid R}, M * (N ⊔ P) = M * N ⊔ M * P
-- Aesop.Index
Aesop.Index.merge : {α : Type} → Aesop.Index α → Aesop.Index α → Aesop.Index α
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_mk : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃ S)
  (h₃ : ∀ (x y : R), e.toFun (x * y) = e.toFun x * e.toFun y)
  (h₄ : ∀ (x y : R), e.toFun (x + y) = e.toFun x + e.toFun y), ⇑{ toEquiv := e, map_mul' := h₃, map_add' := h₄ } = ⇑e
-- Mathlib.Analysis.Analytic.Constructions
/-- The Cartesian product of analytic functions is analytic.  -/
AnalyticWithinAt.prod : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {e : E} {f : E → F} {g : E → G} {s : Set E},
  AnalyticWithinAt 𝕜 f s e → AnalyticWithinAt 𝕜 g s e → AnalyticWithinAt 𝕜 (fun x => (f x, g x)) s e
-- Init.Omega.Coeffs
Lean.Omega.Coeffs.dot_smul_left : ∀ (xs ys : Lean.Omega.Coeffs) (i : ℤ), Lean.Omega.Coeffs.dot (i * xs) ys = i * xs.dot ys
-- Mathlib.Analysis.Convex.Radon
/-- **Helly's theorem** for families of compact convex sets.

If `F` is a family of compact convex sets in a vector space of finite dimension `d`, and any
`k ≤ d + 1` sets of `F` intersect nontrivially, then all sets of `F` intersect nontrivially.  -/
Convex.helly_theorem_compact' : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [FiniteDimensional 𝕜 E] [inst_6 : TopologicalSpace E] [T2Space E]
  {F : ι → Set E},
  (∀ (i : ι), Convex 𝕜 (F i)) →
    (∀ (i : ι), IsCompact (F i)) →
      (∀ (I : Finset ι), I.card ≤ Module.finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → (⋂ i, F i).Nonempty
-- Mathlib.Order.Lattice.Nat
Set.biInter_lt_succ' : ∀ {α : Type u_1} (u : ℕ → Set α) (n : ℕ), ⋂ k, ⋂ (_ : k < n + 1), u k = u 0 ∩ ⋂ k, ⋂ (_ : k < n), u (k + 1)
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.fullyFaithfulForgetToPresheafedSpace_preimage_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C}
  (f :
    AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.obj X ⟶
      AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace.obj Y),
  (AlgebraicGeometry.SheafedSpace.fullyFaithfulForgetToPresheafedSpace.preimage f).hom = f
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1S_sub : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F},
  (∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) →
    MeasureTheory.FinMeasAdditive μ T →
      ∀ (f g : ↥(α →₁ₛ[μ] E)),
        MeasureTheory.L1.SimpleFunc.setToL1S T (f - g) =
          MeasureTheory.L1.SimpleFunc.setToL1S T f - MeasureTheory.L1.SimpleFunc.setToL1S T g
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.instIsZeroApplyMeasure : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β},
  IsZeroApply (ProbabilityTheory.Kernel α β) α (MeasureTheory.Measure β)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_intCast : ∀ (x : ℝ) (n : ℤ), x ^ ↑n = x ^ n
-- Std.Http.Data.Body.Stream
Std.Http.Body.instStream : Std.Http.Body Std.Http.Body.Stream
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBiproductData.ofIso_bicone : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q P' Q' : C} (d : CategoryTheory.Limits.BinaryBiproductData P Q) (eP : P ≅ P') (eQ : Q ≅ Q'),
  (d.ofIso eP eQ).bicone = d.bicone.ofIso eP eQ
-- Init.Data.UInt.Bitwise
UInt16.ofBitVec_and : ∀ (a b : BitVec 16), { toBitVec := a &&& b } = { toBitVec := a } &&& { toBitVec := b }
-- Mathlib.Algebra.CubicDiscriminant
Cubic.leadingCoeff_of_a_ne_zero' : ∀ {R : Type u_1} {a b c d : R} [inst : Semiring R], a ≠ 0 → { a := a, b := b, c := c, d := d }.toPoly.leadingCoeff = a
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
QuadraticMap.Isometry.instFunLike : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      {N : Type u_7} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R N] →
                      {Q₁ : QuadraticMap R M₁ N} → {Q₂ : QuadraticMap R M₂ N} → FunLike (Q₁ →qᵢ Q₂) M₁ M₂
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : ℝ≥0 → ℝ≥0` is continuous on a compact set `s` and `f 0 = 0` and `a : X → A` is
continuous at `x₀` within a set `t : Set X`, and eventually `0 ≤ a x` and has quasispectrum
contained in `s`, then `fun x ↦ cfcₙ f (a x)` is continuous at `x₀` within `t`.  -/
ContinuousWithinAt.cfcₙ_nnreal : ∀ {X : Type u_1} {A : Type u_2} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [ContinuousStar A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  [inst_12 : TopologicalSpace X] {s : Set NNReal},
  IsCompact s →
    ∀ (f : NNReal → NNReal) {a : X → A} {x₀ : X} {t : Set X},
      x₀ ∈ t →
        ContinuousWithinAt a t x₀ →
          (∀ᶠ (x : X) in nhdsWithin x₀ t, quasispectrum NNReal (a x) ⊆ s) →
            (∀ᶠ (x : X) in nhdsWithin x₀ t, 0 ≤ a x) →
              autoParam (ContinuousOn f s) ContinuousWithinAt.cfcₙ_nnreal._auto_1 →
                autoParam (f 0 = 0) ContinuousWithinAt.cfcₙ_nnreal._auto_3 →
                  ContinuousWithinAt (fun x => cfcₙ f (a x)) t x₀
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_eq_some_iff_exists_beq_and_mem_toArray : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {v : β},
  m.WF →
    (Std.DHashMap.Raw.Const.get? m k = some v ↔ ∃ k', (k == k') = true ∧ (k', v) ∈ Std.DHashMap.Raw.Const.toArray m)
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosSemidef.conjTranspose : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] {M : Matrix n n R},
  M.PosSemidef → M.conjTranspose.PosSemidef
-- Init.Data.Char.Lemmas
Char.toNat_inj : ∀ {c d : Char}, c.toNat = d.toNat ↔ c = d
-- Mathlib.Order.RelIso.Basic
/-- **Alias** of `RelEmbedding.stdRefl`. -/
RelEmbedding.isRefl : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [Std.Refl s], Std.Refl r
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
/-- For a topological vector space `E`, "identity mapping" `E → WeakSpace 𝕜 E` is continuous.
This definition implements it as a continuous linear map.  -/
toWeakSpaceCLM : (𝕜 : Type u_2) →
  (E : Type u_4) →
    [inst : CommSemiring 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [inst_2 : ContinuousAdd 𝕜] →
          [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
            [inst_4 : AddCommMonoid E] → [inst_5 : Module 𝕜 E] → [inst_6 : TopologicalSpace E] → E →L[𝕜] WeakSpace 𝕜 E
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.ofIso_neg : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G' X : C} [inst_2 : CategoryTheory.AddGrpObj G'] (e : G' ≅ X),
  CategoryTheory.AddGrpObj.neg =
    CategoryTheory.CategoryStruct.comp e.inv (CategoryTheory.CategoryStruct.comp CategoryTheory.AddGrpObj.neg e.hom)
-- Init.Data.SInt.Basic
instOrOpISize : OrOp ISize
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.instAdd : {𝕜 : Type u_2} → {α : Type u_5} → [inst : AddZeroClass 𝕜] → [inst_1 : LE α] → Add (IncidenceAlgebra 𝕜 α)
-- Lean.Elab.DocString
/-- Elaborates the syntax of an block-level document element to an actual block-level document element.
 -/
Lean.Doc.elabBlock : Lean.TSyntax `block → Lean.Doc.DocM (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock)
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded, nonarchimedean function, then
`seminormFromBounded' f` is nonarchimedean.  -/
seminormFromBounded_isNonarchimedean : ∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ} {c : ℝ},
  0 ≤ f → (∀ (x y : R), f (x * y) ≤ c * f x * f y) → IsNonarchimedean f → IsNonarchimedean (seminormFromBounded' f)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.induce_empty : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph}, G'.induce ∅ = ⊥
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castAdd_Icc_castAdd : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.castAdd m ⁻¹' Set.Icc (Fin.castAdd m i) (Fin.castAdd m j) = Set.Icc i j
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
AlgebraicGeometry.Scheme.isClosedUnderIsomorphisms_quasiCompactCover : ∀ (S : AlgebraicGeometry.Scheme), S.quasiCompactCover.IsClosedUnderIsomorphisms
-- Lean.Environment
/-- `Task AsyncConsts` except for problematic recursion. The set of nested constants created while
elaborating this constant.
 -/
_private.Lean.Environment.0.Lean.AsyncConst.aconstsImpl : Lean.AsyncConst✝ → Task Dynamic
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
/-- The converse of the construction in `liftToFinsetLimitCone`: we can form a cone on the
product of `f` whose legs are the products over the finite subsets of `α`.  -/
CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type w} →
      [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
        (f : α → C) →
          [CategoryTheory.Limits.HasProduct f] →
            CategoryTheory.Limits.Cone
              (CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj (CategoryTheory.Discrete.functor f))
-- Lean.Data.PrefixTree
Lean.PrefixTreeNode.WellFormed.brecOn : ∀ {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2}
  {motive : (a : Lean.PrefixTreeNode α β cmp) → Lean.PrefixTreeNode.WellFormed cmp a → Prop}
  {a : Lean.PrefixTreeNode α β cmp} (t : Lean.PrefixTreeNode.WellFormed cmp a),
  (∀ (a : Lean.PrefixTreeNode α β cmp) (t : Lean.PrefixTreeNode.WellFormed cmp a),
      Lean.PrefixTreeNode.WellFormed.below t → motive a t) →
    motive a t
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.epsilon_lt_of_pos : ∀ {r : ℝ}, 0 < r → Hyperreal.epsilon < ↑r
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iInter_mul_subset : ∀ {α : Type u_2} {ι : Sort u_5} [inst : Mul α] (s : ι → Set α) (t : Set α), (⋂ i, s i) * t ⊆ ⋂ i, s i * t
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.hasDerivWithinAt_arccos_Ici : ∀ {x : ℝ}, x ≠ -1 → HasDerivWithinAt Real.arccos (-(1 / √(1 - x ^ 2))) (Set.Ici x) x
-- Mathlib.RingTheory.Finiteness.Defs
RingHom.finite_algebraMap : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
  (algebraMap A B).Finite ↔ Module.Finite A B
-- Init.Prelude
/-- An overloaded operation to find the lesser of two values of type `α`.
 -/
Min : Type u → Type u
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.lift_mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Sort u_1} {X : C}
  (F : ⦃A : C⦄ → (f : A ⟶ X) → [CategoryTheory.Mono f] → α)
  {h :
    ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst_1 : CategoryTheory.Mono f] [inst_2 : CategoryTheory.Mono g] (i : A ≅ B),
      CategoryTheory.CategoryStruct.comp i.hom g = f → F f = F g}
  {A : C} (f : A ⟶ X) [inst_1 : CategoryTheory.Mono f],
  CategoryTheory.Subobject.lift F h (CategoryTheory.Subobject.mk f) = F f
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.ExistsHomHomCompEqCompAux.i'.congr_simp : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] {S X : AlgebraicGeometry.Scheme}
  {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S}
  [inst_1 : ∀ (i : I), CompactSpace ↥(D.obj i)] [inst_2 : CategoryTheory.IsCofiltered I]
  [inst_3 : ∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)]
  (A A_1 : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f), A = A_1 → A.i' = A_1.i'
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.coe_mul : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) (x y : K),
  { toCompletion := ↑(WithAbs.toAbs (↑v) (x * y)) } =
    { toCompletion := ↑(WithAbs.toAbs (↑v) x) } * { toCompletion := ↑(WithAbs.toAbs (↑v) y) }
-- Mathlib.GroupTheory.Divisible
DivisibleBy.div_cancel : ∀ {A : Type u_1} {α : Type u_2} {inst : AddMonoid A} {inst_1 : SMul α A} {inst_2 : Zero α} [self : DivisibleBy A α]
  {n : α} (a : A), n ≠ 0 → n • DivisibleBy.div a n = a
-- Mathlib.GroupTheory.QuotientGroup.Defs
/-- Two `MonoidHom`s from a quotient group are equal if their compositions with
`QuotientGroup.mk'` are equal.

See note [partially-applied ext lemmas].  -/
QuotientGroup.monoidHom_ext : ∀ {G : Type u_1} {M : Type u_4} [inst : Group G] [inst_1 : Monoid M] (N : Subgroup G) [nN : N.Normal]
  ⦃f g : G ⧸ N →* M⦄, f.comp (QuotientGroup.mk' N) = g.comp (QuotientGroup.mk' N) → f = g
-- Init.Data.Int.DivMod.Lemmas
Int.mul_tdiv_cancel : ∀ (a : ℤ) {b : ℤ}, b ≠ 0 → (a * b).tdiv b = a
-- Mathlib.Algebra.Order.Module.Defs
/-- Do not use this. Use `smul_le_smul_of_nonneg_right` instead.  -/
SMulPosMono.smul_le_smul_of_nonneg_right : ∀ {α : Type u_1} {β : Type u_2} {inst : SMul α β} {inst_1 : Preorder α} {inst_2 : Preorder β} {inst_3 : Zero β}
  [self : SMulPosMono α β] ⦃b : β⦄, 0 ≤ b → ∀ ⦃a₁ a₂ : α⦄, a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
-- Mathlib.Topology.Covering.Basic
IsEvenlyCovered.restrictPreimage : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} (s : Set X)
  {I : Type u_3} [inst_2 : TopologicalSpace I] {x : X} (hxs : x ∈ s),
  IsEvenlyCovered f x I → IsEvenlyCovered (s.restrictPreimage f) ⟨x, hxs⟩ I
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A seminormed ring is a ring endowed with a seminorm which satisfies the inequality
`‖x y‖ ≤ ‖x‖ ‖y‖`.  -/
SeminormedRing : Type u_5 → Type u_5
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpTo.differentiable : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F}, HasFTaylorSeriesUpTo n f p → n ≠ 0 → Differentiable 𝕜 f
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Functor.prod'_map : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A B)
  (G : CategoryTheory.Functor A C) {X Y : A} (f : X ⟶ Y),
  (F.prod' G).map f = CategoryTheory.Prod.mkHom (F.map f) (G.map f)
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.sfiniteSeq.congr_simp : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ μ_1 : MeasureTheory.Measure α) (e_μ : μ = μ_1)
  [h : MeasureTheory.SFinite μ] (a a_1 : ℕ), a = a_1 → MeasureTheory.sfiniteSeq μ a = MeasureTheory.sfiniteSeq μ_1 a_1
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.mem_range_omega_iff : ∀ {x : Ordinal.{u_1}}, x ∈ Set.range ⇑Ordinal.omega ↔ Ordinal.omega0 ≤ x ∧ x.IsInitial
-- Mathlib.RingTheory.Ideal.Cotangent
/-- The quotient map from `I` to `I ⧸ I ^ 2`.  -/
Ideal.toCotangent : {R : Type u} → [inst : CommRing R] → (I : Ideal R) → ↥I →ₗ[R] I.Cotangent
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.mk : (toProfinite : Profinite) →
  [addGroup : AddGroup ↑toProfinite.toTop] →
    [topologicalAddGroup : IsTopologicalAddGroup ↑toProfinite.toTop] → ProfiniteAddGrp.{u}
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsCondKernelCDF.tendsto_atTop_one : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → StieltjesFunction ℝ}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β},
  ProbabilityTheory.IsCondKernelCDF f κ ν → ∀ (p : α × β), Filter.Tendsto (↑(f p)) Filter.atTop (nhds 1)
-- Mathlib.NumberTheory.Wilson
/-- **Wilson's Lemma**: the product of `1`, ..., `p-1` is `-1` modulo `p`.  -/
ZMod.wilsons_lemma : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ↑(p - 1).factorial = -1
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1_mono_left : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {G'' : Type u_8} [inst_2 : NormedAddCommGroup G''] [inst_3 : PartialOrder G'']
  [IsOrderedAddMonoid G''] [inst_5 : NormedSpace ℝ G''] [inst_6 : CompleteSpace G''] [OrderClosedTopology G'']
  {T T' : Set α → E →L[ℝ] G''} {C C' : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'),
  (∀ (s : Set α) (x : E), (T s) x ≤ (T' s) x) →
    ∀ (f : ↥(MeasureTheory.Lp E 1 μ)), (MeasureTheory.L1.setToL1 hT) f ≤ (MeasureTheory.L1.setToL1 hT') f
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Presentation.toRelations : {A : Type u} →
  [inst : Ring A] →
    {M : Type v} → [inst_1 : AddCommGroup M] → [inst_2 : Module A M] → Module.Presentation A M → Module.Relations A
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_keysArray : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {k : α}, m.WF → m.keysArray.contains k = m.contains k
-- Mathlib.Algebra.Ring.Fin
RingEquiv.piFinTwo_apply : ∀ (R : Fin 2 → Type u_1) [inst : (i : Fin 2) → Semiring (R i)] (a : (i : Fin 2) → R i),
  (RingEquiv.piFinTwo R) a = (piFinTwoEquiv R) a
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.down_uliftEquiv_symm_tmul : ∀ (R : Type u_4) (S : Type u_5) {A : Type u_6} {B : Type u_7} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] (a : ULift.{u_8, u_6} A)
  (b : ULift.{u_9, u_7} B),
  ((Algebra.TensorProduct.uliftEquiv R S A B).symm (a ⊗ₜ[ULift.{u_11, u_4} R] b)).down = a.down ⊗ₜ[R] b.down
-- Mathlib.Data.List.Basic
List.idxOf_eq_length_iff : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α}, List.idxOf a l = l.length ↔ a ∉ l
-- Mathlib.Data.BitVec
BitVec.equivFin_apply : ∀ {m : ℕ} (a : BitVec m), BitVec.equivFin a = a.toFin
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
isSemisimpleRing_mulOpposite_iff : ∀ {R : Type u} [inst : Ring R], IsSemisimpleRing Rᵐᵒᵖ ↔ IsSemisimpleRing R
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.coe_mk_finite_iff : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps : DiscreteTiling.Protoset G X ιₚ} {i : ιₚ}
  (g : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i)).subtype (↑ps i).symmetries),
  (↑{ index := i, groupElts := g }).Finite ↔ (↑(↑ps i)).Finite
-- Mathlib.LinearAlgebra.FixedSubmodule
LinearEquiv.fixedSubmodule_eq_top_iff : ∀ {R : Type u_1} [inst : Semiring R] {V : Type u_3} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] {f : V ≃ₗ[R] V},
  (↑f).fixedSubmodule = ⊤ ↔ f = LinearEquiv.refl R V
-- Mathlib.Data.Set.Basic
Set.nonempty_of_not_subset : ∀ {α : Type u} {s t : Set α}, ¬s ⊆ t → (s \ t).Nonempty
-- Mathlib.Tactic.ClickSuggestions.ApplyAt
Mathlib.Tactic.ClickSuggestions.instOrdApplyAtKey : Ord Mathlib.Tactic.ClickSuggestions.ApplyAtKey
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.mem_valueMonoid : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : MonoidWithZero B] (f : A →*₀ B) {b : Bˣ},
  ↑b ∈ Set.range ⇑f → b ∈ f.valueMonoid
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map₂_obj_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B}
  {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V)
  (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)),
  ((CategoryTheory.CostructuredArrow.map₂ α β).obj X).left = F.obj X.left
-- Lean.Environment
/-- Mapping from constant name to `ConstantInfo`. It contains all constants (definitions, theorems,
axioms, etc) that have been already type checked by the kernel.
 -/
Lean.Kernel.Environment.constants : Lean.Kernel.Environment → Lean.ConstMap
-- Mathlib.Analysis.Convex.Jensen
/-- If a function `f` is concave on `s`, then the value it takes at some center of mass of points of
`s` is greater than the value it takes on one of those points.  -/
ConcaveOn.exists_le_of_centerMass : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : LinearOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {w : ι → 𝕜} {p : ι → E} {t : Finset ι},
  ConcaveOn 𝕜 s f → (∀ i ∈ t, 0 ≤ w i) → 0 < ∑ i ∈ t, w i → (∀ i ∈ t, p i ∈ s) → ∃ i ∈ t, f (p i) ≤ f (t.centerMass w p)
-- Init.Data.List.Lemmas
List.all_insert : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {f : α → Bool} {l : List α} {a : α},
  (List.insert a l).all f = (f a && l.all f)
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.GrindM.run : {α : Type} →
  Lean.Meta.Grind.GrindM α → Lean.Meta.Grind.Params → optParam (Option Lean.Meta.Grind.EvalTactic) none → Lean.MetaM α
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
le_iff_forall_pos_lt_add' : ∀ {α : Type u} [inst : LinearOrder α] [DenselyOrdered α] [inst_2 : AddMonoid α] [ExistsAddOfLE α] [AddLeftReflectLT α]
  {a b : α} [AddLeftStrictMono α], a ≤ b ↔ ∀ (ε : α), 0 < ε → a < b + ε
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_sub : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {x y : K},
  0 ≤ ArchimedeanClass.mk x →
    0 ≤ ArchimedeanClass.mk y →
      ArchimedeanClass.stdPart (x - y) = ArchimedeanClass.stdPart x - ArchimedeanClass.stdPart y