mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α] (deg : C → α)
  (lt₁ : ∀ {X Y : C} (f : X ⟶ Y), W₁ f → ¬CategoryTheory.MorphismProperty.identities C f → deg Y < deg X)
  (lt₂ : ∀ {X Y : C} (f : X ⟶ Y), W₂ f → ¬CategoryTheory.MorphismProperty.identities C f → deg X < deg Y)
  (nonempty_unique : ∀ {X Y : C} (f : X ⟶ Y), Nonempty (Unique (W₁.MapFactorizationData W₂ f))) (deg_1 : C → α)
  (lt₁_1 : ∀ {X Y : C} (f : X ⟶ Y), W₁ f → ¬CategoryTheory.MorphismProperty.identities C f → deg_1 Y < deg_1 X)
  (lt₂_1 : ∀ {X Y : C} (f : X ⟶ Y), W₂ f → ¬CategoryTheory.MorphismProperty.identities C f → deg_1 X < deg_1 Y)
  (nonempty_unique_1 : ∀ {X Y : C} (f : X ⟶ Y), Nonempty (Unique (W₁.MapFactorizationData W₂ f))),
  ({ deg := deg, lt₁ := lt₁, lt₂ := lt₂, nonempty_unique := nonempty_unique } =
      { deg := deg_1, lt₁ := lt₁_1, lt₂ := lt₂_1, nonempty_unique := nonempty_unique_1 }) =
    (deg = deg_1)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.step_filterMap : ∀ {α β β' : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] {it : Std.IterM m β} [inst_1 : Monad m]
  [LawfulMonad m] {f : β → Option β'},
  (Std.IterM.filterMap f it).step = do
    let __do_lift ← it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ =>
        match h' : f out with
        | none => pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.filterMap f it') ⋯))
        | some out' => pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.filterMap f it') out' ⋯))
      | ⟨Std.IterStep.skip it', h⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.filterMap f it') ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- Two alternating maps indexed by a `Fintype` are equal if they are equal when all arguments
are distinct basis vectors.  -/
Module.Basis.ext_alternating : ∀ {ι : Type u_7} {ι₁ : Type u_10} [Finite ι] {R' : Type u_11} {N₁ : Type u_12} {N₂ : Type u_13} [inst : CommSemiring R']
  [inst_1 : AddCommMonoid N₁] [inst_2 : AddCommMonoid N₂] [inst_3 : Module R' N₁] [inst_4 : Module R' N₂]
  {f g : N₁ [⋀^ι]→ₗ[R'] N₂} (e : Module.Basis ι₁ R' N₁),
  (∀ (v : ι → ι₁), Function.Injective v → (f fun i => e (v i)) = g fun i => e (v i)) → f = g
-- Init.Data.Nat.Lemmas
Nat.pow_dvd_pow : ∀ {m n : ℕ} (a : ℕ), m ≤ n → a ^ m ∣ a ^ n
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.Nonempty.mk : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {P : CategoryTheory.ObjectProperty C},
  (∃ X, P X) → P.Nonempty
-- Mathlib.Util.ParseCommand
/-- Parse a string as a tactic sequence.

This is a slight modification of `Parser.runParserCategory`.  -/
Mathlib.GuardExceptions.parseAsTacticSeq : Lean.Environment → String → optParam String "<input>" → Except String (Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)
-- Mathlib.Order.CompleteLatticeIntervals
Set.Iic.coe_sSup : ∀ {α : Type u_2} [inst : CompleteLattice α] {a : α} (S : Set ↑(Set.Iic a)), ↑(sSup S) = sSup (Subtype.val '' S)
-- Mathlib.RingTheory.DedekindDomain.Different
not_dvd_differentIdeal_of_isCoprime_of_isSeparable : ∀ (A : Type u_1) {B : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain A]
  [inst_4 : IsDedekindDomain A] [inst_5 : IsDedekindDomain B] [inst_6 : Module.IsTorsionFree A B]
  [inst_7 : Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} [p.IsMaximal]
  (P Q : Ideal B) [P.IsMaximal] [inst_11 : P.LiesOver p],
  IsCoprime P Q →
    P * Q = Ideal.map (algebraMap A B) p → ∀ [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)], ¬P ∣ differentIdeal A B
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_empty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {a : α}, Std.DTreeMap.Internal.Impl.empty.getKey? a = none
-- Std.Do.SPred.Notation
/-- Unexpander that reconstructs `spred(¬ ...)⌝` syntax from applications of `SPred.not`, lifting
nested applications of `spred(...)` from the argument.
 -/
Std.Do.SPred.Notation.unexpandNot : Lean.PrettyPrinter.Unexpander
-- Init.Data.Int.Order
Int.add_lt_add_iff_right : ∀ {a b : ℤ} (c : ℤ), a + c < b + c ↔ a < b
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.coe_toBialgHom : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (e : A ≃ₐc[R] B), ⇑↑e = ⇑e
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.instIsCentralScalar : ∀ {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : (i : ι) → AddCommMonoid (M₁ i)] [inst_1 : AddCommMonoid M₂]
  [inst_2 : (i : ι) → TopologicalSpace (M₁ i)] [inst_3 : TopologicalSpace M₂] {R' : Type u_1} {A : Type u_3}
  [inst_4 : Semiring A] [inst_5 : (i : ι) → Module A (M₁ i)] [inst_6 : Module A M₂] [inst_7 : DistribSMul R' M₂]
  [inst_8 : ContinuousConstSMul R' M₂] [inst_9 : SMulCommClass A R' M₂] [inst_10 : DistribSMul R'ᵐᵒᵖ M₂]
  [inst_11 : IsCentralScalar R' M₂], IsCentralScalar R' (ContinuousMultilinearMap A M₁ M₂)
-- Init.Data.Int.DivMod.Lemmas
Int.add_neg_mul_fmod_self_right : ∀ (a b c : ℤ), (a + -(b * c)).fmod c = a.fmod c
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
/-- Given `φ : F ⟶ G`, this is the cochain in `Cochain (mappingCone φ) K n` that is
constructed from two cochains `α : Cochain F K m` (with `m + 1 = n`) and `β : Cochain F K n`.  -/
CochainComplex.mappingCone.descCochain : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} →
        (φ : F ⟶ G) →
          [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
            {K : CochainComplex C ℤ} →
              {n m : ℤ} →
                CochainComplex.HomComplex.Cochain F K m →
                  CochainComplex.HomComplex.Cochain G K n →
                    m + 1 = n → CochainComplex.HomComplex.Cochain (CochainComplex.mappingCone φ) K n
-- Mathlib.ModelTheory.Satisfiability
/-- The Löwenheim–Skolem Theorem: If `κ` is a cardinal greater than the cardinalities of `L`
and an infinite `L`-structure `M`, then there is an elementary embedding in the appropriate
direction between then `M` and a structure of cardinality `κ`.  -/
FirstOrder.Language.exists_elementaryEmbedding_card_eq : ∀ (L : FirstOrder.Language) (M : Type w') [inst : L.Structure M] [iM : Infinite M] (κ : Cardinal.{w}),
  Cardinal.aleph0 ≤ κ →
    Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ →
      ∃ N, (Nonempty (L.ElementaryEmbedding (↑N) M) ∨ Nonempty (L.ElementaryEmbedding M ↑N)) ∧ Cardinal.mk ↑N = κ
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun
/-- The integral of the derivative of a product of two absolutely continuous functions.  -/
AbsolutelyContinuousOnInterval.integral_deriv_mul_eq_sub : ∀ {f g : ℝ → ℝ} {a b : ℝ},
  AbsolutelyContinuousOnInterval f a b →
    AbsolutelyContinuousOnInterval g a b → ∫ (x : ℝ) in a..b, deriv f x * g x + f x * deriv g x = f b * g b - f a * g a
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.reverse_reverse : ∀ {α : Type u_1} {a : FreeMonoid α}, a.reverse.reverse = a
-- Mathlib.Order.Interval.Finset.Defs
Finset.map_subtype_embedding_Ico : ∀ {α : Type u_1} [inst : Preorder α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : LocallyFiniteOrder α]
  (a b : Subtype p),
  (∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x) →
    Finset.map (Function.Embedding.subtype p) (Finset.Ico a b) = Finset.Ico ↑a ↑b
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- The left Kan extension of `g` along `f` at the level of structured arrows.  -/
CategoryTheory.Bicategory.lanLeftExtension : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f : a ⟶ b) →
        (g : a ⟶ c) → [CategoryTheory.Bicategory.HasLeftKanExtension f g] → CategoryTheory.Bicategory.LeftExtension f g
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
/-- `Proj` of a graded ring as a `SheafedSpace`  -/
AlgebraicGeometry.Proj.toSheafedSpace : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] → (𝒜 : ℕ → σ) → [GradedRing 𝒜] → AlgebraicGeometry.SheafedSpace CommRingCat
-- Mathlib.Algebra.Group.Defs
npowRec'_succ : ∀ {M : Type u_2} [inst : Mul M] [inst_1 : One M] {k : ℕ}, k ≠ 0 → ∀ (m : M), npowRec' (k + 1) m = npowRec' k m * m
-- Mathlib.Algebra.Group.PNatPowAssoc
ppow_mul_assoc : ∀ {M : Type u_1} [inst : Mul M] [inst_1 : Pow M ℕ+] [PNatPowAssoc M] (k m n : ℕ+) (x : M),
  x ^ k * x ^ m * x ^ n = x ^ k * (x ^ m * x ^ n)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.nsmul_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N X : C} [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N] (f : X ⟶ M) (n : ℕ)
  (g : M ⟶ N) [CategoryTheory.IsAddMonHom g],
  CategoryTheory.CategoryStruct.comp (n • f) g = n • CategoryTheory.CategoryStruct.comp f g
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
/-- The functor between free groupoids induced by a functor between categories.  -/
CategoryTheory.FreeGroupoid.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} D] →
        CategoryTheory.Functor C D →
          CategoryTheory.Functor (CategoryTheory.FreeGroupoid C) (CategoryTheory.FreeGroupoid D)
-- Mathlib.Algebra.Group.Defs
npowRec_add : ∀ {M : Type u} [inst : One M] [inst_1 : Semigroup M] (m n : ℕ),
  n ≠ 0 → ∀ (a : M), 1 * a = a → npowRec (m + n) a = npowRec m a * npowRec n a
-- Mathlib.AlgebraicTopology.DoldKan.Notations
/-- The alternating face map complex, on objects  -/
DoldKan.«termK[_]» : Lean.ParserDescr
-- Mathlib.Algebra.Star.Unitary
commute_unitary_star_self : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {u : R}, u ∈ unitary R → Commute (star u) u
-- Lean.Meta.Constructions.SparseCasesOn
_private.Lean.Meta.Constructions.SparseCasesOn.0.Lean.Meta.SparseCasesOnKey : Type
-- Mathlib.Probability.Kernel.Disintegration.Basic
MeasureTheory.Measure.IsCondKernel.mk : ∀ {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} {ρ : MeasureTheory.Measure (α × Ω)}
  {ρCond : ProbabilityTheory.Kernel α Ω}, ρ.fst.compProd ρCond = ρ → ρ.IsCondKernel ρCond
-- Init.Data.UInt.Basic
instDivUInt8 : Div UInt8
-- Mathlib.Order.CompleteBooleanAlgebra
sdiff_iInf_eq : ∀ {α : Type u} {ι : Sort w} [inst : Order.Coframe α] {a : α} {f : ι → α}, a \ ⨅ x, f x = ⨆ x, a \ f x
-- Mathlib.Topology.Homotopy.Lifting
IsQuotientCoveringMap.unop_fundamentalGroupToMulOpposite_smul : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hp : IsQuotientCoveringMap p G) {x : X} {e : ↑(p ⁻¹' {x})}
  {γ : FundamentalGroup X x}, MulOpposite.unop ((hp.fundamentalGroupToMulOpposite e) γ) • ↑e = ↑(⋯.monodromy γ e)
-- Mathlib.CategoryTheory.Sites.CompatibleSheafification
CategoryTheory.GrothendieckTopology.toSheafify_comp_sheafifyCompIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [inst_7 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  [inst_8 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  (P : CategoryTheory.Functor Cᵒᵖ D),
  CategoryTheory.CategoryStruct.comp (J.toSheafify (P.comp F)) (J.sheafifyCompIso F P).inv =
    CategoryTheory.Functor.whiskerRight (J.toSheafify P) F
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
le_of_span_le_span : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R]
  {s t u : Set M}, LinearIndepOn R id u → s ⊆ u → t ⊆ u → Submodule.span R s ≤ Submodule.span R t → s ⊆ t
-- Mathlib.RingTheory.Polynomial.Hermite.Basic
Polynomial.hermite_eq_iterate : ∀ (n : ℕ), Polynomial.hermite n = (fun p => Polynomial.X * p - Polynomial.derivative p)^[n] 1
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instMonoModuleCatToModuleCatHom : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B)
  [CategoryTheory.Mono f], CategoryTheory.Mono (Rep.Hom.toModuleCatHom f)
-- Mathlib.LinearAlgebra.Dual.Lemmas
Submodule.dualCopairing_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {W : Submodule R M}
  (φ : ↥W.dualAnnihilator) (x : M), (W.dualCopairing φ) (Submodule.Quotient.mk x) = φ x
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
/-- Given complementary embeddings of complex shapes
`e₁ : Embedding c₁ c` and `e₂ : Embedding c₂ c`, this is
the obvious map `ι₁ ⊕ ι₂ → ι` from the sum of the index
types of `c₁` and `c₂` to the index type of `c`.  -/
ComplexShape.Embedding.AreComplementary.fromSum : {ι : Type u_1} →
  {ι₁ : Type u_2} →
    {ι₂ : Type u_3} →
      {c : ComplexShape ι} →
        {c₁ : ComplexShape ι₁} → {c₂ : ComplexShape ι₂} → c₁.Embedding c → c₂.Embedding c → ι₁ ⊕ ι₂ → ι
-- Mathlib.CategoryTheory.ConnectedComponents
CategoryTheory.decomposedTo_obj : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J]
  (X : (i : CategoryTheory.ConnectedComponents J) × i.Component), (CategoryTheory.decomposedTo J).obj X = X.snd.obj
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_union_of_contains_eq_false_left : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (contains_eq_false : Std.DTreeMap.Internal.Impl.contains k m₁ = false)
  {h' : Std.DTreeMap.Internal.Impl.contains k (m₁.union m₂ ⋯ ⋯) = true},
  Std.DTreeMap.Internal.Impl.Const.get (m₁.union m₂ ⋯ ⋯) k h' = Std.DTreeMap.Internal.Impl.Const.get m₂ k ⋯
-- Mathlib.Order.Filter.IsBounded
Filter.IsBoundedUnder.mono : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {f g : Filter β} {u : β → α},
  f ≤ g → Filter.IsBoundedUnder r g u → Filter.IsBoundedUnder r f u
-- Mathlib.Algebra.Algebra.Subalgebra.Prod
AlgHom.range_prodMap : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C]
  [inst_6 : Algebra R C] [inst_7 : Semiring D] [inst_8 : Algebra R D] (f : A →ₐ[R] B) (g : C →ₐ[R] D),
  (f.prodMap g).range = f.range.prod g.range
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Create a continuous semilinear map between Schwartz spaces.

For an example of using this definition, see `fderivCLM`.  -/
SchwartzMap.mkCLM : {𝕜 : Type u_2} →
  {𝕜' : Type u_3} →
    {D : Type u_4} →
      {E : Type u_5} →
        {F : Type u_6} →
          {G : Type u_7} →
            [inst : NormedAddCommGroup E] →
              [inst_1 : NormedSpace ℝ E] →
                [inst_2 : NormedAddCommGroup F] →
                  [inst_3 : NormedSpace ℝ F] →
                    [inst_4 : NormedField 𝕜] →
                      [inst_5 : NormedField 𝕜'] →
                        [inst_6 : NormedAddCommGroup D] →
                          [inst_7 : NormedSpace ℝ D] →
                            [inst_8 : NormedSpace 𝕜 E] →
                              [inst_9 : SMulCommClass ℝ 𝕜 E] →
                                [inst_10 : NormedAddCommGroup G] →
                                  [inst_11 : NormedSpace ℝ G] →
                                    [inst_12 : NormedSpace 𝕜' G] →
                                      [inst_13 : SMulCommClass ℝ 𝕜' G] →
                                        {σ : 𝕜 →+* 𝕜'} →
                                          [RingHomIsometric σ] →
                                            (A : SchwartzMap D E → F → G) →
                                              (∀ (f g : SchwartzMap D E) (x : F), A (f + g) x = A f x + A g x) →
                                                (∀ (a : 𝕜) (f : SchwartzMap D E) (x : F), A (a • f) x = σ a • A f x) →
                                                  (∀ (f : SchwartzMap D E), ContDiff ℝ (↑⊤) (A f)) →
                                                    (∀ (n : ℕ × ℕ),
                                                        ∃ s C,
                                                          0 ≤ C ∧
                                                            ∀ (f : SchwartzMap D E) (x : F),
                                                              ‖x‖ ^ n.1 * ‖iteratedFDeriv ℝ n.2 (A f) x‖ ≤
                                                                C * (s.sup (schwartzSeminormFamily 𝕜 D E)) f) →
                                                      SchwartzMap D E →SL[σ] SchwartzMap F G
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_mul_le : ∀ {R : Type u} [inst : Semiring R] (p q : Polynomial R), (p * q).degree ≤ p.degree + q.degree
-- Mathlib.FieldTheory.SeparableClosure
IntermediateField.sepDegree_bot' : ∀ {F : Type u} (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type v) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K],
  Field.sepDegree F ↥⊥ = Field.sepDegree F E
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.exists_ne_zero_of_sSup_eq_top : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {f : M →ₛₗ[τ₁₂] M₂}, f ≠ 0 → ∀ (s : Set (Submodule R M)), sSup s = ⊤ → ∃ m ∈ s, f ∘ₛₗ m.subtype ≠ 0
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.toEquiv_symm : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M ≃+ N), ↑f.symm = (↑f).symm
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- A function has bounded variation on a set `s` if its total variation there is finite.  -/
BoundedVariationOn : {α : Type u_1} → [LinearOrder α] → {E : Type u_2} → [PseudoEMetricSpace E] → (α → E) → Set α → Prop
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.exists_isAffineOpen_mem_and_subset : ∀ {X : AlgebraicGeometry.Scheme} {x : ↥X} {U : X.Opens},
  x ∈ U → ∃ W, AlgebraicGeometry.IsAffineOpen W ∧ x ∈ W ∧ W.carrier ⊆ ↑U
-- Mathlib.Geometry.Manifold.Instances.Sphere
hasFDerivAt_stereoInvFunAux_comp_coe : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] (v : E),
  HasFDerivAt (stereoInvFunAux v ∘ Subtype.val) (ℝ ∙ v)ᗮ.subtypeL 0
-- Mathlib.Algebra.Algebra.Operations
Submodule.iSup_smul : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A] {M : Type u_1}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M] {ι : Sort u_2}
  {t : ι → Submodule R A} {N : Submodule R M}, (⨆ i, t i) • N = ⨆ i, t i • N
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instIntCast_1 : {α : Type u} →
  [inst : TopologicalSpace α] → {R : Type u_1} → [inst_1 : SeminormedRing R] → IntCast (BoundedContinuousFunction α R)
-- Mathlib.Data.Finite.Vector
List.Vector.finite : ∀ {α : Type u_1} [Finite α] {n : ℕ}, Finite (List.Vector α n)
-- Aesop.Search.Expansion
Aesop.runRegularRuleCore : {Q : Type} →
  [inst : Aesop.Queue Q] →
    Aesop.GoalRef →
      Aesop.RegularRule →
        Array Aesop.IndexMatchLocation →
          Option (Array Aesop.Substitution) → Aesop.SearchM Q (Option Aesop.RuleTacOutput)
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.AssociatorBimod.hom_right_act_hom' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {R S T U : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U),
  CategoryTheory.CategoryStruct.comp ((P.tensorBimod Q).tensorBimod L).actRight (Bimod.AssociatorBimod.hom P Q L) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (Bimod.AssociatorBimod.hom P Q L) U.X)
      (P.tensorBimod (Q.tensorBimod L)).actRight
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
jacobiSym.div_four_left : ∀ {a : ℤ} {b : ℕ}, a % 4 = 0 → b % 2 = 1 → jacobiSym (a / 4) b = jacobiSym a b
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.coe_iInf : ∀ {R : Type u} [inst : NonAssocSemiring R] {ι : Sort u_1} {S : ι → Subsemiring R}, ↑(⨅ i, S i) = ⋂ i, ↑(S i)
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.isCompl_iff : ∀ {α : Type u_1} [inst : CompleteLattice α] {L : CompleteSublattice α} {a b : ↥L}, IsCompl a b ↔ IsCompl ↑a ↑b
-- Init.Data.UInt.Lemmas
USize.zero_lt_one : 0 < 1
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.derives_iff_eq_or_head : ∀ {T : Type u_1} {g : ContextFreeGrammar T} {u w : List (Symbol T g.NT)},
  g.Derives u w ↔ u = w ∨ ∃ v, g.Produces u v ∧ g.Derives v w
-- Mathlib.Order.Cover
Prod.covBy_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] {x y : α × β},
  x ⋖ y ↔ x.1 ⋖ y.1 ∧ x.2 = y.2 ∨ x.2 ⋖ y.2 ∧ x.1 = y.1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).size = if t.contains k = true then t.size - 1 else t.size
-- Mathlib.Data.Quot
/-- A function `f : α → β` defines a function `map f : Trunc α → Trunc β`.  -/
Trunc.map : {α : Sort u_1} → {β : Sort u_2} → (α → β) → Trunc α → Trunc β
-- Init.Data.UInt.Basic
/-- Bitwise and for 64-bit unsigned integers. Usually accessed via the `&&&` operator.

Each bit of the resulting integer is set if the corresponding bits of both input integers are set.

This function is overridden at runtime with an efficient implementation.
 -/
UInt64.land : UInt64 → UInt64 → UInt64
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousMultilinearMap.hasFiniteFPowerSeriesOnBall : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_5} {Em : ι → Type u_6} [inst_3 : (i : ι) → NormedAddCommGroup (Em i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (Em i)] [inst_5 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 Em F),
  HasFiniteFPowerSeriesOnBall (⇑f) f.toFormalMultilinearSeries 0 (Fintype.card ι + 1) ⊤
-- Plausible.DeriveArbitrary
/-- Creates an instance of the `ArbitraryFueled` typeclass  -/
_private.Plausible.DeriveArbitrary.0.Plausible.mkArbitraryFueledInstanceCmd : Lean.Name → Lean.Elab.TermElabM (Array Lean.Syntax)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.star_eq_zero : ∀ {z : Complex.UnitDisc}, star z = 0 ↔ z = 0
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.instCharZero : CharZero Cardinal.{u_1}