mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Regular.Basic
/-- If an element `b` becomes right-regular after multiplying it on the right by a right-regular
element, then `b` is right-regular.  -/
IsRightRegular.of_mul : ∀ {R : Type u_1} [inst : Semigroup R] {a b : R}, IsRightRegular (b * a) → IsRightRegular b
-- Mathlib.Data.Fin.Rev
Fin.rev_involutive : ∀ {n : ℕ}, Function.Involutive Fin.rev
-- Mathlib.Tactic.CategoryTheory.Coherence
Mathlib.Tactic.Coherence.LiftObj.mk : {C : Type u} → {X : C} → CategoryTheory.FreeMonoidalCategory C → Mathlib.Tactic.Coherence.LiftObj X
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
/-- An object `J` is injective iff every morphism into `J` can be obtained by extending a monomorphism.
 -/
CategoryTheory.Injective : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → C → Prop
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.domRestrict_apply : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  (f : BoundedContinuousFunction α β) (s : Set α) (x : ↑s), (f.domRestrict s) x = f ↑x
-- Std.Do.WP.SimpLemmas
Except.tryCatch.eq_2 : ∀ {ε : Type u} {α : Type u_1} (handle : ε → Except ε α) (a : ε), (Except.error a).tryCatch handle = handle a
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.toProd_apply_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] (x : M),
  Monoid.Coprod.toProd (Monoid.Coprod.inl x) = (x, 1)
-- Init.Data.SInt.IntToBitVec
Int8.toBitVec64_toISize : ∀ (n : Int8) (h : System.Platform.numBits = 64), n.toISize.toBitVec64 h = BitVec.signExtend 64 n.toBitVec
-- Mathlib.Topology.Defs.Sequences
/-- A topological space is said to be a *sequential space* if any sequentially closed set in this
space is closed. This condition is weaker than being a Fréchet-Urysohn space.  -/
SequentialSpace : (X : Type u_1) → [TopologicalSpace X] → Prop
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonTextDocumentItem.fromJson : Lean.Json → Except String Lean.Lsp.TextDocumentItem
-- Mathlib.Algebra.Order.Group.PosPart
oneLePart_eq_ite_lt : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Group α] {a : α}, a⁺ᵐ = if 1 < a then a else 1
-- Mathlib.Order.Filter.Basic
Filter.Eventually.lt_top_iff_ne_top : ∀ {α : Type u} {β : Type v} [inst : PartialOrder β] [inst_1 : OrderTop β] {l : Filter α} {f : α → β},
  (∀ᶠ (x : α) in l, f x < ⊤) ↔ ∀ᶠ (x : α) in l, f x ≠ ⊤
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasStrictDerivAt.scomp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  [inst_5 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {h : 𝕜 → 𝕜'} {h' : 𝕜'} {g₁ : 𝕜' → F} {g₁' : F},
  HasStrictDerivAt g₁ g₁' (h x) → HasStrictDerivAt h h' x → HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.shiftShortComplexFunctor'_inv_app_τ₂ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ),
  ((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).inv.app X).τ₂ =
    (HomologicalComplex.XIsoOfEq X ⋯).inv
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Like `MulZeroClass.toSMulWithZero`, but multiplies on the right.  -/
MulZeroClass.toOppositeSMulWithZero : (M₀ : Type u_2) → [inst : MulZeroClass M₀] → SMulWithZero M₀ᵐᵒᵖ M₀
-- Mathlib.RingTheory.Jacobson.Radical
Ring.jacobson_eq_sInf_isMaximal : ∀ (R : Type u_1) [inst : Ring R], Ring.jacobson R = sInf {I | I.IsMaximal}
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.iInf_normalizer_le_normalizer_iSup : ∀ {G : Type u_2} [inst : AddGroup G] {ι : Sort u_5} (H : ι → AddSubgroup G),
  ⨅ i, AddSubgroup.normalizer ↑(H i) ≤ AddSubgroup.normalizer ↑(⨆ i, H i)
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.Expr.denote_toPoly'_go : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] {k : ℤ} {p : Lean.Grind.Linarith.Poly}
  (ctx : Lean.Grind.Linarith.Context α) (e : Lean.Grind.Linarith.Expr),
  Lean.Grind.Linarith.Poly.denote ctx (Lean.Grind.Linarith.Expr.toPoly'.go k e p) =
    k • Lean.Grind.Linarith.Expr.denote ctx e + Lean.Grind.Linarith.Poly.denote ctx p
-- Lean.Meta.DiscrTree.Basic
Lean.Meta.DiscrTree.Trie.format : {α : Type} → [Std.ToFormat α] → Lean.Meta.DiscrTree.Trie α → Std.Format
-- Mathlib.Algebra.Module.Congruence.Defs
ModuleCon.instDistribSMulQuotient : {S : Type u_2} →
  (M : Type u_3) →
    [inst : AddZeroClass M] → [inst_1 : DistribSMul S M] → (c : ModuleCon S M) → DistribSMul S (ModuleCon.Quotient M c)
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
DirectSum.toAddMonoidAlgebra_sub : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Ring M] [inst_2 : (m : M) → Decidable (m ≠ 0)]
  (f g : DirectSum ι fun x => M), (f - g).toAddMonoidAlgebra = f.toAddMonoidAlgebra - g.toAddMonoidAlgebra
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.mk.sizeOf_spec : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {S : C} [inst_2 : SizeOf C₀] [inst_3 : SizeOf C]
  (toPreOneHypercoverDenseData : F.PreOneHypercoverDenseData S)
  (mem₀ : toPreOneHypercoverDenseData.toPreOneHypercover.sieve₀ ∈ J S)
  (mem₁₀ :
    ∀ (i₁ i₂ : toPreOneHypercoverDenseData.I₀) ⦃W₀ : C₀⦄ (p₁ : W₀ ⟶ toPreOneHypercoverDenseData.X i₁)
      (p₂ : W₀ ⟶ toPreOneHypercoverDenseData.X i₂),
      CategoryTheory.CategoryStruct.comp (F.map p₁) (toPreOneHypercoverDenseData.f i₁) =
          CategoryTheory.CategoryStruct.comp (F.map p₂) (toPreOneHypercoverDenseData.f i₂) →
        toPreOneHypercoverDenseData.sieve₁₀ p₁ p₂ ∈ J₀ W₀),
  sizeOf { toPreOneHypercoverDenseData := toPreOneHypercoverDenseData, mem₀ := mem₀, mem₁₀ := mem₁₀ } =
    1 + sizeOf toPreOneHypercoverDenseData + sizeOf mem₀
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.minValueSealed : Int32
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.δ₀_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} {x : CategoryTheory.ComposableArrows C (n + 1)},
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (CategoryTheory.nerve C) 0)) x = x.δ₀
-- Std.Data.DHashMap.Raw
/-- Transforms the hash map into an array of mappings in some order.  -/
Std.DHashMap.Raw.Const.toArray : {α : Type u} → {β : Type v} → (Std.DHashMap.Raw α fun x => β) → Array (α × β)
-- Mathlib.Order.WellFounded
WellFounded.maximal_wellFounded_lt_max : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : WellFoundedGT α] {s : Set α} (h : s.Nonempty),
  Maximal (fun x => x ∈ s) (⋯.min s h)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getEntryGE?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.getEntryGE? k = t₂.getEntryGE? k
-- Init.Data.UInt.Lemmas
UInt32.toUInt32_toUSize : ∀ (n : UInt32), n.toUSize.toUInt32 = n
-- Mathlib.Algebra.BigOperators.Ring.Multiset
Commute.multiset_sum_left : ∀ {R : Type u_4} [inst : NonUnitalNonAssocSemiring R] (s : Multiset R) (b : R), (∀ a ∈ s, Commute a b) → Commute s.sum b
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (F G : CochainComplex C ℤ) (i : ℤ), (F.HomComplex G).X i = AddCommGrpCat.of (CochainComplex.HomComplex.Cochain F G i)
-- Mathlib.Data.Nat.GCD.Basic
Nat.coprime_iff_isRelPrime : ∀ {m n : ℕ}, m.Coprime n ↔ IsRelPrime m n
-- Mathlib.Tactic.FunProp.Decl
/-- Is `e` a function property statement?  -/
Mathlib.Meta.FunProp.isFunProp : Lean.Expr → Lean.MetaM Bool
-- Std.Data.HashMap.Basic
Std.HashMap.instSDiff : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → SDiff (Std.HashMap α β)
-- Mathlib.Data.Fin.Basic
Fin.val_add_eq_ite : ∀ {n : ℕ} (a b : Fin n), ↑(a + b) = if n ≤ ↑a + ↑b then ↑a + ↑b - n else ↑a + ↑b
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → t.getKey? t.minKey! = some t.minKey!
-- Init.PropLemmas
exists_or_eq_right' : ∀ {α : Sort u_1} (y : α) (p : α → Prop), ∃ x, p x ∨ y = x
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.isTangentAt_center_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {as : AffineSubspace ℝ P},
  s.IsTangentAt s.center as ↔ s.radius = 0 ∧ s.center ∈ as
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
/-- The canonical ring homomorphism from a commutative semiring to the product of its
localizations at all maximal ideals. It is always injective.  -/
MaximalSpectrum.toPiLocalization : (R : Type u_1) → [inst : CommSemiring R] → R →ₐ[R] MaximalSpectrum.PiLocalization R
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.π_comp_colimitRightOpIsoUnopLimit_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ C) [inst_2 : CategoryTheory.Limits.HasLimit F] (j : Jᵒᵖ) {Z : Cᵒᵖ}
  (h : CategoryTheory.Limits.colimit F.rightOp ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j).op
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitRightOpIsoUnopLimit F).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F.rightOp (Opposite.unop j)) h
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.closure_mem_compactNhds_of_mem_openRcNhds : ∀ {α : Type u_1} [inst : TopologicalSpace α] {K : TopologicalSpace.Compacts α} {U : TopologicalSpace.Opens α}
  (h : U ∈ K.openRcNhds), { carrier := closure ↑U, isCompact' := ⋯ } ∈ K.compactNhds
-- Mathlib.Algebra.Order.Sub.Basic
tsub_self : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] (a : α), a - a = 0
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime_toSubring : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  (IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime K v).toSubring =
    (Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯).toSubring
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.tryCatch_ExceptT_lift : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε ε' α : Type u}
  [inst_4 : MonadExceptOf ε m] (x : ExceptT ε' m α) (h : ε → ExceptT ε' m α) (post : α → Pred)
  (epost : EPost.Cons✝ (ε' → Pred) EPred),
  ⦃
    Std.Internal.Do.wp (MonadExceptOf.tryCatch x h)
      (fun x =>
        match x with
        | Except.ok a => post a
        | Except.error e => epost.head e)
      epost.tail ⦄
    MonadExceptOf.tryCatch x h ⦃ post; epost ⦄
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
/-- The exterior derivative of a `0`-form given by a function `f`
is the 1-form given by the derivative of `f`.  -/
extDeriv_constOfIsEmpty : ∀ {𝕜 : 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 : E → F) (x : E),
  extDeriv (fun x => ContinuousAlternatingMap.constOfIsEmpty 𝕜 E (Fin 0) (f x)) x =
    (ContinuousAlternatingMap.ofSubsingleton 𝕜 E F 0) (fderiv 𝕜 f x)
-- Init.Data.BitVec.Bitblast
/-- The `[0..len)` low bits of `x + y` can be computed by truncating `x` and `y`
to `len` bits and then adding.
 -/
BitVec.extractLsb'_add : ∀ {w len : ℕ} {x y : BitVec w},
  len ≤ w → BitVec.extractLsb' 0 len (x + y) = BitVec.extractLsb' 0 len x + BitVec.extractLsb' 0 len y
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.gi.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G],
  AddSubgroup.gi G = { choice := fun s x => AddSubgroup.closure s, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
-- Mathlib.Algebra.Ring.Divisibility.Lemmas
dvd_mul_sub_mul_mul_left_of_dvd : ∀ {R : Type u_1} [inst : CommRing R] {p a b c d x y : R},
  p ∣ a * x + b * y → p ∣ c * x + d * y → p ∣ (a * d - b * c) * x
-- Mathlib.Data.List.Indexes
_private.Mathlib.Data.List.Indexes.0.List.mapIdxMAux'.match_1.splitter : {α : Type u_1} →
  (motive : ℕ → List α → Sort u_2) →
    (x : ℕ) →
      (x_1 : List α) → ((x : ℕ) → motive x []) → ((i : ℕ) → (a : α) → (as : List α) → motive i (a :: as)) → motive x x_1
-- Mathlib.Logic.Function.Basic
Function.FactorsThrough.extend_comp : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : α → γ} (e' : β → γ),
  Function.FactorsThrough g f → Function.extend f g e' ∘ f = g
-- Init.Data.String.Lemmas.Order
String.Pos.lt_sliceFrom_iff : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h : p₀ ≤ q},
  p < p₀.sliceFrom q h ↔ String.Pos.ofSliceFrom p < q
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.commRight_symm_tmul : ∀ (R : Type uR) {S : Type uS} {A : Type uA} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (s : S) (a : A),
  (Algebra.TensorProduct.commRight R S A).symm (a ⊗ₜ[R] s) = s ⊗ₜ[R] a
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.mem_graph_iff : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] (f : E →ₗ.[R] F) {x : E × F}, x ∈ f.graph ↔ ∃ y, ↑y = x.1 ∧ ↑f y = x.2
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.flipping_inverse_map_app_app : ∀ {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₁ F₂ : CategoryTheory.Functor D (CategoryTheory.Functor C E)} (φ : F₁ ⟶ F₂) (Y : C) (X : D),
  ((CategoryTheory.Functor.flipping.inverse.map φ).app Y).app X = (φ.app X).app Y
-- Init.Data.List.Sort.Lemmas
List.mergeSort_cons : ∀ {α : Type u_1} {le : α → α → Bool},
  (∀ (a b c : α), le a b = true → le b c = true → le a c = true) →
    (∀ (a b : α), (le a b || le b a) = true) →
      ∀ (a : α) (l : List α),
        ∃ l₁ l₂, (a :: l).mergeSort le = l₁ ++ a :: l₂ ∧ l.mergeSort le = l₁ ++ l₂ ∧ ∀ b ∈ l₁, (!le a b) = true
-- Mathlib.Algebra.Category.CoalgCat.Basic
/-- Build a `CoalgEquiv` from an isomorphism in the category
`CoalgCat R`.  -/
CategoryTheory.Iso.toCoalgEquiv : {R : Type u} → [inst : CommRing R] → {X Y : CoalgCat R} → (X ≅ Y) → ↑X.toModuleCat ≃ₗc[R] ↑Y.toModuleCat
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- We will make use of the natural quotient map from the free category on the underlying
quiver of a refl quiver to the free category on the reflexive quiver.  -/
CategoryTheory.Cat.freeReflNatTrans : CategoryTheory.ReflQuiv.forgetToQuiv.comp CategoryTheory.Cat.free ⟶ CategoryTheory.Cat.freeRefl
-- Mathlib.RingTheory.ClassGroup.Basic
toPrincipalIdeal_def : ∀ (R : Type u_3) (K : Type u_4) [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K],
  toPrincipalIdeal R K =
    {
      toFun := fun x =>
        { val := FractionalIdeal.spanSingleton (nonZeroDivisors R) ↑x,
          inv := FractionalIdeal.spanSingleton (nonZeroDivisors R) (↑x)⁻¹, val_inv := ⋯, inv_val := ⋯ },
      map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
/-- The inverse Fourier transform satisfies `∫ 𝓕⁻ f * g = ∫ f * 𝓕⁻ g`, i.e., it is self-adjoint.

Version where the multiplication is replaced by a general bilinear form `M`.  -/
SchwartzMap.integral_bilin_fourierInv_eq : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_3} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V] [inst_6 : BorelSpace V]
  {F : Type u_4} [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace ℂ F] {G : Type u_5}
  [inst_9 : NormedAddCommGroup G] [inst_10 : NormedSpace ℂ G] [CompleteSpace E] [CompleteSpace F] (f : SchwartzMap V E)
  (g : SchwartzMap V F) (M : E →L[ℂ] F →L[ℂ] G),
  ∫ (ξ : V), (M ((FourierTransformInv.fourierInv f) ξ)) (g ξ) =
    ∫ (x : V), (M (f x)) ((FourierTransformInv.fourierInv g) x)
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_toUInt64 : ∀ (n : UInt8), n.toUInt64.toBitVec = BitVec.setWidth 64 n.toBitVec
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearMap.BilinMap.toQuadraticMap_apply : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (B : LinearMap.BilinMap R M N) (x : M), B.toQuadraticMap x = (B x) x
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.Relations.isQF : ∀ {L : FirstOrder.Language} {α : Type u'} {n l : ℕ} (r : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin n)),
  (r.boundedFormula ts).IsQF
-- Mathlib.Topology.Order.IsLUB
/-- **Alias** of `IsGLB.mem_of_isClosed`. -/
IsClosed.isGLB_mem : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α} {s : Set α},
  IsGLB s a → s.Nonempty → IsClosed s → a ∈ s
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.fromZeroRingHom.eq_1 : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] (𝒜 : ι → σ)
  [inst_5 : GradedRing 𝒜] (x : Submonoid A),
  HomogeneousLocalization.fromZeroRingHom 𝒜 x =
    { toFun := fun f => HomogeneousLocalization.mk { deg := 0, num := f, den := 1, den_mem := ⋯ }, map_one' := ⋯,
      map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.isBounded_image : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  (f : BoundedContinuousFunction α β) (s : Set α), Bornology.IsBounded (⇑f '' s)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.limitRecOn_succ : ∀ {motive : Ordinal.{u_4} → Sort u_5} (o : Ordinal.{u_4}) (H₁ : motive 0)
  (H₂ : (o : Ordinal.{u_4}) → motive o → motive (o + 1))
  (H₃ : (o : Ordinal.{u_4}) → Order.IsSuccLimit o → ((o' : Ordinal.{u_4}) → o' < o → motive o') → motive o),
  Ordinal.limitRecOn (Order.succ o) H₁ H₂ H₃ = H₂ o (Ordinal.limitRecOn o H₁ H₂ H₃)
-- Mathlib.Analysis.Analytic.OfScalars
FormalMultilinearSeries.ofScalars_series_eq_zero : ∀ {𝕜 : Type u_1} (E : Type u_2) [inst : Field 𝕜] [inst_1 : Ring E] [inst_2 : Algebra 𝕜 E] [inst_3 : TopologicalSpace E]
  [inst_4 : IsTopologicalRing E] {c : ℕ → 𝕜} [Nontrivial E], FormalMultilinearSeries.ofScalars E c = 0 ↔ c = 0
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
/-- Given two strongly Cartesian morphisms `φ`, `ψ` as follows
```
a --φ--> b --ψ--> c
|        |        |
v        v        v
R --f--> S --g--> T
```
Then the composite `φ ≫ ψ` is also strongly Cartesian.  -/
CategoryTheory.Functor.IsStronglyCartesian.comp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S T : 𝒮} {a b c : 𝒳} {f : R ⟶ S} {g : S ⟶ T} {φ : a ⟶ b} {ψ : b ⟶ c}
  [p.IsStronglyCartesian f φ] [p.IsStronglyCartesian g ψ],
  p.IsStronglyCartesian (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp φ ψ)
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.lift_apply_dp : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_4}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {I : Ideal A} (hI : DividedPowers I) {g : M →ₗ[R] A}
  (hg : ∀ (m : M), g m ∈ I) (n : ℕ) (m : M),
  (DividedPowerAlgebra.lift hI g hg) (DividedPowerAlgebra.dp R n m) = hI.dpow n (g m)
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degrees_map_le : ∀ {R : Type u} {S : Type v} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} [inst_1 : CommSemiring S]
  {f : R →+* S}, ((MvPolynomial.map f) p).degrees ≤ p.degrees
-- Init.WF
WellFoundedRelation.mk : {α : Sort u} → (rel : α → α → Prop) → WellFounded rel → WellFoundedRelation α
-- Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
/-- The `R`-linear map `S →ₗ[R] S ⊗[R] S` sending `s : S` to `s ⊗ₜ 1 - 1 ⊗ₜ s`.  -/
Algebra.TensorProduct.includeLeftSubRight : (R : Type u_1) →
  [inst : CommSemiring R] → (S : Type u_2) → [inst_1 : Ring S] → [inst_2 : Algebra R S] → S →ₗ[R] TensorProduct R S S
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
analyticWithinAt_sigmoid : ∀ {x : ℝ} {s : Set ℝ}, AnalyticWithinAt ℝ Real.sigmoid s x
-- Std.Time.Date.Unit.Day
Std.Time.Day.instOrdOffset : Ord Std.Time.Day.Offset
-- Mathlib.Algebra.Homology.ImageToKernel
imageToKernel_zero_right : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V}
  (f : A ⟶ B) [inst_2 : CategoryTheory.Limits.HasImages V] {w : CategoryTheory.CategoryStruct.comp f 0 = 0},
  imageToKernel f 0 w =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow
      (CategoryTheory.inv (CategoryTheory.Limits.kernelSubobject 0).arrow)
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.vaddAssocClass' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : DecidableEq γ] [inst_1 : DecidableEq β] [inst_2 : VAdd α β]
  [inst_3 : VAdd α γ] [inst_4 : VAdd β γ] [VAddAssocClass α β γ], VAddAssocClass α (Finset β) (Finset γ)
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.ringJacobson_le_jacobson : ∀ {R : Type u} [inst : Ring R] {I : Ideal R}, Ring.jacobson R ≤ I.jacobson
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.DelayedTheoremInstance.guards : Lean.Meta.Grind.DelayedTheoremInstance → List Lean.Meta.Grind.TheoremGuard
-- Mathlib.Data.PNat.Factors
/-- `PrimeMultiset.coe`, the coercion from a multiset of primes to a multiset of
naturals, promoted to an `AddMonoidHom`.  -/
PrimeMultiset.coeNatMonoidHom : PrimeMultiset →+ Multiset ℕ
-- Aesop.Rule.Name
Aesop.DisplayRuleName.normUnfold.sizeOf_spec : sizeOf Aesop.DisplayRuleName.normUnfold = 1
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
TopCat.toSSetObj₀Equiv_apply : ∀ {X : TopCat} (a : (TopCat.toSSet.obj X).obj (Opposite.op { len := 0 })),
  TopCat.toSSetObj₀Equiv a = ((X.toSSetObjEquiv (Opposite.op { len := 0 })) a) default
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_inv : ∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_4} [inst_1 : LinearOrderedAddCommGroupWithTop Γ₀]
  (v : AddValuation K Γ₀) {x : K}, v x⁻¹ = -v x
-- Init.Data.SInt.Lemmas
Int64.pow_succ : ∀ (x : Int64) (n : ℕ), x ^ (n + 1) = x ^ n * x
-- Mathlib.Algebra.GroupWithZero.Defs
MulZeroClass.toMul : {M₀ : Type u} → [self : MulZeroClass M₀] → Mul M₀
-- Mathlib.Topology.Category.TopCat.OpenNhds
TopologicalSpace.OpenNhds.inclusionMapIso_inv : ∀ {X Y : TopCat} (f : X ⟶ Y) (x : ↑X),
  (TopologicalSpace.OpenNhds.inclusionMapIso f x).inv =
    CategoryTheory.CategoryStruct.id ((TopologicalSpace.OpenNhds.map f x).comp (TopologicalSpace.OpenNhds.inclusion x))
-- Mathlib.GroupTheory.NoncommPiCoprod
/-- The canonical homomorphism from a family of subgroups where elements from different subgroups
commute  -/
Subgroup.noncommPiCoprod : {G : Type u_1} →
  [inst : Group G] →
    {ι : Type u_2} →
      {H : ι → Subgroup G} →
        [Fintype ι] → (Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y) → ((i : ι) → ↥(H i)) →* G