mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.UniformSpace.Basic
/-- A version of `uniformContinuous_sInf_dom` for binary functions  -/
uniformContinuous_sInf_dom₂ : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {f : α → β → γ} {uas : Set (UniformSpace α)} {ubs : Set (UniformSpace β)}
  {ua : UniformSpace α} {ub : UniformSpace β} {uc : UniformSpace γ},
  ua ∈ uas → ub ∈ ubs → (UniformContinuous fun p => f p.1 p.2) → UniformContinuous fun p => f p.1 p.2
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_inv_le_iff_of_neg : ∀ {x : NNReal} {z : ℝ} {y : NNReal}, 0 < x → 0 < y → z < 0 → (x ^ z⁻¹ ≤ y ↔ y ^ z ≤ x)
-- Mathlib.Analysis.Normed.Group.Basic
exists_enorm_lt' : ∀ (E : Type u_8) [inst : TopologicalSpace E] [inst_1 : ESeminormedMonoid E] [hbot : (nhdsWithin 1 {1}ᶜ).NeBot]
  {c : ENNReal}, c ≠ 0 → ∃ x, x ≠ 1 ∧ ‖x‖ₑ < c
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.getPPAnalyzeTrustId : Lean.Options → Bool
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go_get_aux : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (distance : ℕ)
  (input : aig.RefVec w) (curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr) (idx : ℕ) (hidx : idx < curr)
  (hfoo :
    aig.decls.size ≤
      (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go aig input distance curr hcurr s).aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go aig input distance curr hcurr s).vec.get idx ⋯ =
    (s.get idx hidx).cast hfoo
-- Mathlib.Dynamics.FixedPoints.Basic
Function.IsFixedPt.perm_pow : ∀ {α : Type u_1} {x : α} {e : Equiv.Perm α}, Function.IsFixedPt (⇑e) x → ∀ (n : ℕ), Function.IsFixedPt (⇑(e ^ n)) x
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.coe_mk : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (f : G → H)
  (hf : ∀ (x : G), f (x + a) = f x + b), ⇑{ toFun := f, map_add_const' := hf } = f
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.exists_lt_of_prod_lt' : ∀ {ι : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M] [MulRightMono M] [MulLeftMono M] {l : List ι}
  (f g : ι → M), (List.map f l).prod < (List.map g l).prod → ∃ i ∈ l, f i < g i
-- Aesop.Forward.PremiseIndex
Aesop.instDecidableEqPremiseIndex : DecidableEq Aesop.PremiseIndex
-- Aesop.RuleSet
/-- The simp theorems stored in this rule set.
 -/
Aesop.GlobalRuleSet.simpTheorems : Aesop.GlobalRuleSet → Lean.Meta.SimpTheorems
-- Init.Data.String.TakeDrop
String.trimLeft : String → String
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- If `f : M → N` is an additive monoid homomorphism, then `MonoidAlgebra.mapDomain f` is an
algebra homomorphism between their additive monoid algebras.  -/
AddMonoidAlgebra.mapDomainAlgHom : (R : Type u_1) →
  (A : Type u_4) →
    {M : Type u_7} →
      {N : Type u_8} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : AddMonoid M] →
                [inst_4 : AddMonoid N] → (M →+ N) → AddMonoidAlgebra A M →ₐ[R] AddMonoidAlgebra A N
-- Mathlib.SetTheory.ZFC.Rank
ZFSet.le_succ_rank_sUnion : ∀ (x : ZFSet.{u_1}), x.rank ≤ Order.succ x.sUnion.rank
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.cones_obj_obj : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] (C : Type u₃) [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) (X : Cᵒᵖ),
  ((CategoryTheory.cones J C).obj F).obj X = ((CategoryTheory.Functor.const J).obj (Opposite.unop X) ⟶ F)
-- Mathlib.Geometry.Convex.ConvexSpace.Module
Convexity.isConvexSet_coe : ∀ {F : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : SetLike F M]
  [AddSubmonoidClass F M] [SMulMemClass F R M] [inst_8 : Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M]
  (S : F), Convexity.IsConvexSet R ↑S
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k : α}, k ∉ m₂ → (m₁ \ m₂).getKey! k = m₁.getKey! k
-- Mathlib.Topology.Category.TopCat.Sphere
TopCat.instMonoBallInclusion : ∀ {n : ℕ}, CategoryTheory.Mono (TopCat.ballInclusion n)
-- Mathlib.Order.WithBot
WithBot.unbot_lt_iff : ∀ {α : Type u_1} {b : α} [inst : LT α] {x : WithBot α} (hx : x ≠ ⊥), x.unbot hx < b ↔ x < ↑b
-- Mathlib.Data.Set.Lattice
Set.iUnion_iUnion_eq_or_left : ∀ {α : Type u_1} {β : Type u_2} {b : β} {p : β → Prop} {s : (x : β) → x = b ∨ p x → Set α},
  ⋃ x, ⋃ (h : x = b ∨ p x), s x h = s b ⋯ ∪ ⋃ x, ⋃ (h : p x), s x ⋯
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
/-- Define a right action of `Cᴹᵒᵖ` on `D` from a left action of `C` on `D` via
the formula `d ⊙ᵣ mop c = c ⊙ₗ d`.  -/
CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction : (C : Type u_1) →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.MonoidalCategory C] →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            CategoryTheory.MonoidalCategory.MonoidalRightAction Cᴹᵒᵖ D
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pushforward_apply_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {R : CategoryTheory.Sieve Y} {Z : C} {g : Z ⟶ Y},
  R.arrows g → ∀ (f : Y ⟶ X), (CategoryTheory.Sieve.pushforward f R).arrows (CategoryTheory.CategoryStruct.comp g f)
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.ext_iff : ∀ {R : Type u_1} [inst : Zero R] {f g : ArithmeticFunction R}, f = g ↔ ∀ (x : ℕ), f x = g x
-- Init.Data.UInt.Lemmas
UInt64.ofNatClamp_toNat : ∀ (n : UInt64), UInt64.ofNatClamp n.toNat = n
-- Mathlib.Data.Seq.Computation
Computation.tail_pure : ∀ {α : Type u} (a : α), (Computation.pure a).tail = Computation.pure a
-- Mathlib.Data.Seq.Defs
/-- Remove the first `n` elements from the sequence.  -/
Stream'.Seq.drop : {α : Type u} → Stream'.Seq α → ℕ → Stream'.Seq α
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScott.instClosedIicTopologyOfUnivSet : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsScott α Set.univ], ClosedIicTopology α
-- Mathlib.Topology.Category.LightProfinite.Sequence
_private.Mathlib.Topology.Category.LightProfinite.Sequence.0.LightProfinite.natUnionInftyEmbedding.match_1.splitter : (motive : OnePoint ℕ → Sort u_1) → (x : OnePoint ℕ) → (Unit → motive none) → ((n : ℕ) → motive (some n)) → motive x
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.C_mul : ∀ {R : Type u_1} {a b : R} [inst : NonUnitalNonAssocSemiring R] (x y : R),
  QuadraticAlgebra.C (x * y) = QuadraticAlgebra.C x * QuadraticAlgebra.C y
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.eq_of_factors_eq_factors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a b : Associates α},
  a.factors = b.factors → a = b
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.restr_inter_source : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : Set X}, e.restr (e.source ∩ s) ≈ e.restr s
-- Init.Data.Array.GetLit
Array.toArrayLit_eq : ∀ {α : Type u_1} (xs : Array α) (n : ℕ) (hsz : xs.size = n), xs = xs.toArrayLit n hsz
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] [inst_1 : SizeOf C] (arrows : (c d : C) → Set (c ⟶ d))
  (inv : ∀ {c d : C} {p : c ⟶ d}, p ∈ arrows c d → CategoryTheory.Groupoid.inv p ∈ arrows d c)
  (mul :
    ∀ {c d e : C} {p : c ⟶ d},
      p ∈ arrows c d → ∀ {q : d ⟶ e}, q ∈ arrows d e → CategoryTheory.CategoryStruct.comp p q ∈ arrows c e),
  sizeOf { arrows := arrows, inv := inv, mul := mul } = 1
-- Mathlib.Analysis.Calculus.LogDeriv
logDeriv_comp : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f : 𝕜' → 𝕜'} {g : 𝕜 → 𝕜'} {x : 𝕜},
  DifferentiableAt 𝕜' f (g x) → DifferentiableAt 𝕜 g x → logDeriv (f ∘ g) x = logDeriv f (g x) * deriv g x
-- Mathlib.Analysis.Calculus.ImplicitFunction.Bivariate
tendsto_implicitFunctionOfBivariate : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : IsRCLikeNormedField 𝕜] {E₁ : Type u_2}
  [inst_2 : NormedAddCommGroup E₁] [inst_3 : NormedSpace 𝕜 E₁] [inst_4 : CompleteSpace E₁] {E₂ : Type u_3}
  [inst_5 : NormedAddCommGroup E₂] [inst_6 : NormedSpace 𝕜 E₂] [inst_7 : CompleteSpace E₂] {F : Type u_4}
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : CompleteSpace F] {u : E₁ × E₂} {f : E₁ → E₂ → F}
  {f₁ : E₁ → E₂ → E₁ →L[𝕜] F} {f₂ : E₁ → E₂ → E₂ →L[𝕜] F}
  (df₁ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun x => f x v.2) (f₁ v.1 v.2) v.1)
  (df₂ : ∀ᶠ (v : E₁ × E₂) in nhds u, HasFDerivAt (fun x => f v.1 x) (f₂ v.1 v.2) v.2) (cf₁ : ContinuousAt (↿f₁) u)
  (cf₂ : ContinuousAt (↿f₂) u) (if₂u : (f₂ u.1 u.2).IsInvertible),
  Filter.Tendsto (implicitFunctionOfBivariate df₁ df₂ cf₁ cf₂ if₂u) (nhds u.1) (nhds u.2)
-- Mathlib.Topology.EMetricSpace.Basic
/-- A sigma compact pseudo emetric space has second countable topology.  -/
EMetric.secondCountable_of_sigmaCompact : ∀ (α : Type u) [inst : PseudoEMetricSpace α] [SigmaCompactSpace α], SecondCountableTopology α
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.rightUnitor_hom_τr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b),
  (CategoryTheory.Bicategory.rightUnitor α).hom.τr = (CategoryTheory.Bicategory.leftUnitor α.r).inv
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RicSliceData.mk : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      (Std.DTreeMap.Internal.Impl α fun x => β) → Std.Ric α → Std.DTreeMap.Internal.Const.RicSliceData α β
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.subtypeRestr_symm_eqOn_of_le : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {U V : TopologicalSpace.Opens X} (hU : Nonempty ↥U) (hV : Nonempty ↥V) (hUV : U ≤ V),
  Set.EqOn (↑(e.subtypeRestr hV).symm) (Set.inclusion hUV ∘ ↑(e.subtypeRestr hU).symm) (e.subtypeRestr hU).target
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.out_eq' : ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (a : α ⧸ s), ↑(Quotient.out a) = a
-- Mathlib.Order.Filter.AtTopBot.Finite
Filter.strictMono_subseq_of_id_le : ∀ {u : ℕ → ℕ}, (∀ (n : ℕ), n ≤ u n) → ∃ φ, StrictMono φ ∧ StrictMono (u ∘ φ)
-- Init.Data.BitVec.Lemmas
BitVec.ofFin_neg : ∀ {w : ℕ} {x : Fin (2 ^ w)}, { toFin := -x } = -{ toFin := x }
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.Scheme.Modules.fromTildeΓ.eq_1 : ∀ {R : CommRingCat} (M : (AlgebraicGeometry.Spec (CommRingCat.of ↑R)).Modules),
  M.fromTildeΓ =
    AlgebraicGeometry.SpecModulesToSheafFullyFaithful.preimage
      {
        hom :=
          (TopCat.Sheaf.restrictHomEquivHom
              (AlgebraicGeometry.modulesSpecToSheaf.obj
                  (AlgebraicGeometry.tilde
                    ((AlgebraicGeometry.modulesSpecToSheaf.obj M).presheaf.obj (Opposite.op ⊤)))).obj
              (AlgebraicGeometry.modulesSpecToSheaf.obj M) ⋯)
            {
              app := fun f =>
                ModuleCat.ofHom
                  (IsLocalizedModule.lift (Submonoid.powers (Opposite.unop f))
                    (ModuleCat.Hom.hom
                      (AlgebraicGeometry.tilde.toOpen
                        ((AlgebraicGeometry.modulesSpecToSheaf.obj M).obj.obj (Opposite.op ⊤))
                        (PrimeSpectrum.basicOpen (Opposite.unop f))))
                    (ModuleCat.Hom.hom
                      ((AlgebraicGeometry.modulesSpecToSheaf.obj M).obj.map (CategoryTheory.homOfLE ⋯).op))
                    ⋯),
              naturality := ⋯ } }
-- Mathlib.Tactic.Positivity.Core
/-- An auxiliary entry point to the `positivity` tactic. Given a proposition `t` of the form
`0 [≤/</≠] e`, attempts to recurse on the structure of `t` to prove it. It returns a proof
or fails.  -/
Mathlib.Meta.Positivity.solve : Q(Prop) → Lean.MetaM Lean.Expr
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.map.eq_1 : ∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω']
  (ν : MeasureTheory.ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ↑ν),
  ν.map f_aemble = ⟨MeasureTheory.Measure.map f ↑ν, ⋯⟩
-- Mathlib.Data.List.Sigma
List.NodupKeys.eq_of_mk_mem : ∀ {α : Type u} {β : α → Type v} {a : α} {b b' : β a} {l : List (Sigma β)},
  l.NodupKeys → ⟨a, b⟩ ∈ l → ⟨a, b'⟩ ∈ l → b = b'
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.LaxMonoidalFunctor.isoMk_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F G : CategoryTheory.LaxMonoidalFunctor C D} (e : F.toFunctor ≅ G.toFunctor)
  [inst_4 : CategoryTheory.NatTrans.IsMonoidal e.hom],
  (CategoryTheory.LaxMonoidalFunctor.isoMk e).hom = CategoryTheory.LaxMonoidalFunctor.homMk e.hom
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- For a pair of functors `L : C ⥤ D`, `R : D ⥤ C`, an adjunction `h : L ⊣ R` induces a comonad on
the category `D`.
 -/
CategoryTheory.Adjunction.toComonad : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} → {R : CategoryTheory.Functor D C} → (L ⊣ R) → CategoryTheory.Comonad D
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.erase_eq_empty_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, t.erase k = ∅ ↔ t = ∅ ∨ t.size = 1 ∧ k ∈ t
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.one_apply : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (a : α), 1 a = a
-- Mathlib.MeasureTheory.Measure.Prod
/-- The product measure of the product of two sets is the product of their measures. Note that we
do not need the sets to be measurable.  -/
MeasureTheory.Measure.prod_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] (s : Set α) (t : Set β), (μ.prod ν) (s ×ˢ t) = μ s * ν t
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.isoMk₀_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 0}
  (e :
    F.obj' 0 CategoryTheory.ComposableArrows.homMk₀._proof_1 ≅ G.obj' 0 CategoryTheory.ComposableArrows.homMk₀._proof_1)
  (i : Fin (0 + 1)),
  (CategoryTheory.ComposableArrows.isoMk₀ e).hom.app i =
    match i with
    | ⟨0, isLt⟩ => e.hom
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.tuple.inj : ∀ {args args_1 : List Lean.Parser.Tactic.MCasesPat},
  Lean.Parser.Tactic.MCasesPat.tuple args = Lean.Parser.Tactic.MCasesPat.tuple args_1 → args = args_1
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.Hom.ext_iff : ∀ {R S : SemiRingCat} {x y : R.Hom S}, x = y ↔ x.hom' = y.hom'
-- Mathlib.Combinatorics.SimpleGraph.Sum
_private.Mathlib.Combinatorics.SimpleGraph.Sum.0.SimpleGraph.sum.match_1.eq_3 : ∀ {V : Type u_1} {W : Type u_2} (motive : V ⊕ W → V ⊕ W → Sort u_3) (x x_1 : V ⊕ W)
  (h_1 : (u v : V) → motive (Sum.inl u) (Sum.inl v)) (h_2 : (u v : W) → motive (Sum.inr u) (Sum.inr v))
  (h_3 : (x x_2 : V ⊕ W) → motive x x_2),
  (∀ (u v : V), x = Sum.inl u → x_1 = Sum.inl v → False) →
    (∀ (u v : W), x = Sum.inr u → x_1 = Sum.inr v → False) →
      (match x, x_1 with
        | Sum.inl u, Sum.inl v => h_1 u v
        | Sum.inr u, Sum.inr v => h_2 u v
        | x, x_4 => h_3 x x_4) =
        h_3 x x_1
-- Mathlib.Analysis.Distribution.Sobolev
TemperedDistribution.memSobolev_zero_iff_exists_fourier : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : InnerProductSpace ℂ F] [inst_7 : CompleteSpace F] {f : TemperedDistribution E F},
  TemperedDistribution.MemSobolev 0 2 f ↔ ∃ f', FourierTransform.fourier f = MeasureTheory.Lp.toTemperedDistribution f'
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.instBEqKey.beq : Lean.Meta.LazyDiscrTree.Key → Lean.Meta.LazyDiscrTree.Key → Bool
-- Mathlib.Algebra.Group.Units.Equiv
toAddUnits.eq_1 : ∀ {G : Type u_5} [inst : AddGroup G],
  toAddUnits =
    { toFun := fun x => { val := x, neg := -x, val_neg := ⋯, neg_val := ⋯ }, invFun := fun x => ↑x, left_inv := ⋯,
      right_inv := ⋯, map_add' := ⋯ }
-- Lean.Syntax
Lean.Syntax.antiquotSpliceKind? : Lean.Syntax → Option Lean.SyntaxNodeKind
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.l_inv_hom : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X : CategoryTheory.FreeMonoidalCategory C}, CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Mathlib.CategoryTheory.Subobject.Limits
/-- A factorisation of `h : W ⟶ X` through `kernelSubobject f`, assuming `h ≫ f = 0`.  -/
CategoryTheory.Limits.factorThruKernelSubobject : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Limits.HasKernel f] →
            {W : C} →
              (h : W ⟶ X) →
                CategoryTheory.CategoryStruct.comp h f = 0 →
                  (W ⟶ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f))
-- Mathlib.Algebra.Homology.Factorizations.CM5b
/-- The second projection `mappingCone (𝟙 (I K)) ⊞ L ⟶ L`.  -/
CochainComplex.cm5b.p : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.EnoughInjectives C] →
        (K L : CochainComplex C ℤ) →
          CochainComplex.mappingCone (CategoryTheory.CategoryStruct.id (CochainComplex.cm5b.I K)) ⊞ L ⟶ L
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.toRows₁_fromRows : ∀ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R),
  (A₁.fromRows A₂).toRows₁ = A₁
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.all_eq_forIn : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {p : β → Bool},
  Std.Iter.all p it =
    (forIn it true fun x x_1 => if p x = true then pure (ForInStep.yield true) else pure (ForInStep.done false)).run
-- Mathlib.Tactic.NormNum.Core
/-- The extension should be run in the `pre` phase when used as simp plugin.  -/
Mathlib.Meta.NormNum.NormNumExt.pre : Mathlib.Meta.NormNum.NormNumExt → Bool
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.getGE_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {h' : ∃ a ∈ t₁, (cmp a k).isGE = true} (h : t₁.Equiv t₂), t₁.getGE k h' = t₂.getGE k ⋯
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.insertMany_list_singleton : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, m.insertMany [k] = m.insert k
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- When `S.g = 0`, this is the canonical isomorphism `S.opcycles ≅ S.rightHomology` induced
by `S.rightHomologyι`.  -/
CategoryTheory.ShortComplex.opcyclesIsoRightHomology : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [inst_2 : S.HasRightHomology] → S.g = 0 → (S.opcycles ≅ S.rightHomology)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.Hom.mulAction.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] {X : C} [inst_3 : CategoryTheory.ModObj M X] (Z : C),
  CategoryTheory.Hom.mulAction Z = { toSMul := CategoryTheory.Hom.instSMulHom Z, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Tactic.Contrapose
Mathlib.Tactic.Contrapose.contrapose_iff₄ : ∀ {p q : Prop}, (p ↔ q) → (¬p ↔ ¬q)
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
/-- `yoneda` is dense: Every `X : Cᵒᵖ ⥤ Type v₁` is the colimit over
`CostructuredArrow.proj yoneda X ⋙ yoneda`.  -/
CategoryTheory.denseAtYoneda : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (X : CategoryTheory.Functor Cᵒᵖ (Type v₁)) → CategoryTheory.yoneda.DenseAt X
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.ιMulti_apply_coe : ∀ (R : Type u) [inst : CommRing R] (n : ℕ) {M : Type u_1} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (a : Fin n → M), ↑((exteriorPower.ιMulti R n) a) = (ExteriorAlgebra.ιMulti R n) a
-- Mathlib.Combinatorics.Hindman
/-- **Alias** of `Hindman.FP.finsetProd`. -/
Hindman.FP.finset_prod : ∀ {M : Type u_1} [inst : CommMonoid M] (a : Stream' M) (s : Finset ℕ), s.Nonempty → ∏ i ∈ s, a.get i ∈ Hindman.FP a
-- Mathlib.RingTheory.MvPowerSeries.Restricted
/-- A multivariate powe0r series over a normed ring `R` is restricted for a
tuple `c` if `‖coeff t f‖ * ∏ i ∈ t.support, c i ^ t i → 0` under the cofinite filter.  -/
MvPowerSeries.IsRestricted : {R : Type u_1} → [NormedRing R] → {σ : Type u_2} → (σ → ℝ) → MvPowerSeries σ R → Prop
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.eval : ∀ {Ω : Type u_1} {ι : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : ι → Type u_5}
  [inst : (i : ι) → NormedAddCommGroup (E i)] [inst_1 : (i : ι) → NormedSpace ℝ (E i)]
  [inst_2 : (i : ι) → MeasurableSpace (E i)] [∀ (i : ι), BorelSpace (E i)] {X : (i : ι) → Ω → E i},
  ProbabilityTheory.HasGaussianLaw (fun ω x => X x ω) P → ∀ (i : ι), ProbabilityTheory.HasGaussianLaw (X i) P
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.adjp_apply : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (s : ℤˣ)
  (A : Matrix n n R) (i j : n), Matrix.adjp s A i j = ∑ σ ∈ Equiv.Perm.ofSign s with σ j = i, ∏ k ∈ {j}ᶜ, A k (σ k)
-- Init.Data.Nat.Basic
Nat.succ_pred : ∀ {a : ℕ}, a ≠ 0 → a.pred.succ = a
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.instAddCommGroupWithOne : {R : Type u_1} → [AddCommGroupWithOne R] → AddCommGroupWithOne Rᵃᵒᵖ
-- Lean.Meta.Tactic.Ext
Lean.Meta.Ext.ExtTheorems.mk.sizeOf_spec : ∀ (tree : Lean.Meta.DiscrTree Lean.Meta.Ext.ExtTheorem) (erased : Lean.PHashSet Lean.Name),
  sizeOf { tree := tree, erased := erased } = 1 + sizeOf tree + sizeOf erased
-- Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
/-- This is the continuous version of `AlgEquiv.eq_linearEquivConjAlgEquiv`.  -/
ContinuousAlgEquiv.eq_continuousLinearEquivConjContinuousAlgEquiv : ∀ {𝕜 : Type u_1} {V : Type u_2} {W : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : SeminormedAddCommGroup W] [inst_3 : NormedSpace 𝕜 V] [inst_4 : NormedSpace 𝕜 W] [SeparatingDual 𝕜 V]
  [SeparatingDual 𝕜 W] (f : (V →L[𝕜] V) ≃A[𝕜] W →L[𝕜] W), ∃ U, f = U.conjContinuousAlgEquiv
-- Mathlib.Order.Atoms
Set.Ioi_eq_singleton_top_iff : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, Set.Ioi a = {⊤} ↔ IsCoatom a
-- Mathlib.CategoryTheory.Idempotents.Karoubi
/-- the condition that the given endomorphism is an idempotent  -/
CategoryTheory.Idempotents.Karoubi.idem : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (self : CategoryTheory.Idempotents.Karoubi C),
  CategoryTheory.CategoryStruct.comp self.p self.p = self.p