mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Control.StateCps
/-- Executes an action from a monad with added state in the underlying monad `m`. Given an initial
state, it returns a value paired with the final state.

While the state is internally represented in continuation passing style, the resulting value is the
same as for a non-CPS state monad.
 -/
StateCpsT.run : {α σ : Type u} → {m : Type u → Type v} → [Monad m] → StateCpsT σ m α → σ → m (α × σ)
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_pow : ∀ {R : Type u} [inst : CommSemiring R] (p : Polynomial R) (n : ℕ),
  Polynomial.derivative (p ^ n) = Polynomial.C ↑n * p ^ (n - 1) * Polynomial.derivative p
-- Mathlib.Analysis.Normed.Module.RCLike.Extend
/-- **Alias** of `StrongDual.norm_extendRCLike`. -/
ContinuousLinearMap.norm_extendTo𝕜' : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : IsScalarTower ℝ 𝕜 F] (fr : StrongDual ℝ F), ‖fr.extendRCLike‖ = ‖fr‖
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.smul_mem_iff'' : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M)
  {r : R} {x : M} [Invertible r], r • x ∈ p ↔ x ∈ p
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.coe_ringHom_id : ∀ {α : Type u_2} [inst : NonAssocSemiring α] [inst_1 : Preorder α], ↑(OrderRingHom.id α) = RingHom.id α
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Right.pow_lt_one_of_lt : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulRightMono M] {n : ℕ} {x : M}, 0 < n → x < 1 → x ^ n < 1
-- Mathlib.Order.Interval.Set.ProjIcc
Set.IccExtend.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a b : α} (h : a ≤ b) (f f_1 : ↑(Set.Icc a b) → β),
  f = f_1 → ∀ (a_1 a_2 : α), a_1 = a_2 → Set.IccExtend h f a_1 = Set.IccExtend h f_1 a_2
-- Mathlib.Algebra.Group.Prod
/-- The equivalence between `M × N` and `N × M` given by swapping the components
is multiplicative.  -/
MulEquiv.prodComm : {M : Type u_3} → {N : Type u_4} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → M × N ≃* N × M
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- **Alias** of the reverse direction of `affineSpan_nonempty`.

---

The affine span of a set is nonempty if and only if that set is.  -/
Set.Nonempty.affineSpan : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P}, s.Nonempty → (↑(affineSpan k s)).Nonempty
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_comap_eq : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid N),
  AddSubmonoid.map f (AddSubmonoid.comap f S) = S ⊓ AddMonoidHom.mrange f
-- Init.Data.Order.Lemmas
Std.asymm_of_irrefl_of_antisymm : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Irrefl r] [Std.Antisymm r], Std.Asymm r
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.Quotient.mk_cast : ∀ {X : Type u} [inst : TopologicalSpace X] {x y : X} (P : Path x y) {x' y' : X} (hx : x' = x) (hy : y' = y),
  Path.Homotopic.Quotient.mk (P.cast hx hy) = (Path.Homotopic.Quotient.mk P).cast hx hy
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.mk_apply : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (hμ : MeasureTheory.IsProbabilityMeasure μ)
  (s : Set Ω), ⟨μ, hμ⟩ s = (μ s).toNNReal
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
integral_gaussian_Ioi : ∀ (b : ℝ), ∫ (x : ℝ) in Set.Ioi 0, Real.exp (-b * x ^ 2) = √(Real.pi / b) / 2
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.instSmallHomOfLocallySmall : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] (X Y : C),
  Small.{w, v} (X ⟶ Y)
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_upperBounds_range : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [Nonempty β] {f : β → α},
  BddAbove (Set.range f) → sInf (upperBounds (Set.range f)) = ⨆ i, f i
-- Lean.Meta.Hint
/-- Diff using whitespace-separated tokens.  -/
Lean.Meta.Hint.DiffGranularity.word : Lean.Meta.Hint.DiffGranularity
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Real.cosh_le_exp_half_sq : ∀ (x : ℝ), Real.cosh x ≤ Real.exp (x ^ 2 / 2)
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- The limit of `n * log (1 + g n)` as `(n : ℝ) → ∞` is `t`,
where `t : ℂ` is the limit of `n * g n`.  -/
Complex.tendsto_nat_mul_log_one_add_of_tendsto : ∀ {g : ℕ → ℂ} {t : ℂ},
  Filter.Tendsto (fun n => ↑n * g n) Filter.atTop (nhds t) →
    Filter.Tendsto (fun n => ↑n * Complex.log (1 + g n)) Filter.atTop (nhds t)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
SpectrumRestricts.starAlgHom_apply : ∀ {R : Type u} {S : Type v} {A : Type w} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Semifield S] [inst_6 : StarRing S]
  [inst_7 : TopologicalSpace S] [inst_8 : IsTopologicalSemiring S] [inst_9 : ContinuousStar S] [inst_10 : Ring A]
  [inst_11 : StarRing A] [inst_12 : Algebra R S] [inst_13 : Algebra R A] [inst_14 : Algebra S A]
  [inst_15 : IsScalarTower R S A] [inst_16 : StarModule R S] [inst_17 : ContinuousSMul R S] {a : A}
  (φ : C(↑(spectrum S a), S) →⋆ₐ[S] A) {f : C(S, R)} (h : SpectrumRestricts a ⇑f) (x : C(↑(spectrum R a), R)),
  (SpectrumRestricts.starAlgHom φ h) x =
    φ
      ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp
        (x.comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ }))
-- Mathlib.Probability.Kernel.Condexp
ProbabilityTheory.condExp_generateFrom_singleton : ∀ {Ω : Type u_1} {F : Type u_2} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ]
  {s : Set Ω} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] [CompleteSpace F],
  MeasurableSet s →
    ∀ {f : Ω → F},
      MeasureTheory.Integrable f μ →
        μ[f | MeasurableSpace.generateFrom {s}] =ᵐ[μ.restrict s] fun x => ∫ (x : Ω), f x ∂μ[|s]
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- If `f₁` and `f₂` have unequal order at `x`, then the trailing coefficient of `f₁ + f₂` at `x` is the
trailing coefficient of the function with the lowest order.
 -/
MeromorphicAt.meromorphicTrailingCoeffAt_add_eq_left_of_lt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f₁ f₂ : 𝕜 → E},
  MeromorphicAt f₂ x →
    meromorphicOrderAt f₁ x < meromorphicOrderAt f₂ x →
      meromorphicTrailingCoeffAt (f₁ + f₂) x = meromorphicTrailingCoeffAt f₁ x
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.Int.toNat.match_1.eq_1 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (a : ℕ) → motive (Int.negSucc a)),
  (match Int.ofNat n with
    | Int.ofNat n => h_1 n
    | Int.negSucc a => h_2 a) =
    h_1 n
-- Mathlib.Algebra.Group.Equiv.TypeTags
MulEquiv.AddMonoid.End_apply : ∀ {M : Type u_4} [inst : AddMonoid M] (f : M →+ M),
  MulEquiv.AddMonoid.End f =
    { toFun := fun a => Multiplicative.ofAdd (f (Multiplicative.toAdd a)), map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Module.CharacterModule
/-- The character module of an abelian group `A` in the unit rational circle is `A⋆ := Hom_ℤ(A, ℚ ⧸ ℤ)`.
 -/
CharacterModule : (A : Type uA) → [AddCommGroup A] → Type uA
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
zmodMulEquivOfGenerator_apply_ofAdd_intCast : ∀ {G : Type u_2} [inst : Group G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {n : ℕ} (hn : Nat.card G = n)
  (i : ℤ), (zmodMulEquivOfGenerator hg hn) (Multiplicative.ofAdd ↑i) = g ^ i
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.int_even_mul_periodic : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : NonAssocRing α] [inst_1 : InvolutiveNeg β],
  Function.Antiperiodic f c → ∀ (n : ℤ), Function.Periodic f (↑n * (2 * c))
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α} {fallback : β},
  (List.map Prod.fst l).contains k = false → (t.insertMany l).getD k fallback = t.getD k fallback
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey_insert_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β k}, (m.insert k v).getKey k ⋯ = k
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.mk0.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDedekindDomain R],
  ClassGroup.mk0 = (ClassGroup.mk (FractionRing R)).comp (FractionalIdeal.mk0 (FractionRing R))
-- Init.Data.Array.Count
Array.countP_filter : ∀ {α : Type u_1} {p q : α → Bool} {xs : Array α},
  Array.countP p (Array.filter q xs) = Array.countP (fun a => p a && q a) xs
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.hom_ext_iff : ∀ {X Y : GrpCat} {f g : X ⟶ Y}, f = g ↔ GrpCat.Hom.hom f = GrpCat.Hom.hom g
-- Mathlib.Data.List.Basic
List.Disjoint.map_iff : ∀ {α : Type u} {β : Type v} {f : α → β} {s t : List α},
  Function.Injective f → ((List.map f s).Disjoint (List.map f t) ↔ s.Disjoint t)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
mem_zpowers_of_prime_card : ∀ {G : Type u_2} [inst : Group G] {p : ℕ} [hp : Fact (Nat.Prime p)],
  Nat.card G = p → ∀ {g g' : G}, g ≠ 1 → g' ∈ Subgroup.zpowers g
-- Aesop.Tree.Data
Aesop.Goal.forwardState : Aesop.Goal → Aesop.ForwardState
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.germ_stalkIso_hom_assoc : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) {V : (↑U).Opens} (x : ↥U) (hx : x ∈ V) {Z : CommRingCat}
  (h : X.presheaf.stalk ↑x ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((↑U).presheaf.germ V x hx)
      (CategoryTheory.CategoryStruct.comp (U.stalkIso x).hom h) =
    CategoryTheory.CategoryStruct.comp (X.presheaf.germ ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V) ↑x ⋯) h
-- Aesop.Tracing
Aesop.TraceOption.option : Aesop.TraceOption → Lean.Option Bool
-- Mathlib.Topology.Compactness.LocallyCompact
local_compact_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyCompactSpace X] {x : X} {n : Set X},
  n ∈ nhds x → ∃ s ∈ nhds x, s ⊆ n ∧ IsCompact s
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.mk.injEq : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (boxes : Finset (BoxIntegral.Box ι)) (le_of_mem' : ∀ J ∈ boxes, J ≤ I)
  (pairwiseDisjoint : (↑boxes).Pairwise (Function.onFun Disjoint BoxIntegral.Box.toSet))
  (boxes_1 : Finset (BoxIntegral.Box ι)) (le_of_mem'_1 : ∀ J ∈ boxes_1, J ≤ I)
  (pairwiseDisjoint_1 : (↑boxes_1).Pairwise (Function.onFun Disjoint BoxIntegral.Box.toSet)),
  ({ boxes := boxes, le_of_mem' := le_of_mem', pairwiseDisjoint := pairwiseDisjoint } =
      { boxes := boxes_1, le_of_mem' := le_of_mem'_1, pairwiseDisjoint := pairwiseDisjoint_1 }) =
    (boxes = boxes_1)
-- Mathlib.Algebra.Group.Hom.Defs
/-- The identity map from a type with 1 to itself.  -/
OneHom.id : (M : Type u_10) → [inst : One M] → OneHom M M
-- Mathlib.Data.List.OfFn
List.ofFn_getElem_eq_map : ∀ {α : Type u} {β : Type u_1} (l : List α) (f : α → β), (List.ofFn fun i => f l[↑i]) = List.map f l
-- Mathlib.RingTheory.LocalProperties.Reduced
/-- `M⁻¹R` is reduced if `R` is reduced.  -/
isReduced_localizationPreserves : LocalizationPreserves fun R x => IsReduced R
-- Lean.LocalContext
Lean.LocalDeclKind.auxDecl.sizeOf_spec : sizeOf Lean.LocalDeclKind.auxDecl = 1
-- Mathlib.LinearAlgebra.Matrix.IsDiag
Matrix.IsDiag.add : ∀ {α : Type u_1} {n : Type u_4} [inst : AddZeroClass α] {A B : Matrix n n α}, A.IsDiag → B.IsDiag → (A + B).IsDiag
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.instCategory : {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] →
        {A : Type u_5} →
          [inst_2 : AddMonoid A] →
            [inst_3 : CategoryTheory.HasShift D A] →
              CategoryTheory.Category.{max (max u_1 u_5) v_2, max (max (max (max u_5 u_2) v_2) u_1) v_1}
                (CategoryTheory.SingleFunctors C D A)
-- Std.Time.DateTime.Timestamp
/-- Adds a `Duration` to the given `Timestamp`.
 -/
Std.Time.Timestamp.addDuration : Std.Time.Timestamp → Std.Time.Duration → Std.Time.Timestamp
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities.signatureHelpProvider? : Lean.Lsp.ServerCapabilities → Option Lean.Lsp.SignatureHelpOptions
-- Mathlib.RingTheory.OrderOfVanishing.Noetherian
/-- Order of vanishing function as a monoid homomorphism
 -/
Ring.ordMonoidHom : {R : Type u_2} →
  [inst : CommRing R] → [IsNoetherianRing R] → [Ring.KrullDimLE 1 R] → ↥(nonZeroDivisors R) →* Multiplicative ℕ
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.NullMeasurableSet.subtype_coe : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set ↑s},
  MeasureTheory.NullMeasurableSet s μ →
    MeasureTheory.NullMeasurableSet t (MeasureTheory.Measure.comap Subtype.val μ) →
      MeasureTheory.NullMeasurableSet (Subtype.val '' t) μ
-- Mathlib.Topology.Algebra.OpenSubgroup
/-- The type of open normal subgroups of a topological group.  -/
OpenNormalSubgroup : (G : Type u) → [Group G] → [TopologicalSpace G] → Type u
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.piUnique.eq_1 : ∀ {ι : Type u_16} (M : ι → Type u_17) [inst : (j : ι) → Add (M j)] [inst_1 : Unique ι],
  AddEquiv.piUnique M = { toEquiv := Equiv.piUnique M, map_add' := ⋯ }
-- Lean.Widget.Basic
Lean.Widget.instTypeNameInfoWithCtx : TypeName Lean.Elab.InfoWithCtx
-- Mathlib.Order.Filter.Pointwise
Filter.mulOneClass.eq_1 : ∀ {α : Type u_2} [inst : MulOneClass α],
  Filter.mulOneClass = { toOne := Filter.instOne, toMul := Filter.instMul, one_mul := ⋯, mul_one := ⋯ }
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- A family of elements for the arrow set `R` is *compatible* if for any `f₁ : Y₁ ⟶ X` and
`f₂ : Y₂ ⟶ X` in `R`, and any `g₁ : Z ⟶ Y₁` and `g₂ : Z ⟶ Y₂`, if the square `g₁ ≫ f₁ = g₂ ≫ f₂`
commutes then the elements of `P Z` obtained by restricting the element of `P Y₁` along `g₁` and
restricting the element of `P Y₂` along `g₂` are the same.

In special cases, this condition can be simplified, see `pullbackCompatible_iff` and
`compatible_iff_sieveCompatible`.

This is referred to as a "compatible family" in Definition C2.1.2 of [Elephant], and on nlab:
https://ncatlab.org/nlab/show/sheaf#GeneralDefinitionInComponents

For a more explicit version in the case where `R` is of the form `Presieve.ofArrows`, see
`CategoryTheory.Presieve.Arrows.Compatible`.
 -/
CategoryTheory.Presieve.FamilyOfElements.Compatible : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      {X : C} → {R : CategoryTheory.Presieve X} → CategoryTheory.Presieve.FamilyOfElements P R → Prop
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.GeneratorNode.mk.injEq : ∀ (mvar key : Lean.Expr) (mctx : Lean.MetavarContext) (instances : Array Lean.Meta.SynthInstance.Instance)
  (currInstanceIdx : ℕ) (typeHasMVars : Bool) (mvar_1 key_1 : Lean.Expr) (mctx_1 : Lean.MetavarContext)
  (instances_1 : Array Lean.Meta.SynthInstance.Instance) (currInstanceIdx_1 : ℕ) (typeHasMVars_1 : Bool),
  ({ mvar := mvar, key := key, mctx := mctx, instances := instances, currInstanceIdx := currInstanceIdx,
        typeHasMVars := typeHasMVars } =
      { mvar := mvar_1, key := key_1, mctx := mctx_1, instances := instances_1, currInstanceIdx := currInstanceIdx_1,
        typeHasMVars := typeHasMVars_1 }) =
    (mvar = mvar_1 ∧
      key = key_1 ∧
        mctx = mctx_1 ∧ instances = instances_1 ∧ currInstanceIdx = currInstanceIdx_1 ∧ typeHasMVars = typeHasMVars_1)
-- Mathlib.Data.Multiset.Fintype
/-- **Alias** of `Multiset.mapEquivAux`.

---

There is some equivalence between `m` and `m.map f` which respects `f`.
 -/
Multiset.mapEquiv_aux : {α : Type u_1} →
  {β : Type u_2} →
    [inst : DecidableEq α] →
      [inst_1 : DecidableEq β] → (m : Multiset α) → (f : α → β) → Squash { v // ∀ (a : m.ToType), (v a).fst = f a.fst }
-- Mathlib.Analysis.Convex.Deriv
ConvexOn.monotoneOn_slope_gt : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} {x : 𝕜},
  ConvexOn 𝕜 s f → x ∈ s → MonotoneOn (slope f x) {y | y ∈ s ∧ x < y}
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.filterMapM_cons.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Algebra.Group.Action.Basic
MulAction.toFun_apply : ∀ {M : Type u_2} {α : Type u_5} [inst : Monoid M] [inst_1 : MulAction M α] (x : M) (y : α),
  (MulAction.toFun M α) y x = x • y
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.Integrable.restrict : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {f : X → E} {μ : MeasureTheory.VectorMeasure X F},
  μ.Integrable f → ∀ {s : Set X}, (μ.restrict s).Integrable f
-- Mathlib.GroupTheory.Torsion
IsMulTorsion.group.eq_1 : ∀ {G : Type u_1} [inst : Monoid G] (tG : IsMulTorsion G),
  tG.group =
    { toMonoid := inst, inv := fun g => g ^ (orderOf g - 1), div := DivInvMonoid.div', zpow := zpowRec,
      div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯ }
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddCancelCommMonoid : {α : Type u_1} → [AddCancelCommMonoid α] → AddCancelCommMonoid (Lex α)
-- Init.Control.Lawful.Basic
/-- An applicative functor satisfies the laws of an applicative functor.

The `Applicative` class contains the operations of an applicative functor, but does not require that
instances prove they satisfy the laws of an applicative functor. A `LawfulApplicative` instance
includes proofs that the laws are satisfied.

Because `Applicative` instances may provide optimized implementations of `seqLeft` and `seqRight`,
`LawfulApplicative` instances must also prove that the optimized implementation is equivalent to the
standard implementation.
 -/
LawfulApplicative : (f : Type u → Type v) → [Applicative f] → Prop
-- Init.Data.String.Defs
String.utf8ByteSize_eq_zero_iff : ∀ {s : String}, s.utf8ByteSize = 0 ↔ s = ""
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.equiv_iff_toList_perm : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp},
  t₁.Equiv t₂ ↔ t₁.toList.Perm t₂.toList
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_ge_of_countable_range : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {ι : Type u_4} [inst : LinearOrder ι] {τ : Ω → WithTop ι}
  {f : MeasureTheory.Filtration ι m},
  MeasureTheory.IsStoppingTime f τ → (Set.range τ).Countable → ∀ (i : ι), MeasurableSet {ω | ↑i ≤ τ ω}
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitHomIsoLimitYoneda.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (F : CategoryTheory.Functor I C) [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type u₂)] (A : C),
  CategoryTheory.Limits.colimitHomIsoLimitYoneda F A =
    (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda F).app A ≪≫
      CategoryTheory.Limits.limitObjIsoLimitCompEvaluation (F.op.comp CategoryTheory.coyoneda) A
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.lift_map_liftStar : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x ⟶ Z)
  (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x) (x : C),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.WithTerminal.lift F M hM).map
        (CategoryTheory.WithTerminal.starTerminal.from (CategoryTheory.WithTerminal.incl.obj x)))
      (CategoryTheory.WithTerminal.liftStar F M hM).hom =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.WithTerminal.inclLift F M hM).hom.app x) (M x)
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullback_const_smul_apply : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M}
  {V : (x : M') → TangentSpace I' x} {c : 𝕜},
  VectorField.mpullback I I' f (c • V) x = c • VectorField.mpullback I I' f V x
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
lt_inv_mul_iff_lt : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a b : α}, 1 < b⁻¹ * a ↔ b < a
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile.0.Std.IterM.step_takeWhileM.match_1.splitter : {m : Type u_1 → Type u_2} →
  {β : Type u_1} →
    [inst : MonadAttach m] →
      {P : β → m (ULift.{u_1, 0} Bool)} →
        (out : β) →
          (motive : Subtype (MonadAttach.CanReturn (P out)) → Sort u_3) →
            (__do_lift : Subtype (MonadAttach.CanReturn (P out))) →
              ((hP : MonadAttach.CanReturn (P out) { down := true }) → motive ⟨{ down := true }, hP⟩) →
                ((hP : MonadAttach.CanReturn (P out) { down := false }) → motive ⟨{ down := false }, hP⟩) →
                  motive __do_lift
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `antivaryOn_inv_left`. -/
MonovaryOn.inv_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f : ι → α} {g : ι → β}, MonovaryOn f g s → AntivaryOn f⁻¹ g s
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
/-- A pretransitive action is `n.succ-`preprimitive
iff the action of stabilizers is `n`-preprimitive.  -/
AddAction.isMultiplyPreprimitive_succ_iff_ofStabilizer : ∀ (M : Type u_1) (α : Type u_2) [inst : AddGroup M] [inst_1 : AddAction M α] [AddAction.IsPretransitive M α] {n : ℕ},
  1 ≤ n →
    ∀ {a : α},
      AddAction.IsMultiplyPreprimitive M α n.succ ↔
        AddAction.IsMultiplyPreprimitive (↥(AddAction.stabilizer M a)) (↥(SubAddAction.ofStabilizer M a)) n
-- Mathlib.RingTheory.Localization.InvSubmonoid
IsLocalization.toInvSubmonoid_eq_mk' : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalization M S] (x : ↥M), ↑((IsLocalization.toInvSubmonoid M S) x) = IsLocalization.mk' S 1 x
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instHashableCompletionItem.hash : Lean.Lsp.CompletionItem → UInt64
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.le_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {k fallback : α}, (cmp k (t.minKeyD fallback)).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.Data.Finmap
Finmap.lookup_union_left : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {s₁ s₂ : Finmap β},
  a ∈ s₁ → Finmap.lookup a (s₁ ∪ s₂) = Finmap.lookup a s₁