mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_sub_const_Ioo : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => x - a) '' Set.Ioo b c = Set.Ioo (b - a) (c - a)
-- Mathlib.AlgebraicGeometry.Cover.Open
/-- The open cover associated to an affine open cover.  -/
AlgebraicGeometry.Scheme.AffineOpenCover.openCover : {X : AlgebraicGeometry.Scheme} → X.AffineOpenCover → X.OpenCover
-- Mathlib.MeasureTheory.Measure.MeasuredSets
MeasureTheory.MeasuredSets.lipschitzWith_measureReal : ∀ {α : Type u_1} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ],
  LipschitzWith 1 fun s => μ.real ↑s
-- Lean.Parser.Term
Lean.Parser.Term.dynamicQuot.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_hom_comp_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) [inst_2 : S.HasRightHomology],
  CategoryTheory.CategoryStruct.comp h.rightHomologyIso.hom h.ι =
    CategoryTheory.CategoryStruct.comp S.rightHomologyι h.opcyclesIso.hom
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.centralizer_toSubalgebra : ∀ (R : Type u_2) {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (s : Set A),
  (StarSubalgebra.centralizer R s).toSubalgebra = Subalgebra.centralizer R (s ∪ star s)
-- Init.Data.List.Pairwise
List.Pairwise.iff_of_mem : ∀ {α : Type u_1} {R S : α → α → Prop} {l : List α},
  (∀ {a b : α}, a ∈ l → b ∈ l → (R a b ↔ S a b)) → (List.Pairwise R l ↔ List.Pairwise S l)
-- Lean.Elab.Binders
Lean.Elab.Term.quoteAutoTactic : Lean.Syntax → Lean.CoreM Lean.Expr
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.centralizer_closure : ∀ {G : Type u_1} [inst : Group G] (s : Set G), Subgroup.centralizer ↑(Subgroup.closure s) = Subgroup.centralizer s
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- An additive action is `1`-pretransitive iff it is pretransitive.  -/
AddAction.zeroEmbedding_isPretransitive_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {zero : Type u_5} [Unique zero],
  AddAction.IsPretransitive G (zero ↪ α) ↔ AddAction.IsPretransitive G α
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccLimit.withTopCoe : ∀ {α : Type u_1} [inst : Preorder α] {x : α}, Order.IsSuccLimit x → Order.IsSuccLimit ↑x
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.coeff_zero : ∀ (p n : ℕ) (R : Type u_1) [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (i : Fin n),
  TruncatedWittVector.coeff i 0 = 0
-- Mathlib.Analysis.Real.Sqrt
NNReal.sqrt_eq_one : ∀ {x : NNReal}, NNReal.sqrt x = 1 ↔ x = 1
-- Init.Data.List.Lemmas
List.nil_beq_eq : ∀ {α : Type u_1} [inst : BEq α] {l : List α}, ([] == l) = l.isEmpty
-- Lean.Meta.Tactic.Injection
Lean.Meta.InjectionsResult.subgoal.sizeOf_spec : ∀ (mvarId : Lean.MVarId) (remainingNames : List Lean.Name) (forbidden : Lean.FVarIdSet),
  sizeOf (Lean.Meta.InjectionsResult.subgoal mvarId remainingNames forbidden) =
    1 + sizeOf mvarId + sizeOf remainingNames + sizeOf forbidden
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- **Alias** of `Set.image_finsetSum`. -/
Set.image_finset_sum : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [inst : FunLike F α β] [inst_1 : AddCommMonoid α]
  [inst_2 : AddCommMonoid β] [AddMonoidHomClass F α β] (f : F) (m : Finset ι) (s : ι → Set α),
  ⇑f '' ∑ i ∈ m, s i = ∑ i ∈ m, ⇑f '' s i
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.subtypeMop_apply : ∀ {R : Type u_1} [inst : Ring R] (I : TwoSidedIdeal R) (x : ↥I), I.subtypeMop x = MulOpposite.op ↑x
-- Mathlib.Order.Disjoint
Complementeds.mk_inf_mk : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {a b : α} (ha : IsComplemented a)
  (hb : IsComplemented b), ⟨a, ha⟩ ⊓ ⟨b, hb⟩ = ⟨a ⊓ b, ⋯⟩
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.ι_descMapObj_assoc : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  (X : CategoryTheory.GradedObject I C) (p : I → J) [inst_1 : X.HasMap p] {A : C} {j : J}
  (φ : (i : I) → p i = j → (X i ⟶ A)) (i : I) (hi : p i = j) {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hi) (CategoryTheory.CategoryStruct.comp (X.descMapObj p φ) h) =
    CategoryTheory.CategoryStruct.comp (φ i hi) h
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
/-- If `c` is a colimit cocone on `G : Grothendieck F ⥤ H`, then the induced cocone on the
fiberwise colimit on `G` is a colimit cocone, too.  -/
CategoryTheory.Limits.isColimitCoconeFiberwiseColimitOfCocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      {H : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} H] →
          {G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H} →
            [inst_2 :
                ∀ {X Y : C} (f : X ⟶ Y),
                  CategoryTheory.Limits.HasColimit
                    ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] →
              {c : CategoryTheory.Limits.Cocone G} →
                CategoryTheory.Limits.IsColimit c →
                  CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeFiberwiseColimitOfCocone c)
-- Mathlib.Analysis.SpecialFunctions.Pow.Integral
MeasureTheory.integrableOn_ball_of_norm_le_rpow : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] [inst_5 : NormedAddCommGroup F] {μ : MeasureTheory.Measure E}
  [μ.IsAddHaarMeasure],
  1 ≤ Module.finrank ℝ E →
    ∀ {f : E → F} {C α r : ℝ},
      α < ↑(Module.finrank ℝ E) →
        (∀ᵐ (x : E) ∂μ.restrict (Metric.ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)) →
          MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.IntegrableOn f (Metric.ball 0 r) μ
-- Mathlib.Algebra.Ring.Semireal.Defs
IsSemireal.mk : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] [inst_2 : One R] [inst_3 : Zero R],
  (∀ {s : R}, IsSumSq s → 1 + s ≠ 0) → IsSemireal R
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Three
_private.Mathlib.NumberTheory.NumberField.Cyclotomic.Three.0.IsCyclotomicExtension.Rat.Three.«termλ» : Lean.ParserDescr
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Set.algebraMap_mem_centralizer : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A} (r : R),
  (algebraMap R A) r ∈ s.centralizer
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.uniqueBaseOn_inter_ground_eq : ∀ {α : Type u_1} (I E : Set α), Matroid.uniqueBaseOn (I ∩ E) E = Matroid.uniqueBaseOn I E
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- A version of `liftExpand` used to simultaneously lift functions with two arguments.  -/
AddOreLocalization.lift₂Expand : {R : Type u_1} →
  [inst : AddMonoid R] →
    {S : AddSubmonoid R} →
      [inst_1 : AddOreLocalization.AddOreSet S] →
        {X : Type u_3} →
          [inst_2 : AddAction R X] →
            {C : Sort u_2} →
              (P : X → ↥S → X → ↥S → C) →
                (∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ + ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ + ↑s₂ ∈ S),
                    P r₁ s₁ r₂ s₂ = P (t₁ +ᵥ r₁) ⟨t₁ + ↑s₁, ht₁⟩ (t₂ +ᵥ r₂) ⟨t₂ + ↑s₂, ht₂⟩) →
                  AddOreLocalization S X → AddOreLocalization S X → C
-- Mathlib.ModelTheory.Topology.Types
CompleteType.instTotallySeparatedSpaceCompleteType : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type u_1}, TotallySeparatedSpace (T.CompleteType α)
-- Mathlib.AlgebraicTopology.SimplicialSet.Subdivision
SSet.instIsLeftKanExtensionSimplexCategorySdInvFunctorSdIso : SSet.sd.IsLeftKanExtension SSet.stdSimplex.sdIso.inv
-- Mathlib.Data.TypeVec
TypeVec.id_comp : ∀ {n : ℕ} {α : TypeVec.{u} n} {β : TypeVec.{v} n} (f : α.Arrow β), TypeVec.comp TypeVec.id f = f
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.add_le_add_iff_left : ∀ {α : Type u} [inst : Add α] {x y z : WithBot α} [inst_1 : LE α] [AddLeftMono α] [AddLeftReflectLE α],
  x ≠ ⊥ → (x + y ≤ x + z ↔ y ≤ z)
-- Mathlib.Order.GameAdd
/-- `Prod.RProd` is a subrelation of the transitive closure of `Prod.GameAdd`.  -/
Prod.rprod_le_transGen_gameAdd : ∀ {α : Type u_1} {β : Type u_2} (rα : α → α → Prop) (rβ : β → β → Prop),
  Prod.RProd rα rβ ≤ Relation.TransGen (Prod.GameAdd rα rβ)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instRightCancelMonoidOfMulOpposite : {M : Type u_1} → [RightCancelMonoid Mᵐᵒᵖ] → RightCancelMonoid Mᵈᵐᵃ
-- Mathlib.Lean.Meta.CongrTheorems
/-- A version of `IsEmpty` with few instances. It should fail fast.  -/
Lean.Meta.FastIsEmpty : Sort u → Prop
-- Mathlib.Data.WSeq.Basic
/-- Compute for one tick, without producing any elements  -/
Stream'.WSeq.think : {α : Type u} → Stream'.WSeq α → Stream'.WSeq α
-- Mathlib.RingTheory.Derivation.Basic
Derivation.coe_smul : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] {S : Type u_5}
  [inst_6 : Monoid S] [inst_7 : DistribMulAction S M] [inst_8 : SMulCommClass R S M] [inst_9 : SMulCommClass S A M]
  (r : S) (D : Derivation R A M), ⇑(r • D) = r • ⇑D
-- Mathlib.CategoryTheory.Subobject.NoetherianObject
/-- An object `X` in a category `C` is Noetherian if `Subobject X`
satisfies the ascending chain condition.  -/
CategoryTheory.IsNoetherianObject : {C : Type u} → [CategoryTheory.Category.{v, u} C] → C → Prop
-- Init.Data.Nat.Basic
Nat.lt.step : ∀ {n m : ℕ}, n < m → n < m.succ
-- Init.Data.Vector.Lemmas
Vector.findSomeM?_toArray : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [inst : Monad m] {f : α → m (Option β)}
  {xs : Vector α n}, Array.findSomeM? f xs.toArray = Vector.findSomeM? f xs
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedCategory.assoc : ∀ {V : Type v} {inst : CategoryTheory.Category.{w, v} V} {inst_1 : CategoryTheory.MonoidalCategory V} {C : Type u₁}
  [self : CategoryTheory.EnrichedCategory V C] (W X Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (W ⟶[V] X) (X ⟶[V] Y) (Y ⟶[V] Z)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.EnrichedCategory.comp W X Y) (Y ⟶[V] Z))
        (CategoryTheory.EnrichedCategory.comp W Y Z)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (W ⟶[V] X) (CategoryTheory.EnrichedCategory.comp X Y Z))
      (CategoryTheory.EnrichedCategory.comp W X Z)
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₃ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Preadditive C] [inst_6 : CategoryTheory.Preadditive D] [inst_7 : F.Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (F.mapTriangleRotateIso.hom.app X).hom₃ = (CategoryTheory.Functor.commShiftIso F 1).inv.app X.obj₁
-- Init.Data.Dyadic.Basic
Dyadic.roundUp_eq_neg_roundDown_neg : ∀ (x : Dyadic) (prec : ℤ), x.roundUp prec = -(-x).roundDown prec
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.BasisExtension.nil.sizeOf_spec : sizeOf Tactic.ComputeAsymptotics.BasisExtension.nil = 1
-- Mathlib.Algebra.GroupWithZero.Action.Hom
ZeroHom.instIsScalarTower : ∀ {M : Type u_1} {N : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Zero A] [inst_1 : Zero B] [inst_2 : SMul M N]
  [inst_3 : SMulZeroClass M B] [inst_4 : SMulZeroClass N B] [IsScalarTower M N B], IsScalarTower M N (ZeroHom A B)
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.waitForWatchdogILeans : optParam Lean.JsonRpc.RequestID 0 → Lean.Lsp.Ipc.IpcM Unit
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.eRank_diagonal : ∀ {m : Type um} {R : Type uR} [inst : Field R] [inst_1 : DecidableEq m] (w : m → R),
  (Matrix.diagonal w).eRank = {i | w i ≠ 0}.encard
-- Mathlib.Algebra.Algebra.Opposite
AlgHom.op_apply_apply : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (a : Aᵐᵒᵖ),
  (AlgHom.op f) a = MulOpposite.op (f (MulOpposite.unop a))
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.image.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} [inst_1 : CategoryTheory.Limits.HasImages C],
  CategoryTheory.MonoOver.image = CategoryTheory.MonoOver.image
-- Aesop.RuleTac.ElabRuleTerm
Aesop.elabRuleTermForApplyLikeCore : Lean.MVarId → Lean.Term → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.Functor.flip_obj_map : ∀ {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 : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (k : D) {X Y : C} (f : X ⟶ Y),
  (F.flip.obj k).map f = (F.map f).app k
-- Mathlib.Topology.Category.LightProfinite.Extend
/-- Given a functor `G` from `LightProfiniteᵒᵖ` and `S : LightProfinite`, we obtain a cocone on
`(CostructuredArrow.proj toLightProfinite.op ⟨S⟩ ⋙ toLightProfinite.op ⋙ G)` with cocone point
`G.obj ⟨S⟩`.

Whiskering this cocone with `LightProfinite.Extend.functorOp c` gives `G.mapCocone c.op` as we
check in the example below.
 -/
LightProfinite.Extend.cocone : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (G : CategoryTheory.Functor LightProfiniteᵒᵖ C) →
      (S : LightProfinite) →
        CategoryTheory.Limits.Cocone
          ((CategoryTheory.CostructuredArrow.proj FintypeCat.toLightProfinite.op (Opposite.op S)).comp
            (FintypeCat.toLightProfinite.op.comp G))
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.IsReflection.isReflection_inv : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {t : W},
  cs.IsReflection t → cs.IsReflection t⁻¹
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_alter_of_beq_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α} {f : Option β → Option β}, (k == k') = false → (k' ∈ m.alter k f ↔ k' ∈ m)
-- Mathlib.Order.ConditionallyCompletePartialOrder.Defs
DirectedOn.le_csSup : ∀ {α : Type u_2} [inst : ConditionallyCompletePartialOrderSup α] {s : Set α} {a : α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) s → BddAbove s → a ∈ s → a ≤ sSup s
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Preconnected.mono : ∀ {V : Type u} {G G' : SimpleGraph V}, G ≤ G' → G.Preconnected → G'.Preconnected
-- Lean.Elab.Parallel
/-- Runs a list of TacticM computations in parallel and collects results in the original order,
including the saved state after each task completes.

Unlike `parIter`, this waits for all tasks to complete and returns results
in the same order as the input list, not in completion order.

Results are wrapped in `Except Exception (α × Tactic.SavedState)` so that errors in individual
tasks don't stop the collection - you can observe all results including which tasks failed.

The final TacticM state is restored to the initial state (before tasks ran).
 -/
Lean.Elab.Tactic.TacticM.par : {α : Type} →
  List (Lean.Elab.Tactic.TacticM α) →
    Lean.Elab.Tactic.TacticM (List (Except Lean.Exception (α × Lean.Elab.Tactic.SavedState)))
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.instUniqueHomInitial : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → {f : X ⟶ Y} → (d : CategoryTheory.Factorisation f) → Unique (CategoryTheory.Factorisation.initial ⟶ d)
-- Mathlib.Analysis.LocallyConvex.Bounded
/-- [Bourbaki, *Topological Vector Spaces*, III §1.6][bourbaki1987]  -/
isCompact_closure_of_totallyBounded_quasiComplete : ∀ {E : Type u_8} {𝕜 : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : UniformSpace E] [IsUniformAddGroup E] [ContinuousSMul 𝕜 E] [QuasiCompleteSpace 𝕜 E] {s : Set E},
  TotallyBounded s → IsCompact (closure s)
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.instDistribLatticeCarrier : (X : FinBddDistLat) → DistribLattice ↑X.toDistLat
-- Mathlib.Analysis.Fourier.FourierTransform
/-- The 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`.  -/
VectorFourier.integral_bilin_fourierIntegral_eq_flip : ∀ {𝕜 : 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}
  {F : Type u_5} {G : Type u_6} [inst_6 : NormedAddCommGroup E] [inst_7 : NormedSpace ℂ E]
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace ℂ F] [inst_10 : NormedAddCommGroup G]
  [inst_11 : NormedSpace ℂ G] [inst_12 : TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] [inst_14 : TopologicalSpace V]
  [BorelSpace V] [inst_16 : TopologicalSpace W] [inst_17 : MeasurableSpace W] [BorelSpace W] {e : AddChar 𝕜 Circle}
  {μ : MeasureTheory.Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} {ν : MeasureTheory.Measure W} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν] [SecondCountableTopologyEither W V] [CompleteSpace E] [CompleteSpace F] {f : V → E}
  {g : W → F} (M : E →L[ℂ] F →L[ℂ] G),
  Continuous ⇑e →
    (Continuous fun p => (L p.1) p.2) →
      MeasureTheory.Integrable f μ →
        MeasureTheory.Integrable g ν →
          ∫ (ξ : W), (M (VectorFourier.fourierIntegral e μ L f ξ)) (g ξ) ∂ν =
            ∫ (x : V), (M (f x)) (VectorFourier.fourierIntegral e ν L.flip g x) ∂μ
-- Mathlib.Logic.Equiv.Fin.Rotate
coe_finRotate_of_ne_last : ∀ {n : ℕ} {i : Fin n.succ}, i ≠ Fin.last n → ↑((finRotate (n + 1)) i) = ↑i + 1
-- Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
AddMonoidAlgebra.instNoZeroDivisorsOfUniqueSums : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [NoZeroDivisors R] [inst_2 : Add A] [UniqueSums A],
  NoZeroDivisors (AddMonoidAlgebra R A)
-- Mathlib.Data.EReal.Operations
_private.Mathlib.Data.EReal.Operations.0.EReal.exists_lt_add_left : ∀ {a b c : EReal}, c < a + b → ∃ a' < a, c < a' + b
-- Mathlib.Analysis.Calculus.FDeriv.Prod
fderiv_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {ι : Type u_6} {F' : ι → Type u_7} [inst_3 : (i : ι) → NormedAddCommGroup (F' i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i},
  DifferentiableAt 𝕜 Φ x → ∀ (i : ι), fderiv 𝕜 (fun x => Φ x i) x = ContinuousLinearMap.proj i ∘SL fderiv 𝕜 Φ x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey_alter_eq_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β} {he : (t.alter k f).isEmpty = false},
  (t.alter k f).maxKey he = k ↔ (f t[k]?).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.laverage_one : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [NeZero μ],
  ⨍⁻ (_x : α), 1 ∂μ = 1
-- Mathlib.Topology.PartitionOfUnity
/-- The partition of unity defined by a `BumpCovering`.

The partition of unity is given by the formula `g i x = f i x * ∏ᶠ j < i, (1 - f j x)`. In other
words, `g i x = ∏ᶠ j < i, (1 - f j x) - ∏ᶠ j ≤ i, (1 - f j x)`, so
`∑ᶠ i, g i x = 1 - ∏ᶠ j, (1 - f j x)`. If `x ∈ s`, then one of `f j x` equals one, hence the product
of `1 - f j x` vanishes, and `∑ᶠ i, g i x = 1`.

In order to avoid an assumption `LinearOrder ι`, we use `WellOrderingRel` instead of `(<)`.  -/
BumpCovering.toPartitionOfUnity : {ι : Type u} → {X : Type v} → [inst : TopologicalSpace X] → {s : Set X} → BumpCovering ι X s → PartitionOfUnity ι X s
-- Mathlib.RingTheory.Coprime.Basic
isCoprime_group_smul : ∀ {R : Type u_1} {G : Type u_2} [inst : CommSemiring R] [inst_1 : Group G] [inst_2 : MulAction G R]
  [SMulCommClass G R R] [IsScalarTower G R R] (x : G) (y z : R), IsCoprime (x • y) (x • z) ↔ IsCoprime y z
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
iteratedDeriv_exp_const_mul : ∀ (n : ℕ) (c : ℝ), (iteratedDeriv n fun s => Real.exp (c * s)) = fun s => c ^ n * Real.exp (c * s)
-- Mathlib.Topology.Covering.Basic
IsCoveringMapOn.homeomorph_comp_iff : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {s : Set X}
  {Y : Type u_3} [inst_2 : TopologicalSpace Y] (g : X ≃ₜ Y),
  IsCoveringMapOn (⇑g ∘ f) (⇑g.symm ⁻¹' s) ↔ IsCoveringMapOn f s
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- Multiplicativity of a continuous alternating map along all coordinates at the same time,
writing `f (fun i ↦ c i • m i)` as `(∏ i, c i) • f m`.  -/
ContinuousAlternatingMap.map_smul_univ : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [inst_7 : Fintype ι] (c : ι → R) (m : ι → M),
  (f fun i => c i • m i) = (∏ i, c i) • f m
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The inclusion of the cycles of a homological complex.  -/
HomologicalComplex.iCycles : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} → (K : HomologicalComplex C c) → (i : ι) → [inst_2 : K.HasHomology i] → K.cycles i ⟶ K.X i
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.BiconeHom.diagram.inj : ∀ {J : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} J} {j k : J} {f f_1 : j ⟶ k},
  CategoryTheory.BiconeHom.diagram f = CategoryTheory.BiconeHom.diagram f_1 → f = f_1
-- Lean.Meta.Diagnostics
Lean.Meta.mkDiagSummaryForUnfoldedReducible : Lean.PHashMap Lean.Name ℕ → Lean.MetaM Lean.Meta.DiagSummary
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.val_map : ∀ {α : Type u_1} (n : ℕ) {β : Type u_2} (f : α ↪ β) (s : ↑(Set.powersetCard α n)),
  ↑(Set.powersetCard.map n f s) = Finset.map f ↑s
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.component_nontrivial : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) (U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace) [hU : Nonempty ↥U],
  Nontrivial ↑(X.presheaf.obj (Opposite.op U))
-- Mathlib.Order.Antichain
IsAntichain.mono : ∀ {α : Type u_1} {r₁ r₂ : α → α → Prop} {s : Set α}, IsAntichain r₁ s → r₂ ≤ r₁ → IsAntichain r₂ s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  {f : (a : α) → β a → γ a}, (Std.DTreeMap.map f t).size = t.size
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.SemiCartesianMonoidalCategory.snd_def : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.SemiCartesianMonoidalCategory C]
  (X Y : C),
  CategoryTheory.SemiCartesianMonoidalCategory.snd X Y =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.SemiCartesianMonoidalCategory.isTerminalTensorUnit.from X) Y)
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom
-- Mathlib.Algebra.Order.Hom.Basic
/-- The argument is zero if its image under the map is zero.  -/
AddGroupNormClass.eq_zero_of_map_eq_zero : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : AddGroup α} {inst_1 : AddCommMonoid β}
  {inst_2 : PartialOrder β} {inst_3 : FunLike F α β} [self : AddGroupNormClass F α β] (f : F) {a : α}, f a = 0 → a = 0