mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.FiberBundle.Basic
FiberBundle.totalSpaceMk_isEmbedding : ∀ {B : Type u_2} (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (E : B → Type u_5)
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)] [FiberBundle F E]
  (x : B), Topology.IsEmbedding (Bundle.TotalSpace.mk x)
-- Mathlib.Topology.UnitInterval
unitInterval.symm_projIcc : ∀ (x : ℝ), unitInterval.symm (Set.projIcc 0 1 ⋯ x) = Set.projIcc 0 1 ⋯ (1 - x)
-- Mathlib.Data.Multiset.UnionInter
/-- `s ∩ t` is the multiset such that the multiplicity of each `a` in it is the minimum of the
multiplicity of `a` in `s` and `t`. This is the infimum of multisets.  -/
Multiset.inter : {α : Type u_1} → [DecidableEq α] → Multiset α → Multiset α → Multiset α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey!_eq_default : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = true → t.maxKey! = default
-- Mathlib.Topology.Inseparable
SeparationQuotient.subsingleton_iff : ∀ {α : Type u_4} [inst : TopologicalSpace α], Subsingleton (SeparationQuotient α) ↔ IndiscreteTopology α
-- Mathlib.Algebra.Lie.Normalizer
/-- Regarding a Lie subalgebra `H ⊆ L` as a module over itself, its normalizer is in fact a Lie
subalgebra.  -/
LieSubalgebra.normalizer : {R : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → LieSubalgebra R L → LieSubalgebra R L
-- Mathlib.Order.Hom.Basic
OrderIso.le_iff_le : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) {x y : α}, e x ≤ e y ↔ x ≤ y
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
/-- Two measures which are finite on closed-open intervals are equal if they agree on all
closed-open intervals.  -/
MeasureTheory.Measure.ext_of_Ico : ∀ {α : Type u_5} [inst : TopologicalSpace α] {_m : MeasurableSpace α} [SecondCountableTopology α]
  [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] [BorelSpace α] [NoMaxOrder α]
  (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure μ],
  (∀ ⦃a b : α⦄, a < b → μ (Set.Ico a b) = ν (Set.Ico a b)) → μ = ν
-- Mathlib.Topology.Algebra.PontryaginDual
/-- `ContinuousMonoidHom.dual` as a `ContinuousMonoidHom`.  -/
PontryaginDual.mapHom : (A : Type u_1) →
  (G : Type u_4) →
    [inst : Monoid A] →
      [inst_1 : CommGroup G] →
        [inst_2 : TopologicalSpace A] →
          [inst_3 : TopologicalSpace G] →
            [inst_4 : IsTopologicalGroup G] →
              [LocallyCompactSpace G] → (A →ₜ* G) →ₜ* PontryaginDual G →ₜ* PontryaginDual A
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.trivialOn_edgeSet : ∀ {α : Type u_1} (f : Set α), (Hypergraph.trivialOn f).edgeSet = ∅
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsFoelner.tendsto_meas_smul_symmDiff : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : Group G]
  [inst_2 : MulAction G X] {ι : Type u_3} {l : Filter ι} {F : ι → Set X},
  IsFoelner G μ l F → ∀ (g : G), Filter.Tendsto (fun i => μ (symmDiff (g • F i) (F i)) / μ (F i)) l (nhds 0)
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- The inverse Fourier transform of line derivative in direction `m` is given by multiplication of
`-(2 * π * Complex.I) • (inner ℝ · m)` with the inverse Fourier transform.  -/
TemperedDistribution.fourierInv_lineDerivOp_eq : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℂ F] (f : TemperedDistribution E F) (m : E),
  FourierTransformInv.fourierInv (LineDeriv.lineDerivOp m f) =
    -(2 * ↑Real.pi * Complex.I) •
      (TemperedDistribution.smulLeftCLM F fun x => ↑(inner ℝ x m)) (FourierTransformInv.fourierInv f)
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.polyCharpolyAux_map_aeval : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [inst : CommRing R]
  [inst_1 : AddCommGroup L] [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M]
  (φ : L →ₗ[R] Module.End R M) [inst_5 : Fintype ι] [inst_6 : Fintype ιM] [inst_7 : DecidableEq ι]
  [inst_8 : DecidableEq ιM] (b : Module.Basis ι R L) (bₘ : Module.Basis ιM R M) (A : Type u_8) [inst_9 : CommRing A]
  [inst_10 : Algebra R A] [inst_11 : Module.Finite A (TensorProduct R A M)]
  [inst_12 : Module.Free A (TensorProduct R A M)] (x : ι → A),
  Polynomial.map (MvPolynomial.aeval x).toRingHom (φ.polyCharpolyAux b bₘ) =
    ((LinearMap.tensorProduct R A M M ∘ₗ LinearMap.baseChange A φ)
        ((Algebra.TensorProduct.basis A b).repr.symm (Finsupp.equivFunOnFinite.symm x))).charpoly
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Alt.rhs : {σ : Type} → Lean.Elab.Term.Do.Alt σ → σ
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.ofNat_def : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddZeroClass M] (n : ℕ) [inst_2 : n.AtLeastTwo],
  OfNat.ofNat n = AddMonoidAlgebra.single 0 (OfNat.ofNat n)
-- Mathlib.Order.Partition.Finpartition
Finpartition.mem_part_iff_exists : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s) {a b : α},
  a ∈ P.part b ↔ ∃ p ∈ P.parts, a ∈ p ∧ b ∈ p
-- Lean.Meta.AbstractMVars
Lean.Meta.AbstractMVars.State.lctx : Lean.Meta.AbstractMVars.State → Lean.LocalContext
-- Mathlib.RingTheory.Noetherian.Basic
isNoetherian_top_iff : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  IsNoetherian R ↥⊤ ↔ IsNoetherian R M
-- Mathlib.Order.Lattice
instCommutativeMax_mathlib : ∀ {α : Type u} [inst : SemilatticeSup α], Std.Commutative fun x1 x2 => x1 ⊔ x2
-- Mathlib.GroupTheory.GroupAction.CardCommute
card_comm_eq_card_conjClasses_mul_card : ∀ (G : Type u_3) [inst : Group G], Nat.card { p // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G
-- Init.Data.List.Basic
List.zip.eq_1 : ∀ {α : Type u} {β : Type v}, List.zip = List.zipWith Prod.mk
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.toCols₁_apply : ∀ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) (i : m) (j : n₁),
  A.toCols₁ i j = A i (Sum.inl j)
-- Mathlib.CategoryTheory.Shift.CommShift
/-- The commutation isomorphisms for all `a`-shifts this functor is equipped with  -/
CategoryTheory.Functor.CommShift.commShiftIso : {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} →
        (F : CategoryTheory.Functor C D) →
          {A : Type u_6} →
            {inst_2 : AddMonoid A} →
              {inst_3 : CategoryTheory.HasShift C A} →
                {inst_4 : CategoryTheory.HasShift D A} →
                  [self : F.CommShift A] →
                    (a : A) → (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a)
-- Mathlib.RingTheory.Finiteness.Small
Submodule.small_sup : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {P Q : Submodule R M} [smallP : Small.{u, u_2} ↥P] [smallQ : Small.{u, u_2} ↥Q], Small.{u, u_2} ↥(P ⊔ Q)
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
/-- **Alias** of `Ordinal.cof_map_of_isNormal`. -/
Ordinal.cof_eq_of_isNormal : ∀ {f : Ordinal.{u_1} → Ordinal.{u_1}}, Order.IsNormal f → ∀ {a : Ordinal.{u_1}}, Order.IsSuccLimit a → (f a).cof = a.cof
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- The `v`-adic norm of an integer is less than 1 if and only if it is in the ideal.  -/
NumberField.FinitePlace.norm_lt_one_iff_mem : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] (x : R),
  ‖(NumberField.FinitePlace.embedding v) ((algebraMap R K) x)‖ < 1 ↔ x ∈ v.asIdeal
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.zsmul_singleton : ∀ {α : Type u_2} [inst : SubtractionMonoid α] (a : α) (n : ℤ), n • {a} = {n • a}
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Given two coforks with isomorphic components in such a way that the natural diagrams commute, then
one is a colimit if and only if the other one is.
 -/
CategoryTheory.Limits.Cofork.isColimitEquivOfIsos : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f g : X ⟶ Y} →
        {X' Y' : C} →
          (c : CategoryTheory.Limits.Cofork f g) →
            {f' g' : X' ⟶ Y'} →
              (c' : CategoryTheory.Limits.Cofork f' g') →
                (e₀ : X ≅ X') →
                  (e₁ : Y ≅ Y') →
                    (e : c.pt ≅ c'.pt) →
                      autoParam
                          (CategoryTheory.CategoryStruct.comp e₀.hom f' = CategoryTheory.CategoryStruct.comp f e₁.hom)
                          CategoryTheory.Limits.Cofork.isColimitEquivOfIsos._auto_1 →
                        autoParam
                            (CategoryTheory.CategoryStruct.comp e₀.hom g' = CategoryTheory.CategoryStruct.comp g e₁.hom)
                            CategoryTheory.Limits.Cofork.isColimitEquivOfIsos._auto_3 →
                          autoParam
                              (CategoryTheory.CategoryStruct.comp e₁.inv
                                  (CategoryTheory.CategoryStruct.comp c.π e.hom) =
                                c'.π)
                              CategoryTheory.Limits.Cofork.isColimitEquivOfIsos._auto_5 →
                            CategoryTheory.Limits.IsColimit c ≃ CategoryTheory.Limits.IsColimit c'
-- Mathlib.NumberTheory.ModularForms.Discriminant
/-- The discriminant expressed as a q-expansion: `Δ(z) = q * ∏' (1 - q ^ (n + 1)) ^ 24`.  -/
ModularForm.discriminant_eq_q_prod : ∀ (z : UpperHalfPlane),
  ModularForm.discriminant z = Function.Periodic.qParam 1 ↑z * ∏' (n : ℕ), (1 - ModularForm.eta_q n ↑z) ^ 24
-- Mathlib.Algebra.Order.Monoid.Lex
MonoidHom.inr_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst_1 : Preorder α] [inst_2 : Monoid β] [inst_3 : Preorder β],
  Monotone ⇑(MonoidHom.inr α β)
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.Monadic.step.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α] (it : Std.IterM Id α),
  Std.Rxc.Iterator.Monadic.step it =
    match it.internalState.next with
    | none => Std.IterStep.done
    | some next =>
      if next ≤ it.internalState.upperBound then
        Std.IterStep.yield
          { internalState := { next := Std.PRange.succ? next, upperBound := it.internalState.upperBound } } next
      else Std.IterStep.done
-- Mathlib.Data.List.OfFn
List.ofFn_succ' : ∀ {α : Type u} {n : ℕ} (f : Fin n.succ → α), List.ofFn f = (List.ofFn fun i => f i.castSucc).concat (f (Fin.last n))
-- Mathlib.Algebra.Group.Basic
zpow_sub_one : ∀ {G : Type u_3} [inst : Group G] (a : G) (n : ℤ), a ^ (n - 1) = a ^ n * a⁻¹
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.spanSingleton_mul_spanSingleton : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P] (x y : P),
  FractionalIdeal.spanSingleton S x * FractionalIdeal.spanSingleton S y = FractionalIdeal.spanSingleton S (x * y)
-- Mathlib.Analysis.Normed.Module.Ball.Action
instSMulElemSphereOfNatReal : {𝕜 : Type u_1} →
  {E : Type u_3} →
    [inst : NormedField 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] → [NormedSpace 𝕜 E] → {r : ℝ} → SMul ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 r)
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.iInf_iff : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {ι : Type u_1}
  (W : ι → CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y), iInf W f ↔ ∀ (i : ι), W i f
-- Mathlib.Data.List.SplitLengths
List.map_splitLengths_length : ∀ {α : Type u_1} (l : List α) (sz : List ℕ), sz.sum ≤ l.length → List.map List.length (sz.splitLengths l) = sz
-- Mathlib.NumberTheory.ModularForms.SlashActions
ModularForm.SL_slash : ∀ {k : ℤ} (f : UpperHalfPlane → ℂ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ),
  SlashAction.map k γ f =
    SlashAction.map k (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) f
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioc_subset_Iic_self : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] [inst_2 : LocallyFiniteOrder α],
  Finset.Ioc a b ⊆ Finset.Iic b
-- Lean.Meta.Basic
Lean.Meta.mkLevelStuckErrorMessage : Lean.Meta.PostponedEntry → Lean.MetaM Lean.MessageData
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the number of elements contained in the given left-closed right-unbounded range.
 -/
Std.Rci.size : {α : Type u} → [Std.Rxi.HasSize α] → Std.Rci α → ℕ
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : Preorder α]
  [inst_2 : TopologicalSpace β] [inst_3 : Preorder β] [inst_4 : TopologicalSpace γ] [inst_5 : Preorder γ]
  {g₁ g₂ : EsakiaHom β γ} {f : EsakiaHom α β}, Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.constPi_apply : ∀ (α : Type u_1) {β : Type u_2} [inst : TopologicalSpace β], ⇑(ContinuousMap.constPi α) = fun b => Function.const α b
-- Mathlib.Data.PNat.Factors
PrimeMultiset.instRepr : Repr PrimeMultiset
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
/-- The inverse map in `lTensor.equiv`  -/
lTensor.inverse : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {P : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : AddCommGroup N] →
              [inst_3 : AddCommGroup P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] →
                      {f : M →ₗ[R] N} →
                        {g : N →ₗ[R] P} →
                          (Q : Type u_5) →
                            [inst_7 : AddCommGroup Q] →
                              [inst_8 : Module R Q] →
                                Function.Exact ⇑f ⇑g →
                                  Function.Surjective ⇑g →
                                    TensorProduct R Q P →ₗ[R] TensorProduct R Q N ⧸ (LinearMap.lTensor Q f).range
-- Mathlib.Analysis.Convex.GaugeRescale
gaugeRescale_self_apply : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [T1Space E] {s : Set E},
  Absorbent ℝ s → Bornology.IsVonNBounded ℝ s → ∀ (x : E), gaugeRescale s s x = x
-- Mathlib.Data.Nat.Find
Nat.find_comp_succ : ∀ {p : ℕ → Prop} [inst : DecidablePred p] (h₁ : ∃ n, p n) (h₂ : ∃ n, p (n + 1)), ¬p 0 → Nat.find h₁ = Nat.find h₂ + 1
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.instAddMonoid : {R : Type u_1} → [inst : AddMonoid R] → AddMonoid (ArithmeticFunction R)
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.AreSeparated.empty_left : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (s : Set X), Metric.AreSeparated ∅ s
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- A morphism of functors `WithTerminal C ⥤ D` gives a morphism between the associated comma
objects.  -/
CategoryTheory.WithTerminal.mkCommaMorphism : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {F G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D} →
          (F ⟶ G) → (CategoryTheory.WithTerminal.mkCommaObject F ⟶ CategoryTheory.WithTerminal.mkCommaObject G)
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.CallHierarchy.mk : Lean.Lsp.CallHierarchyItem → Array Lean.Lsp.Range → Array Lean.Lsp.Ipc.CallHierarchy → Lean.Lsp.Ipc.CallHierarchy
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Polynomial.cyclotomic.eval_apply_ofReal : ∀ (q : ℝ) (n : ℕ), Polynomial.eval (↑q) (Polynomial.cyclotomic n ℂ) = ↑(Polynomial.eval q (Polynomial.cyclotomic n ℝ))
-- Std.Async.Select
Std.Async.Waiter.promise : {α : Type} → Std.Async.Waiter α → IO.Promise (Except IO.Error α)
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- Every `n`-colorable graph is contained in a `completeEquipartiteGraph` in `n` parts (as long
as the parts are at least as large as the largest color class).  -/
SimpleGraph.isContained_completeEquipartiteGraph_of_colorable : ∀ {α : Type u} {G : SimpleGraph α} [inst : Fintype α] {n : ℕ} (C : G.Coloring (Fin n)) (t : ℕ),
  (∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t) → G.IsContained (SimpleGraph.completeEquipartiteGraph n t)
-- Mathlib.Algebra.MonoidAlgebra.Lift
AddMonoidAlgebra.liftNC_mul : ∀ {k : Type u₁} {G : Type u₂} {R : Type u_2} [inst : Semiring k] [inst_1 : Add G] [inst_2 : Semiring R]
  {g_hom : Type u_6} [inst_3 : FunLike g_hom (Multiplicative G) R] [MulHomClass g_hom (Multiplicative G) R]
  (f : k →+* R) (g : g_hom) (a b : AddMonoidAlgebra k G),
  (∀ {x y : G}, y ∈ a.coeff.support → Commute (f (b.coeff x)) (g (Multiplicative.ofAdd y))) →
    (AddMonoidAlgebra.liftNC ↑f ⇑g) (a * b) = (AddMonoidAlgebra.liftNC ↑f ⇑g) a * (AddMonoidAlgebra.liftNC ↑f ⇑g) b
-- Mathlib.Analysis.Convolution
MeasureTheory.ConvolutionExistsAt.add_distrib : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f f' : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  {L : E →L[𝕜] E' →L[𝕜] F} [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : NormedSpace ℝ F]
  [inst_9 : AddGroup G] {x : G},
  MeasureTheory.ConvolutionExistsAt f g x L μ →
    MeasureTheory.ConvolutionExistsAt f' g x L μ →
      MeasureTheory.convolution (f + f') g L μ x =
        MeasureTheory.convolution f g L μ x + MeasureTheory.convolution f' g L μ x
-- Lean.LoadDynlib
/-- A dynamic library handle.  -/
Lean.Dynlib : Type
-- Mathlib.Order.Heyting.Basic
bot_sdiff : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a : α}, ⊥ \ a = ⊥
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.instMulSubtypeMemAddSubgroup : {R : Type u_1} → [inst : NonUnitalCommRing R] → [inst_1 : StarRing R] → Mul ↥(selfAdjoint R)
-- Mathlib.Data.Nat.Find
Nat.find_min' : ∀ {p : ℕ → Prop} [inst : DecidablePred p] (H : ∃ n, p n) {m : ℕ}, p m → Nat.find H ≤ m
-- Mathlib.Logic.Embedding.Basic
/-- There is always an embedding from an empty type.  -/
Function.Embedding.ofIsEmpty : {α : Sort u_1} → {β : Sort u_2} → [IsEmpty α] → α ↪ β
-- Mathlib.RepresentationTheory.Maschke
/-- We construct our `k[G]`-linear retraction of `i` as
$$ \frac{1}{|G|} \sum_{g \in G} g⁻¹ • π(g • -). $$
 -/
LinearMap.equivariantProjection : {k : Type u_1} →
  [inst : CommRing k] →
    (G : Type u_2) →
      [inst_1 : Group G] →
        {V : Type u_3} →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Module k V] →
              [inst_4 : Module (MonoidAlgebra k G) V] →
                [IsScalarTower k (MonoidAlgebra k G) V] →
                  {W : Type u_4} →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : Module k W] →
                        [inst_8 : Module (MonoidAlgebra k G) W] →
                          [IsScalarTower k (MonoidAlgebra k G) W] →
                            (W →ₗ[k] V) → [Fintype G] → W →ₗ[MonoidAlgebra k G] V
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.toSentence.eq_3 : FirstOrder.Field.FieldAxiom.negAddCancel.toSentence =
  ((-(FirstOrder.Language.var ∘ Sum.inr) 0 + (FirstOrder.Language.var ∘ Sum.inr) 0).bdEqual 0).all.all
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.strictMono : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (f : α ≃*o β), StrictMono ⇑f
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.eHomEquiv_id : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] (X : C),
  (CategoryTheory.eHomEquiv V) (CategoryTheory.CategoryStruct.id X) = CategoryTheory.eId V X
-- Mathlib.Algebra.Category.Grp.FilteredColimits
/-- The cocone over the proposed colimit additive group.  -/
AddGrpCat.FilteredColimits.colimitCocone : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] → (F : CategoryTheory.Functor J AddGrpCat) → CategoryTheory.Limits.Cocone F
-- Mathlib.Algebra.Field.Periodic
Int.fract_periodic : ∀ (α : Type u_4) [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α],
  Function.Periodic Int.fract 1
-- Mathlib.Combinatorics.Enumerative.Catalan.Basic
_private.Mathlib.Combinatorics.Enumerative.Catalan.Basic.0.gosper_catalan_sub_eq_central_binom_div : ∀ (n : ℕ), gosperCatalan✝ (n + 1) (n + 1) - gosperCatalan✝ (n + 1) 0 = ↑(n + 1).centralBinom / (↑n + 2)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instNonAssocCommRingOfRingHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → NonAssocCommRing (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] → NonAssocCommRing (DirectLimit G f)
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.disjoint_map_of_ker_le_left : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {p q : Submodule R M},
  Disjoint p q → f.ker ≤ p → Disjoint (Submodule.map f p) (Submodule.map f q)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.brecOn.eq : ∀ {motive_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr → Sort u}
  {motive_2 : Lean.Meta.Grind.Arith.Linear.EqCnstrProof → Sort u}
  {motive_3 : Lean.Meta.Grind.Arith.Linear.IneqCnstr → Sort u}
  {motive_4 : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof → Sort u}
  {motive_5 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr → Sort u}
  {motive_6 : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof → Sort u}
  {motive_7 : Lean.Meta.Grind.Arith.Linear.UnsatProof → Sort u} (t : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof)
  (F_1 : (t : Lean.Meta.Grind.Arith.Linear.EqCnstr) → t.below → motive_1 t)
  (F_2 : (t : Lean.Meta.Grind.Arith.Linear.EqCnstrProof) → t.below → motive_2 t)
  (F_3 : (t : Lean.Meta.Grind.Arith.Linear.IneqCnstr) → t.below → motive_3 t)
  (F_4 : (t : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof) → t.below → motive_4 t)
  (F_5 : (t : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) → t.below → motive_5 t)
  (F_6 : (t : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof) → t.below → motive_6 t)
  (F_7 : (t : Lean.Meta.Grind.Arith.Linear.UnsatProof) → t.below → motive_7 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 F_6 F_7 =
    F_6 t (Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.brecOn.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7).2
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.MaybeFunctionData.lam.inj : ∀ {f f_1 : Lean.Expr},
  Mathlib.Meta.FunProp.MaybeFunctionData.lam f = Mathlib.Meta.FunProp.MaybeFunctionData.lam f_1 → f = f_1
-- Mathlib.Data.Nat.Prime.Defs
Nat.Primes.coe_nat_inj : ∀ (p q : Nat.Primes), ↑p = ↑q ↔ p = q