mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.equivOp.eq_1 : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup G), H.equivOp = AddOpposite.opEquiv.subtypeEquiv ⋯
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_pow_eq_pow_sum : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] (s : Finset ι) (f : ι → ℕ) (a : M),
  ∏ i ∈ s, a ^ f i = a ^ ∑ i ∈ s, f i
-- Mathlib.Computability.TuringMachine.Computable
Turing.inhabitedTM2ComputableAux : Inhabited (Turing.TM2ComputableAux Bool Bool)
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- An equivalence of finite domains induces a linearly isometric equivalence of finitely supported
functions.  -/
LinearIsometryEquiv.piLpCongrLeft : (p : ENNReal) →
  (𝕜 : Type u_1) →
    {ι : Type u_2} →
      [hp : Fact (1 ≤ p)] →
        [inst : Fintype ι] →
          [inst_1 : Semiring 𝕜] →
            {ι' : Type u_5} →
              [inst_2 : Fintype ι'] →
                (E : Type u_6) →
                  [inst_3 : SeminormedAddCommGroup E] →
                    [inst_4 : Module 𝕜 E] → ι ≃ ι' → (PiLp p fun x => E) ≃ₗᵢ[𝕜] PiLp p fun x => E
-- Mathlib.NumberTheory.Wilson
/-- For `n ≠ 1`, `(n-1)!` is congruent to `-1` modulo `n` only if n is prime.  -/
Nat.prime_of_fac_equiv_neg_one : ∀ {n : ℕ}, ↑(n - 1).factorial = -1 → n ≠ 1 → Nat.Prime n
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
ZMod.exponent : ∀ (n : ℕ), AddMonoid.exponent (ZMod n) = n
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncGEπ_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) {X Y : C} (f : X ⟶ Y) {Z : C} (h : (t.truncGE n).obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X)
      (CategoryTheory.CategoryStruct.comp ((t.truncGE n).map f) h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app Y) h)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.inhabited : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] → [inst_1 : Inhabited T] → Inhabited (CategoryTheory.Under default)
-- Mathlib.Algebra.Group.Defs
one_zsmul : ∀ {G : Type u_1} [inst : SubNegMonoid G] (a : G), 1 • a = a
-- Mathlib.Topology.Maps.Basic
Topology.isOpenEmbedding_iff_continuous_injective_isOpenMap : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsOpenEmbedding f ↔ Continuous f ∧ Function.Injective f ∧ IsOpenMap f
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Relation.below.map : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat}
  {motive : (a a_1 : MonCat.Colimits.Prequotient F) → MonCat.Colimits.Relation F a a_1 → Prop} (j j' : J) (f : j ⟶ j')
  (x : ↑(F.obj j)), MonCat.Colimits.Relation.below ⋯
-- Lean.Elab.Deriving.Basic
Lean.Elab.DerivingClassView.applyHandlers : Lean.Elab.DerivingClassView → Array Lean.Name → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.RingTheory.Bialgebra.Convolution
AlgHom.convOne_apply : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring C]
  [inst_3 : Bialgebra R C] [inst_4 : Algebra R A] (c : C),
  (WithConv.ofConv 1) c = (algebraMap R A) (CoalgebraStruct.counit c)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.isSuccLimit_add_iff_of_isSuccLimit : ∀ {a b : Ordinal.{u_4}}, Order.IsSuccLimit a → (Order.IsSuccLimit (a + b) ↔ Order.IsSuccPrelimit b)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.unop_φK : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (ψ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂), ψ.unop.φK = ψ.φQ.unop
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- `MonoidAlgebra.coeff` as an `AddEquiv`.  -/
MonoidAlgebra.coeffAddEquiv : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → MonoidAlgebra R M ≃+ (M →₀ R)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_alterKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k k' fallback : α}
  {f : Option (β k) → Option (β k)} (l : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKeyD k' (Std.Internal.List.alterKey k f l) fallback =
      if (k == k') = true then if (f (Std.Internal.List.getValueCast? k l)).isSome = true then k else fallback
      else Std.Internal.List.getKeyD k' l fallback
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- If `f` is an integrable periodic function with period `T`, then its integral over `[t, s + T]`
is the sum of its integrals over the intervals `[t, s]` and `[t, t + T]`.  -/
Function.Periodic.intervalIntegral_add_eq_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T : ℝ} [inst_1 : NormedSpace ℝ E],
  Function.Periodic f T →
    ∀ (t s : ℝ),
      (∀ (t₁ t₂ : ℝ), IntervalIntegrable f MeasureTheory.volume t₁ t₂) →
        ∫ (x : ℝ) in t..s + T, f x = (∫ (x : ℝ) in t..s, f x) + ∫ (x : ℝ) in t..t + T, f x
-- Mathlib.Analysis.Calculus.FDeriv.Const
fderivWithin_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {s : Set E}, fderivWithin 𝕜 0 s = 0
-- Mathlib.Topology.Defs.Filter
LocallyCompactPair.mk : ∀ {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  (∀ {f : X → Y} {x : X} {s : Set Y}, Continuous f → s ∈ nhds (f x) → ∃ K ∈ nhds x, IsCompact K ∧ Set.MapsTo f K s) →
    LocallyCompactPair X Y
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.instTypeNameTryThisInfo : TypeName Lean.Meta.Tactic.TryThis.TryThisInfo
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapDomain_comapDomain : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] {f : M → N} {x : MonoidAlgebra R N},
  ↑x.coeff.support ⊆ Set.range f →
    ∀ (hf : Function.Injective f), MonoidAlgebra.mapDomain f (MonoidAlgebra.comapDomain f hf x) = x
-- Mathlib.CategoryTheory.Shift.Localization
CategoryTheory.LocalizerMorphism.instCommShiftLocalizationHomFunctorIsoFunctorQLocalizedFunctor : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {M : Type u_3}
  [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C₁ M] [inst_4 : CategoryTheory.HasShift C₂ M]
  [inst_5 : Φ.functor.CommShift M] [inst_6 : W₁.IsCompatibleWithShift M] [inst_7 : W₂.IsCompatibleWithShift M],
  CategoryTheory.NatTrans.CommShift
    (CategoryTheory.CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).hom M
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α},
  cmp k k' = Ordering.eq → (k ∈ t ↔ k' ∈ t)
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
expNegInvGlue.monotone : Monotone expNegInvGlue
-- Init.Data.Int.Gcd
Int.gcd_mul_right_sub_right : ∀ (m n k : ℤ), m.gcd (k * m - n) = m.gcd n
-- Mathlib.Topology.Sequences
/-- If a set is equal to its sequential closure, then it is sequentially closed.  -/
isSeqClosed_of_seqClosure_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, seqClosure s = s → IsSeqClosed s
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
IsStrictlyPositive.add_nonneg : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a b : A},
  IsStrictlyPositive a → 0 ≤ b → IsStrictlyPositive (a + b)
-- Std.Async.System
Std.Async.System.instInhabitedCPUInfo.default : Std.Async.System.CPUInfo
-- Batteries.Util.ProofWanted
/-- Wrapper carrying the body of a *transparent* `def_wanted` (one given a `:= body`). Unlike the
empty `DefWanted`, it stores the value, so `❰foo❱` projects it back out and downstream definitional
equalities go through; but the placeholder still has type `DerivedWanted T`, not `T`, so it
cannot be used directly as an inhabitant of `T` — the intended access is via the `❰…❱` syntax,
which projects
the value back out. (`val` is `public`, so direct projection is possible, but `❰…❱` is what callers
should use.)  -/
DerivedWanted : Sort u → Sort (max 1 u)
-- Mathlib.GroupTheory.NoncommPiCoprod
MonoidHom.noncommPiCoprod_apply : ∀ {M : Type u_1} [inst : Monoid M] {ι : Type u_2} [inst_1 : Fintype ι] {N : ι → Type u_3}
  [inst_2 : (i : ι) → Monoid (N i)] (ϕ : (i : ι) → N i →* M)
  {hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)} (h : (i : ι) → N i),
  (MonoidHom.noncommPiCoprod ϕ hcomm) h = Finset.univ.noncommProd (fun i => (ϕ i) (h i)) ⋯
-- Init.Data.String.Search
/-- Returns the position of the beginning of the line that contains the position `pos`.

Lines are ended by `'\n'`, and the returned position is either `0 : String.Pos.Raw` or
immediately after a `'\n'` character.
 -/
String.findLineStart : String → String.Pos.Raw → String.Pos.Raw
-- Lean.Meta.Match.Basic
Lean.Meta.Match.MatcherResult.addMatcher : Lean.Meta.Match.MatcherResult → Lean.MetaM Unit
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Colex.isOrderedCancelAddMonoid : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → AddCommMonoid (α i)]
  [inst_2 : (i : ι) → PartialOrder (α i)] [∀ (i : ι), IsOrderedCancelAddMonoid (α i)],
  IsOrderedCancelAddMonoid (Colex (Π₀ (i : ι), α i))
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
_private.Mathlib.Analysis.BoxIntegral.Partition.Additive.0.Option.elim'.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Mathlib.Algebra.Group.Hom.Defs
map_comp_zero : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : Zero M] [inst_1 : Zero N] [inst_2 : FunLike F M N]
  [ZeroHomClass F M N] (f : F), ⇑f ∘ 0 = 0
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.monadMap_refl : ∀ {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}
  {f : {β : Type u} → m β → m β} {post : α → Pred} {epost : EPred} (x : m α),
  ⦃ Std.Internal.Do.wp (f x) post epost ⦄ monadMap f x ⦃ post; epost ⦄
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.comap.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {N : Type u_2} [inst_2 : AddGroup N]
  [inst_3 : TopologicalSpace N] (f : G →+ N) (hf : Continuous ⇑f) (H : OpenAddSubgroup N),
  OpenAddSubgroup.comap f hf H = { toAddSubgroup := AddSubgroup.comap f ↑H, isOpen' := ⋯ }
-- Mathlib.CategoryTheory.Functor.Category
/-- The associator for functors, a natural isomorphism `((F ⋙ G) ⋙ H) ≅ (F ⋙ (G ⋙ H))`.

(In fact, `iso.refl _` will work here, but it tends to make Lean slow later,
and it's usually best to insert explicit associators.)
 -/
CategoryTheory.Functor.associator : {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] →
            {E' : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] →
                (F : CategoryTheory.Functor C D) →
                  (G : CategoryTheory.Functor D E) →
                    (H : CategoryTheory.Functor E E') → (F.comp G).comp H ≅ F.comp (G.comp H)
-- Mathlib.NumberTheory.Height.MvPolynomial
finProdFinEquiv.eq_1 : ∀ {m n : ℕ},
  finProdFinEquiv =
    { toFun := fun x => ⟨↑x.2 + n * ↑x.1, ⋯⟩, invFun := fun x => (x.divNat, x.modNat), left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.instSup : {L : FirstOrder.Language} →
  {M : Type w} → [inst : L.Structure M] → {A : Set M} → {α : Type u₁} → Max (L.DefinableSet A α)
-- Mathlib.Probability.ProbabilityMassFunction.Binomial
/-- The binomial `PMF`: the probability of observing exactly `i` “heads” in a sequence of `n`
independent coin tosses, each having probability `p` of coming up “heads”.  -/
PMF.binomial : (p : NNReal) → p ≤ 1 → (n : ℕ) → PMF (Fin (n + 1))
-- Mathlib.LinearAlgebra.Lagrange
/-- This is the second barycentric form of the Lagrange interpolant.  -/
Lagrange.eval_interpolate_not_at_node' : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F)
  {x : F},
  Set.InjOn v ↑s →
    s.Nonempty →
      (∀ i ∈ s, x ≠ v i) →
        Polynomial.eval x ((Lagrange.interpolate s v) r) =
          (∑ i ∈ s, Lagrange.nodalWeight s v i * (x - v i)⁻¹ * r i) / ∑ i ∈ s, Lagrange.nodalWeight s v i * (x - v i)⁻¹
-- Init.Data.SInt.Lemmas
Int16.ofIntLE_int64ToInt : ∀ (x : Int64) {h₁ : Int16.minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ Int16.maxValue.toInt},
  Int16.ofIntLE x.toInt h₁ h₂ = x.toInt16
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (sieves : (X : C) → Set (CategoryTheory.Sieve X)) →
      (∀ (X : C), ⊤ ∈ sieves X) →
        (∀ ⦃X Y : C⦄ ⦃S : CategoryTheory.Sieve X⦄ (f : Y ⟶ X),
            S ∈ sieves X → CategoryTheory.Sieve.pullback f S ∈ sieves Y) →
          (∀ ⦃X : C⦄ ⦃S : CategoryTheory.Sieve X⦄,
              S ∈ sieves X →
                ∀ (R : CategoryTheory.Sieve X),
                  (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → CategoryTheory.Sieve.pullback f R ∈ sieves Y) → R ∈ sieves X) →
            CategoryTheory.GrothendieckTopology C
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.BuilderOption.transparency.sizeOf_spec : ∀ (md : Lean.Meta.TransparencyMode) (alsoForIndex : Bool),
  sizeOf (Aesop.Frontend.BuilderOption.transparency md alsoForIndex) = 1 + sizeOf md + sizeOf alsoForIndex
-- Mathlib.Condensed.Discrete.Colimit
/-- Auxiliary definition for `isoFinYoneda`.  -/
Condensed.isoFinYonedaComponents : (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) →
  [CategoryTheory.Limits.PreservesFiniteProducts F] →
    (X : Profinite) →
      [Finite ↑X.toTop] → F.obj (Opposite.op X) ≅ ↑X.toTop → F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))
-- Lean.Elab.PreDefinition.FixedParams
/-- Brings the fixed parameters from `type`, which should be the type of the `funIdx`'s function, into
scope.
 -/
_private.Lean.Elab.PreDefinition.FixedParams.0.Lean.Elab.FixedParamPerm.forallTelescopeImpl : {α : Type} → Lean.Elab.FixedParamPerm → Lean.Expr → (Array Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_iff_of_isLocalizedEquivalence : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₁' : CategoryTheory.MorphismProperty D₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  {W₂' : CategoryTheory.MorphismProperty D₂} {T : CategoryTheory.LocalizerMorphism W₁ W₂}
  {L : CategoryTheory.LocalizerMorphism W₁ W₁'} {R : CategoryTheory.LocalizerMorphism W₂ W₂'}
  {B : CategoryTheory.LocalizerMorphism W₁' W₂'} [W₂'.RespectsIso] [L.IsLocalizedEquivalence] [R.IsLocalizedEquivalence]
  [R.functor.EssSurj] [L.functor.EssSurj] [R.functor.Full] [R.IsInduced]
  (iso : T.functor.comp R.functor ≅ L.functor.comp B.functor) [CategoryTheory.TwoSquare.GuitartExact iso.hom],
  T.IsRightDerivabilityStructure ↔ B.IsRightDerivabilityStructure
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.Rel.below.smul : ∀ {R : Type u} {X : Type v} [inst : CommRing R]
  {motive : (a a_1 : FreeNonUnitalNonAssocAlgebra R X) → FreeLieAlgebra.Rel R X a a_1 → Prop} (t : R)
  {a b : FreeNonUnitalNonAssocAlgebra R X} (a_1 : FreeLieAlgebra.Rel R X a b),
  FreeLieAlgebra.Rel.below a_1 → motive a b a_1 → FreeLieAlgebra.Rel.below ⋯
-- Mathlib.Analysis.Fourier.FourierTransform
VectorFourier.fourierIntegral_congr_ae : ∀ {𝕜 : Type u_1} [inst : CommRing 𝕜] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : MeasurableSpace V] {W : Type u_3} [inst_4 : AddCommGroup W] [inst_5 : Module 𝕜 W] {E : Type u_4}
  [inst_6 : NormedAddCommGroup E] [inst_7 : NormedSpace ℂ E] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure V)
  (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) {f₁ f₂ : V → E},
  f₁ =ᵐ[μ] f₂ → VectorFourier.fourierIntegral e μ L f₁ = VectorFourier.fourierIntegral e μ L f₂
-- Init.Tactics
/-- Implementation of `norm_cast` (the full `norm_cast` calls `trivial` afterwards).  -/
Lean.Parser.Tactic.normCast0 : Lean.ParserDescr
-- Mathlib.ModelTheory.Fraisse
FirstOrder.Language.IsFraisse.hereditary : ∀ {L : FirstOrder.Language} {K : Set (CategoryTheory.Bundled L.Structure)} [self : FirstOrder.Language.IsFraisse K],
  FirstOrder.Language.Hereditary K
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey!_eq_getElem!_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.minKey! = t.keysArray[0]!
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extendOpcyclesIso.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {j : ι} {j' : ι'}
  (hj' : e.f j = j') [inst_3 : K.HasHomology j] [inst_4 : (K.extend e).HasHomology j'],
  K.extendOpcyclesIso e hj' = K.extendOpcyclesIso e hj'
-- Mathlib.Tactic.NormNum.Inv
/-- The `norm_num` extension which identifies expressions of the form `mkRat a b`,
such that `norm_num` successfully recognises both `a` and `b`, and returns `a / b`.  -/
Mathlib.Meta.NormNum.evalMkRat : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.lift_def : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] (F : M →* A), ⇑((MonoidAlgebra.lift R A M) F) = ⇑(MonoidAlgebra.liftNC ↑(algebraMap R A) ⇑F)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.le_chromaticNumber_iff_colorable : ∀ {V : Type u} {G : SimpleGraph V} {n : ℕ}, ↑n ≤ G.chromaticNumber ↔ ∀ (m : ℕ), G.Colorable m → n ≤ m
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.inv_hom_id_tensor_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) {Z_1 : C} (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj W Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.inv g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom h) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id W) g)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id W) h) h_1)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_add_right' : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddGroup α] {t : Finset α} {b : α},
  Finset.image (fun x => x + -b) t = t.preimage (fun x => x + b) ⋯
-- Mathlib.MeasureTheory.Covering.VitaliFamily
/-- Consider a (possibly non-measurable) set `s`,
and for any `x` in `s` a subfamily `f x` of `setsAt x`
containing sets of arbitrarily small diameter.
Then one can extract a disjoint subfamily covering almost all `s`.  -/
VitaliFamily.covering : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (self : VitaliFamily μ) (s : Set X) (f : X → Set (Set X)),
  (∀ x ∈ s, f x ⊆ self.setsAt x) →
    (∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ Metric.closedBall x ε) →
      ∃ t, (∀ p ∈ t, p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p => p.2) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0
-- Mathlib.FieldTheory.Perfect
PerfectField.separable_iff_squarefree : ∀ {K : Type u_1} [inst : Field K] [PerfectField K] {g : Polynomial K}, g.Separable ↔ Squarefree g
-- Lean.Elab.Coinductive
/-- Declaration name of the predicate -/
Lean.Elab.Command.CoinductiveElabData.declName : Lean.Elab.Command.CoinductiveElabData → Lean.Name
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.map.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) (H : AddSubgroup G),
  AddSubgroup.map f H = { carrier := ⇑f '' ↑H, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
-- Mathlib.Computability.Primrec.Basic
Primrec.nat_iterate : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {f : α → ℕ} {g : α → β} {h : α → β → β},
  Primrec f → Primrec g → Primrec₂ h → Primrec fun a => (h a)^[f a] (g a)
-- Init.Data.Vector.Lemmas
Vector.insertIdx!_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} {h : xs.size = n} {i : ℕ} {x : α} (hi : i ≤ n),
  (Vector.mk xs h).insertIdx! i x = Vector.mk (xs.insertIdx i x ⋯) ⋯
-- Mathlib.Data.PNat.Prime
PNat.Coprime.coprime_dvd_left : ∀ {m k n : ℕ+}, m ∣ k → k.Coprime n → m.Coprime n
-- Mathlib.Analysis.Convex.Segment
openSegment_translate_image : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [AddRightMono 𝕜] [inst_3 : AddCommGroup E]
  [inst_4 : Module 𝕜 E] (a b c : E), (fun x => a + x) '' openSegment 𝕜 b c = openSegment 𝕜 (a + b) (a + c)
-- Mathlib.Combinatorics.Hindman
Hindman.exists_FP_of_large : ∀ {M : Type u_1} [inst : Semigroup M] (U : Ultrafilter M), U * U = U → ∀ s₀ ∈ U, ∃ a, Hindman.FP a ⊆ s₀
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_le_size_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, t.size ≤ (t.insert k v).size
-- Init.Classical
Classical.imp_and_neg_imp_iff : ∀ (p : Prop) {q : Prop}, (p → q) ∧ (¬p → q) ↔ q
-- Mathlib.Analysis.Normed.Module.WeakDual
WeakDual.seminormFamily_apply : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (x : E) (f : WeakDual 𝕜 E), (WeakDual.seminormFamily 𝕜 E x) f = ‖f x‖
-- Mathlib.Topology.Algebra.Monoid
/-- If the action of `R` on `A` commutes with left-addition, then
continuous addition implies continuous affine addition by constants.

Notably, this instance applies when `R = Aᵃᵒᵖ`.  -/
VAddCommClass.continuousConstVAdd : ∀ {R : Type u_6} {A : Type u_7} [inst : AddMonoid A] [inst_1 : VAdd R A] [VAddCommClass R A A]
  [inst_3 : TopologicalSpace A] [SeparatelyContinuousAdd A], ContinuousConstVAdd R A
-- Mathlib.Geometry.Convex.ConvexSpace.Module
/-- `convexCombPair` in a module can be expressed as a sum.  -/
Convexity.convexCombPair_eq_sum : ∀ {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 : Convexity.ConvexSpace R M]
  [Convexity.IsModuleConvexSpace R M] (a b : R) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (x y : M),
  Convexity.convexCombPair a b ha hb hab x y = a • x + b • y
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicFrontier.eq_1 : ∀ (𝕜 : Type u_1) {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] (s : Set P),
  intrinsicFrontier 𝕜 s = Subtype.val '' frontier (Subtype.val ⁻¹' s)