mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.Thickening
Metric.cthickening_subset_thickening : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ₁ : NNReal} {δ₂ : ℝ},
  ↑δ₁ < δ₂ → ∀ (E : Set α), Metric.cthickening (↑δ₁) E ⊆ Metric.thickening δ₂ E
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.instInhabitedMatchEqnsExtState : Inhabited Lean.Meta.Match.MatchEqnsExtState
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atom_mul_atom : ∀ {R : Type u_1} [inst : CommRing R] {W : ℤ → R},
  Function.Odd W →
    ∀ (a b c d : ℤ),
      IsEllipticNet.atom W a b * IsEllipticNet.atom W c d = IsEllipticNet.atom W b a * IsEllipticNet.atom W d c
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.comp_coimage_π_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} {f : P ⟶ Q}
  {R : C} {g : Q ⟶ R},
  CategoryTheory.CategoryStruct.comp f g = 0 →
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.Abelian.coimage.π g) = 0
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.mk_eq_zero_of_den : ∀ {ι : 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} (f : HomogeneousLocalization.NumDenSameDeg 𝒜 x),
  f.den = 0 → HomogeneousLocalization.mk f = 0
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiableWithinAt.clm_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_16} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {g : M → F₁ →L[𝕜] F₃}
  {f : M → F₂ →L[𝕜] F₁} {s : Set M} {x : M}, MDiffAt[s] g x → MDiffAt[s] f x → (MDiffAt[s] fun x => g x ∘SL f x) x
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.add : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (j : J)
  (x y : ↑(F.obj j)),
  CommRingCat.Colimits.Relation F (CommRingCat.Colimits.Prequotient.of j (x + y))
    ((CommRingCat.Colimits.Prequotient.of j x).add (CommRingCat.Colimits.Prequotient.of j y))
-- Init.Data.BitVec.Lemmas
BitVec.instLawfulCommIdentityHAndAllOnes : ∀ {n : ℕ}, Std.LawfulCommIdentity (fun x1 x2 => x1 &&& x2) (BitVec.allOnes n)
-- Lean.Elab.Tactic.Conv.Pattern
/-- The state corresponding to a `(occs := *)` pattern, which acts like `occs := 1 2 ... n` where
`n` is the total number of pattern matches.
* `subgoals` is the list of subgoals for patterns already matched
 -/
Lean.Elab.Tactic.Conv.PatternMatchState.all : Array Lean.MVarId → Lean.Elab.Tactic.Conv.PatternMatchState
-- Mathlib.Algebra.Algebra.Hom
Algebra.comp_ofId : ∀ {R : Type u} (A : Type v) (B : Type w) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (φ : A →ₐ[R] B), φ.comp (Algebra.ofId R A) = Algebra.ofId R B
-- Mathlib.Algebra.Order.Group.Action.End
/-- The tautological action by `r →r r` on `α`.  -/
RelHom.applyMulAction : {α : Type u_1} → {r : α → α → Prop} → MulAction (r →r r) α
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.val_eq_ite_valMinAbs : ∀ {n : ℕ} [NeZero n] (a : ZMod n), ↑a.val = a.valMinAbs + ↑(if a.val ≤ n / 2 then 0 else n)
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.ppow.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (f : ArithmeticFunction R) (k : ℕ),
  f.ppow k = if h0 : k = 0 then ↑ArithmeticFunction.zeta else { toFun := fun x => f x ^ k, map_zero' := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeIsoApp'_unit : ∀ (C : Type u) (n : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C),
  CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C
      (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.FreeMonoidalCategory C)) n =
    CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.FreeMonoidalCategory.inclusionObj n)
-- Mathlib.Algebra.Order.Group.PosPart
/-- See also `negPart_eq_neg`.  -/
negPart_eq_neg' : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : SubNegMonoid α] {a : α}, a⁻ = -a ↔ 0 ≤ -a
-- Mathlib.Tactic.FunProp.Decl
/-- path for discrimination tree  -/
Mathlib.Meta.FunProp.FunPropDecl.path : Mathlib.Meta.FunProp.FunPropDecl → Array Lean.Meta.DiscrTree.Key
-- Mathlib.Algebra.Module.NatInt
instMulActionIntOfSubtractionMonoid : {M : Type u_3} → [SubtractionMonoid M] → MulAction ℤ M
-- Mathlib.NumberTheory.NumberField.ClassNumber
/-- The class number of a number field is the (finite) cardinality of the class group.  -/
NumberField.classNumber : (K : Type u_1) → [inst : Field K] → [NumberField K] → ℕ
-- Mathlib.CategoryTheory.FiberedCategory.Fibered
/-- In a fibered category, any Cartesian morphism is strongly Cartesian.  -/
CategoryTheory.Functor.IsFibered.isStronglyCartesian_of_isCartesian : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) [p.IsFibered] {R S : 𝒮} (f : R ⟶ S) {a b : 𝒳} (φ : a ⟶ b) [p.IsCartesian f φ],
  p.IsStronglyCartesian f φ
-- Mathlib.Algebra.Category.Grp.ForgetCorepresentable
uliftZMultiplesHom_apply_add : ∀ (G : Type u) [inst : AddCommGroup G] (x y : G),
  (uliftZMultiplesHom G) (x + y) = (uliftZMultiplesHom G) x + (uliftZMultiplesHom G) y
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.Derivation.d_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R}
  (self : M.Derivation φ) {X : Cᵒᵖ} (a : ↑(S.obj X)), self.d ((CategoryTheory.ConcreteCategory.hom (φ.app X)) a) = 0
-- Mathlib.Data.Ineq
Mathlib.Ineq.le : Mathlib.Ineq
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.mk : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E],
  Topology.IsQuotientMap f →
    ContinuousConstSMul G E →
      (∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂) →
        (∀ (e : E), ∃ U ∈ nhds e, ∀ (g : G), ((fun x => g • x) '' U ∩ U).Nonempty → g = 1) → IsQuotientCoveringMap f G
-- Mathlib.Topology.UniformSpace.UniformConvergence
UniformCauchySeqOnFilter.mono_right : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {p : Filter ι}
  {p' p'' : Filter α}, UniformCauchySeqOnFilter F p p' → p'' ≤ p' → UniformCauchySeqOnFilter F p p''
-- Mathlib.Order.Basic
PUnit.instDenselyOrdered : DenselyOrdered PUnit.{u_5 + 1}
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.ofLp_zero : ∀ (p : ENNReal) {V : Type u_4} [inst : AddCommGroup V], WithLp.ofLp 0 = 0
-- Mathlib.Order.JordanHolder
CompositionSeries.mem_eraseLast : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s : CompositionSeries X} {x : X},
  0 < s.length → (x ∈ RelSeries.eraseLast s ↔ x ≠ RelSeries.last s ∧ x ∈ s)
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.Monic.eq_X_pow_iff_natDegree_le_natTrailingDegree : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R},
  p.Monic → (p = Polynomial.X ^ p.natDegree ↔ p.natDegree ≤ p.natTrailingDegree)
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.getElem_toList : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (p : Equiv.Perm α) (x : α) (n : ℕ)
  (hn : n < (p.toList x).length), (p.toList x)[n] = (p ^ n) x
-- Mathlib.CategoryTheory.Limits.Presentation
/-- The cone associated to a limit presentation.  -/
CategoryTheory.Limits.LimitPresentation.cone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        {X : C} → (pres : CategoryTheory.Limits.LimitPresentation J X) → CategoryTheory.Limits.Cone pres.diag
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.instBot : {M : Type u_1} → [inst : Monoid M] → Bot (Associates M)
-- Mathlib.Topology.Order.Lattice
ContinuousAt.sup : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] [inst_2 : Max L]
  [ContinuousSup L] {f g : X → L} {x : X}, ContinuousAt f x → ContinuousAt g x → ContinuousAt (fun a => f a ⊔ g a) x
-- Mathlib.Topology.QuasiSeparated
IsCompact.inter_of_isOpen : ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {U V : Set α},
  IsCompact U → IsCompact V → IsOpen U → IsOpen V → IsCompact (U ∩ V)
-- Mathlib.LinearAlgebra.Dual.BaseChange
Module.Dual.baseChange_apply_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] {V : Type u_2} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] (A : Type u_4)
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] (f : Module.Dual R V) (a : A) (v : V),
  ((Module.Dual.baseChange A) f) (a ⊗ₜ[R] v) = f v • a
-- Mathlib.LinearAlgebra.Projectivization.Basic
/-- The setoid whose quotient is the projectivization of `V`.  -/
projectivizationSetoid : (K : Type u_1) →
  (V : Type u_2) → [inst : DivisionRing K] → [inst_1 : AddCommGroup V] → [Module K V] → Setoid { v // v ≠ 0 }
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
/-- Extend a function on `ℍ` arbitrarily to a function on all of `ℂ`.  -/
UpperHalfPlane.«term↑ₕ_» : Lean.ParserDescr
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.naive_val : ∀ {R : Type u} [inst : CommRing R] {σ : Type u_2} {I : Ideal (MvPolynomial σ R)}
  (s : optParam (MvPolynomial σ R ⧸ I → MvPolynomial σ R) (Function.surjInv ⋯))
  (hs : autoParam (∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s x) = x) Algebra.Generators.naive._auto_1)
  (i : σ), (Algebra.Generators.naive s hs).val i = (Ideal.Quotient.mk I) (MvPolynomial.X i)
-- Init.WFExtrinsicFix
/-- A 3-ary fixpoint combinator that can be used to construct recursive functions with an
**extrinsic, partial** proof of termination.

Given a relation `R` and a fixpoint functional `F` which must be decreasing with respect
to `R`, `partialExtrinsicFix₃ R F` is the recursive function obtained by having `F` call
itself recursively.

For each pair of inputs `a`, `b` and `c`, `partialExtrinsicFix₃ R F a b` can be
verified given a **partial** termination proof. The precise semantics are as follows.

If `Acc R ⟨a, b, c⟩ ` does not hold, `partialExtrinsicFix₃ R F a b` might run forever. In this
case, nothing interesting can be proved about the recursive function; it is opaque and behaves like
a recursive function with the `partial` modifier.

If `Acc R ⟨a, b, c⟩` *does* hold, `partialExtrinsicFix₃ R F a b` is equivalent to
`F a b c (fun a' b' c' _ => partialExtrinsicFix₃ R F a' b' c')`, both logically and regarding its
termination behavior.

In particular, if `R` is well-founded, `partialExtrinsicFix₃ R F a b c` is equivalent to
a well-foundesd fixpoint.
 -/
WellFounded.partialExtrinsicFix₃ : {α : Sort u_1} →
  {β : α → Sort u_2} →
    {γ : (a : α) → β a → Sort u_3} →
      {C₃ : (a : α) → (b : β a) → γ a b → Sort u_4} →
        [∀ (a : α) (b : β a) (c : γ a b), Nonempty (C₃ a b c)] →
          (R : (a : α) ×' (b : β a) ×' γ a b → (a : α) ×' (b : β a) ×' γ a b → Prop) →
            ((a : α) →
                (b : β a) →
                  (c : γ a b) →
                    ((a' : α) → (b' : β a') → (c' : γ a' b') → R ⟨a', ⟨b', c'⟩⟩ ⟨a, ⟨b, c⟩⟩ → C₃ a' b' c') → C₃ a b c) →
              (a : α) → (b : β a) → (c : γ a b) → C₃ a b c
-- Mathlib.Topology.MetricSpace.Thickening
Metric.thickening_ball : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] (x : α) (ε δ : ℝ),
  Metric.thickening ε (Metric.ball x δ) ⊆ Metric.ball x (ε + δ)
-- Init.Grind.Module.Basic
Lean.Grind.AddCommGroup.sub_eq_zero_iff : ∀ {M : Type u} [inst : Lean.Grind.AddCommGroup M] {a b : M}, a - b = 0 ↔ a = b
-- Mathlib.Data.FunLike.Module
FunLike.isScalarTower : ∀ {M : Type u_1} {M' : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} [i : FunLike F α β] [inst : SMul M β]
  [inst_1 : SMul M' β] [inst_2 : SMul M F] [inst_3 : SMul M' F] [IsSMulApply M F α β] [IsSMulApply M' F α β]
  [inst_6 : SMul M M'] [IsScalarTower M M' β], IsScalarTower M M' F
-- Lean.Data.Lsp.Basic
Lean.Lsp.VersionedTextDocumentIdentifier.mk.injEq : ∀ (uri : Lean.Lsp.DocumentUri) (version? : Option ℕ) (uri_1 : Lean.Lsp.DocumentUri) (version?_1 : Option ℕ),
  ({ uri := uri, version? := version? } = { uri := uri_1, version? := version?_1 }) =
    (uri = uri_1 ∧ version? = version?_1)
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.measurableSet_memPartitionSet : ∀ {α : Type u_1} [inst : MeasurableSpace α] {t : ℕ → Set α},
  (∀ (n : ℕ), MeasurableSet (t n)) → ∀ (n : ℕ) (a : α), MeasurableSet (memPartitionSet t n a)
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.isUnit_prod_comp_inverse : ∀ {n : Type u_1} {R : Type u₂} [inst : DecidableEq n] [inst_1 : CommRing R] [inst_2 : Fintype n]
  (L : List (Matrix.TransvectionStruct n R)),
  IsUnit (List.map (Matrix.TransvectionStruct.toMatrix ∘ Matrix.TransvectionStruct.inv) L).prod
-- Mathlib.Algebra.WithConv
WithConv.ext_iff : ∀ {A : Type u_2} {x y : WithConv A}, x = y ↔ x.ofConv = y.ofConv
-- Mathlib.Analysis.Calculus.Implicit
/-- Given a map `f : E → F` to a finite-dimensional space with a surjective derivative `f'`,
returns an open partial homeomorphism between `E` and `F × ker f'`.  -/
HasStrictFDerivAt.implicitToOpenPartialHomeomorph : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    [CompleteSpace 𝕜] →
      {E : Type u_2} →
        [inst_2 : NormedAddCommGroup E] →
          [inst_3 : NormedSpace 𝕜 E] →
            [CompleteSpace E] →
              {F : Type u_3} →
                [inst_5 : NormedAddCommGroup F] →
                  [inst_6 : NormedSpace 𝕜 F] →
                    [FiniteDimensional 𝕜 F] →
                      (f : E → F) →
                        (f' : E →L[𝕜] F) →
                          {a : E} →
                            HasStrictFDerivAt f f' a → (↑f').range = ⊤ → OpenPartialHomeomorph E (F × ↥(↑f').ker)
-- Mathlib.Order.Interval.Set.SuccPred
Set.insert_Ioc_right_eq_Ioc_succ_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α},
  a ≤ b → ¬IsMax b → insert (Order.succ b) (Set.Ioc a b) = Set.Ioc a (Order.succ b)
-- Mathlib.Data.Prod.TProd
/-- Turning a function `f : ∀ i, α i` into an element of the iterated product `TProd α l`.  -/
List.TProd.mk : {ι : Type u} → {α : ι → Type v} → (l : List ι) → ((i : ι) → α i) → List.TProd α l
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.instSubHom : {R : Type u} → [inst : Ring R] → {M N : ModuleCat R} → Sub (M ⟶ N)
-- Mathlib.Probability.Kernel.Composition.MapComap
/-- The pushforward of a kernel along a function.
If the function is not measurable, we use zero instead. This choice of junk
value ensures that typeclass inference can infer that the `map` of a kernel
satisfying `IsZeroOrMarkovKernel` again satisfies this property.  -/
ProbabilityTheory.Kernel.map : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        {γ : Type u_4} →
          [inst : MeasurableSpace γ] → ProbabilityTheory.Kernel α β → (β → γ) → ProbabilityTheory.Kernel α γ
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instBoundedOrder : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → [inst : LE β] → [BoundedOrder β] → BoundedOrder (l.Germ β)
-- Mathlib.Algebra.Group.Hom.Defs
/-- Composition of `AddHom`s as an `AddHom`.  -/
AddHom.comp : {M : Type u_4} →
  {N : Type u_5} →
    {P : Type u_6} → [inst : Add M] → [inst_1 : Add N] → [inst_2 : Add P] → (N →ₙ+ P) → (M →ₙ+ N) → M →ₙ+ P
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succ_lt_succ_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.PRange.InfinitelyUpwardEnumerable α] [Std.PRange.LinearlyUpwardEnumerable α] {a b : α},
  Std.PRange.UpwardEnumerable.LT (Std.PRange.succ a) (Std.PRange.succ b) ↔ Std.PRange.UpwardEnumerable.LT a b
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- A subgroupoid of `C` consists of a choice of arrows for each pair of vertices, closed
under composition and inverses.
 -/
CategoryTheory.Subgroupoid : (C : Type u) → [CategoryTheory.Groupoid C] → Type (max u u_1)
-- Mathlib.Topology.Order.LeftRightNhds
LinearOrderedCommGroup.tendsto_nhds : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : CommGroup α] [inst_2 : LinearOrder α]
  [IsOrderedMonoid α] [OrderTopology α] {f : β → α} {x : Filter β} {a : α},
  Filter.Tendsto f x (nhds a) ↔ ∀ ε > 1, ∀ᶠ (b : β) in x, |f b / a|ₘ < ε
-- Lean.Meta.Tactic.Grind.ProveEq
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.AbstractM.State.cache : Lean.Meta.Grind.AbstractM.State✝ → Std.HashMap (Lean.Expr × Lean.Expr) Lean.Expr
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
SchwartzMap.fourier_evalCLM_eq : ∀ {V : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
  [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V] (𝕜' : Type u_4) [inst_5 : NormedField 𝕜'] {F : Type u_5}
  [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace ℝ F] {G : Type u_6} [inst_8 : NormedAddCommGroup G]
  [inst_9 : NormedSpace ℂ G] [inst_10 : NormedSpace 𝕜' G] [inst_11 : SMulCommClass ℝ 𝕜' G]
  (f : SchwartzMap V (F →L[ℝ] G)) (m : F),
  FourierTransform.fourier ((SchwartzMap.evalCLM 𝕜' V G m) f) =
    (SchwartzMap.evalCLM 𝕜' V G m) (FourierTransform.fourier f)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.precomp_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
  {W' : CategoryTheory.MorphismProperty C} [W.RespectsLeft W'] [W.HasOfPrecompProperty W'] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z), W' f → (W (CategoryTheory.CategoryStruct.comp f g) ↔ W g)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.comp_natTrans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  {X Y Z : CategoryTheory.MonoidalCategory.DayFunctor C V} (α : X.Hom Y) (β : Y.Hom Z),
  (CategoryTheory.CategoryStruct.comp α β).natTrans = CategoryTheory.CategoryStruct.comp α.natTrans β.natTrans
-- Lean.Util.SCC
_private.Lean.Util.SCC.0.Lean.SCC.sccAux : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → (α → List α) → α → Lean.SCC.M α Unit
-- Init.Data.Iterators.Combinators.Monadic.ULift
Std.Iterators.Types.ULiftIterator.instProductive : ∀ {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u}
  {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} [inst : Std.Iterator α m β] [Std.Iterators.Productive α m]
  [inst_2 : Monad n], Std.Iterators.Productive (Std.Iterators.Types.ULiftIterator α m n β lift) n
-- Mathlib.Topology.UniformSpace.Real
NNReal.instCompleteSpace : CompleteSpace NNReal
-- Mathlib.GroupTheory.Sylow
/-- A special case of **Sylow's first theorem**. If `G` is a `p`-group and `H` a subgroup of size at
least `k` then there is a subgroup of `H` of cardinality between `k / p` and `k`.  -/
Sylow.exists_subgroup_le_card_le : ∀ {G : Type u} [inst : Group G] {k p : ℕ},
  Nat.Prime p →
    IsPGroup p G → ∀ {H : Subgroup G}, k ≤ Nat.card ↥H → k ≠ 0 → ∃ H' ≤ H, Nat.card ↥H' ≤ k ∧ k < p * Nat.card ↥H'
-- Lean.Server.FileWorker.ExampleHover
/-- In a non-`output` code block opened with `ticks` backtick characters  -/
_private.Lean.Server.FileWorker.ExampleHover.0.Lean.Server.FileWorker.Hover.RWState.nonOutput : ℕ → Lean.Server.FileWorker.Hover.RWState✝
-- Mathlib.Data.Multiset.AddSub
Multiset.erase_le_erase : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α} (a : α), s ≤ t → s.erase a ≤ t.erase a
-- Mathlib.Algebra.Order.GroupWithZero.Basic
Right.neg_of_mul_neg_right : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : LinearOrder α] [MulPosMono α], a * b < 0 → 0 ≤ a → b < 0
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.intSpanEquivQuotAddOrderOf_apply_self : ∀ {A : Type uA} [inst : AddCommGroup A] (a : A),
  (CharacterModule.intSpanEquivQuotAddOrderOf a) ⟨a, ⋯⟩ = Submodule.Quotient.mk 1
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_ofNat : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (n : ℕ)
  [inst_4 : n.AtLeastTwo], ⌊OfNat.ofNat n⌋ = OfNat.ofNat n
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous
MeasureTheory.Lp.instContinuousVAddDomAddAct : ∀ {X : Type u_1} {M : Type u_2} {E : Type u_3} [inst : TopologicalSpace X] [R1Space X] [inst_2 : MeasurableSpace X]
  [inst_3 : BorelSpace X] [inst_4 : TopologicalSpace M] [inst_5 : MeasurableSpace M] [inst_6 : OpensMeasurableSpace M]
  [inst_7 : VAdd M X] [inst_8 : ContinuousVAdd M X] [inst_9 : NormedAddCommGroup E] {μ : MeasureTheory.Measure X}
  [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.InnerRegularCompactLTTop]
  [inst_12 : MeasureTheory.VAddInvariantMeasure M X μ] {p : ENNReal} [inst_13 : Fact (1 ≤ p)] [hp : Fact (p ≠ ⊤)],
  ContinuousVAdd Mᵈᵃᵃ ↥(MeasureTheory.Lp E p μ)
-- Init.Data.SInt.Bitwise
Int8.shiftRight_xor : ∀ {a b c : Int8}, (a ^^^ b) >>> c = a >>> c ^^^ b >>> c
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rco_eq_nil_iff : ∀ {m n : ℕ}, (m...n).toList = [] ↔ n ≤ m
-- Init.WF
/-- A proof that `rel` is, in fact, well-founded.  -/
WellFoundedRelation.wf : ∀ {α : Sort u} [self : WellFoundedRelation α], WellFounded WellFoundedRelation.rel
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuedAdicCompletion_def : ∀ {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)
  {x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v}, Valued.v x = Valued.extensionValuation x.toCompletion
-- Mathlib.Data.Finset.NAry
Finset.card_image₂ : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ},
  Function.Injective2 f → ∀ (s : Finset α) (t : Finset β), (Finset.image₂ f s t).card = s.card * t.card
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
multipliable_sineTerm : ∀ (x : ℂ), Multipliable fun i => 1 + sineTerm x i
-- Mathlib.Algebra.Group.Equiv.TypeTags
AddEquiv.piAdditive_symm_apply : ∀ {ι : Type u_1} (K : ι → Type u_4) [inst : (i : ι) → Mul (K i)] (x : (i : ι) → Additive (K i)),
  (AddEquiv.piAdditive K).symm x = Additive.ofMul fun i => Additive.toMul (x i)
-- Init.Core
/-- `LeftIdentity op o` indicates `o` is a left identity of `op`.

This class does not require a proof that `o` is an identity, and
is used primarily for inferring the identity using class resolution.
 -/
Std.LeftIdentity : {α : Sort u} → {β : Sort u_1} → (α → β → β) → outParam α → Prop
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.Context.mk.sizeOf_spec : ∀ (u : Lean.Level) (type fieldInst isChar0Inst ringInst semiringInst : Lean.Expr),
  sizeOf
      { u := u, type := type, fieldInst := fieldInst, isChar0Inst := isChar0Inst, ringInst := ringInst,
        semiringInst := semiringInst } =
    1 + sizeOf u + sizeOf type + sizeOf fieldInst + sizeOf isChar0Inst + sizeOf ringInst + sizeOf semiringInst