mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
/-- The functor between categories of spectral objects that is induced by
a triangulated functor.  -/
CategoryTheory.Functor.mapTriangulatedSpectralObject : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [inst_3 : CategoryTheory.Preadditive C] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              {D : Type u_3} →
                [inst_6 : CategoryTheory.Category.{v_3, u_3} D] →
                  [inst_7 : CategoryTheory.Limits.HasZeroObject D] →
                    [inst_8 : CategoryTheory.HasShift D ℤ] →
                      [inst_9 : CategoryTheory.Preadditive D] →
                        [inst_10 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] →
                          [inst_11 : CategoryTheory.Pretriangulated D] →
                            (F : CategoryTheory.Functor C D) →
                              [inst_12 : F.CommShift ℤ] →
                                [F.IsTriangulated] →
                                  (ι : Type u_4) →
                                    [inst_14 : CategoryTheory.Category.{v_4, u_4} ι] →
                                      CategoryTheory.Functor (CategoryTheory.Triangulated.SpectralObject C ι)
                                        (CategoryTheory.Triangulated.SpectralObject D ι)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.fold.eq_def : ∀ {σ : Sort u_1} {α : Type u_2} (v₀ : σ) (f : σ → α → σ → σ) (x : RBTree.RBNode α),
  RBTree.RBNode.fold v₀ f x =
    match x with
    | RBTree.RBNode.nil => v₀
    | RBTree.RBNode.node c l v r => f (RBTree.RBNode.fold v₀ f l) v (RBTree.RBNode.fold v₀ f r)
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.conjTranspose_replicateCol : ∀ {m : Type u_2} {α : Type v} {ι : Type u_6} [inst : Star α] (v : m → α),
  (Matrix.replicateCol ι v).conjTranspose = Matrix.replicateRow ι (star v)
-- Mathlib.Topology.UniformSpace.Cauchy
isComplete_iff_ultrafilter : ∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α},
  IsComplete s ↔ ∀ (l : Ultrafilter α), Cauchy ↑l → ↑l ≤ Filter.principal s → ∃ x ∈ s, ↑l ≤ nhds x
-- Mathlib.Data.Real.Basic
/-- Make a real number from a Cauchy sequence of rationals (by taking the equivalence class).  -/
Real.mk : CauSeq ℚ abs → ℝ
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- The image of a measurable set in a standard Borel space under a measurable map
is an analytic set.  -/
MeasurableSet.analyticSet_image : ∀ {X : Type u_3} {Y : Type u_4} [inst : MeasurableSpace X] [StandardBorelSpace X] [inst_2 : TopologicalSpace Y]
  [inst_3 : MeasurableSpace Y] [OpensMeasurableSpace Y] {f : X → Y} [SecondCountableTopology ↑(Set.range f)]
  {s : Set X}, MeasurableSet s → Measurable f → MeasureTheory.AnalyticSet (f '' s)
-- Mathlib.Data.List.Sublists
List.sublists_map : ∀ {α : Type u} {β : Type v} (f : α → β) (l : List α), (List.map f l).sublists = List.map (List.map f) l.sublists
-- Mathlib.NumberTheory.NumberField.Completion.Ramification
NumberField.InfinitePlace.inertiaDeg_of_liesOver : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K) (w : NumberField.InfinitePlace L) [inst_3 : w.LiesOver v],
  v.inertiaDeg w = ⊥.inertiaDeg v.Completion
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.IntegrableOn.mono : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.VectorMeasure X F} {f : X → E} {s t : Set X},
  MeasurableSet s → t ⊆ s → μ.IntegrableOn f s → μ.IntegrableOn f t
-- Mathlib.Algebra.Order.Module.Defs
OrderDual.instIsStrictOrderedModule : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : MonoidWithZero α] [inst_2 : AddCommGroup β]
  [inst_3 : PartialOrder β] [IsOrderedAddMonoid β] [inst_5 : DistribMulAction α β] [IsStrictOrderedModule α β],
  IsStrictOrderedModule α βᵒᵈ
-- Mathlib.LinearAlgebra.TensorProduct.Vanishing
TensorProduct.VanishesTrivially.of_fintype : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι : Type u_4} [inst_5 : Fintype ι] {m : ι → M} {n : ι → N}
  {κ : Type u_5} [inst_6 : Fintype κ] (a : ι → κ → R) (y : κ → N),
  (∀ (i : ι), n i = ∑ j, a i j • y j) → (∀ (j : κ), ∑ i, a i j • m i = 0) → TensorProduct.VanishesTrivially R m n
-- Mathlib.Analysis.Calculus.UniformLimitsDeriv
/-- A variant of the second fundamental theorem of calculus (FTC-2): If a sequence of functions
between real or complex normed spaces are differentiable on a ball centered at `x`, they
form a Cauchy sequence _at_ `x`, and their derivatives are Cauchy uniformly on the ball, then the
functions form a uniform Cauchy sequence on the ball.

NOTE: The fact that we work on a ball is typically all that is necessary to work with power series
and Dirichlet series (our primary use case). However, this can be generalized by replacing the ball
with any connected, bounded, open set and replacing uniform convergence with local uniform
convergence. See `cauchy_map_of_uniformCauchySeqOn_fderiv`.
 -/
uniformCauchySeqOn_ball_of_fderiv : ∀ {ι : Type u_1} {l : Filter ι} {E : Type u_2} [inst : NormedAddCommGroup E] {𝕜 : Type u_3}
  [inst_1 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] {G : Type u_4}
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace 𝕜 G] {f : ι → E → G} {f' : ι → E → E →L[𝕜] G} {x : E} {r : ℝ},
  UniformCauchySeqOn f' l (Metric.ball x r) →
    (∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y) →
      Cauchy (Filter.map (fun n => f n x) l) → UniformCauchySeqOn f l (Metric.ball x r)
-- Init.Data.UInt.Lemmas
USize.toBitVec_eq_of_eq : ∀ {a b : USize}, a = b → a.toBitVec = b.toBitVec
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A block containing `a` is the orbit of `a` under its stabilizer  -/
MulAction.IsBlock.orbit_stabilizer_eq : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X} [MulAction.IsPretransitive G X],
  MulAction.IsBlock G B → ∀ {a : X}, a ∈ B → MulAction.orbit (↥(MulAction.stabilizer G B)) a = B
-- Lean.Elab.Tactic.Grind.Param
_private.Lean.Elab.Tactic.Grind.Param.0.Lean.Elab.Tactic.processParam : Lean.Meta.Grind.Params →
  Lean.TSyntax `Lean.Parser.Tactic.grindParam →
    Option (Lean.TSyntax `Lean.Parser.Attr.grindMod) →
      Lean.TSyntax `ident → Bool → Bool → Bool → Lean.Elab.TermElabM Lean.Meta.Grind.Params
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsSemilinearSet.iUnion : ∀ {M : Type u_1} {ι : Type u_3} [inst : AddCommMonoid M] [Finite ι] {s : ι → Set M},
  (∀ (i : ι), IsSemilinearSet (s i)) → IsSemilinearSet (⋃ i, s i)
-- Mathlib.Tactic.Explode.Datatypes
Mathlib.Explode.Status.sintro.sizeOf_spec : sizeOf Mathlib.Explode.Status.sintro = 1
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Limits.pullbackConeEquivBinaryFan_inverse_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X}
  {c₁ c₂ : CategoryTheory.Limits.BinaryFan (CategoryTheory.Over.mk f) (CategoryTheory.Over.mk g)} (a : c₁ ⟶ c₂),
  (CategoryTheory.Limits.pullbackConeEquivBinaryFan.inverse.map a).hom = CategoryTheory.Over.Hom.left a.hom
-- Mathlib.Algebra.Module.CharacterModule
/-- Two isomorphic modules have isomorphic character modules.
 -/
CharacterModule.congr : {R : Type uR} →
  [inst : CommRing R] →
    {A : Type uA} →
      [inst_1 : AddCommGroup A] →
        {B : Type uB} →
          [inst_2 : AddCommGroup B] →
            [inst_3 : Module R A] → [inst_4 : Module R B] → (A ≃ₗ[R] B) → CharacterModule A ≃ₗ[R] CharacterModule B
-- Mathlib.Order.Ideal
Order.IsIdeal.mk : ∀ {P : Type u_2} [inst : LE P] {I : Set P},
  IsLowerSet I → I.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) I → Order.IsIdeal I
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normalizer_eq_top_iff : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, Subgroup.normalizer ↑H = ⊤ ↔ H.Normal
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.ofCoeff_zero`. -/
SkewMonoidAlgebra.ofFinsupp_zero : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k], { coeff := 0 } = 0
-- Lean.Meta.Sym.SymM
/-- None of the arguments of the function can be rewritten.  -/
Lean.Meta.Sym.CongrInfo.none : Lean.Meta.Sym.CongrInfo
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.contains_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → t.contains t.min! = true
-- Mathlib.Analysis.SpecificLimits.Normed
dist_partial_sum : ∀ {α : Type u_1} [inst : SeminormedAddCommGroup α] (u : ℕ → α) (n : ℕ),
  dist (∑ k ∈ Finset.range (n + 1), u k) (∑ k ∈ Finset.range n, u k) = ‖u n‖
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.BoundedFormula.alls.match_1.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → Sort u_4) (_n : ℕ)
  (φ : L.BoundedFormula α (_n + 1)) (h_1 : (φ : L.BoundedFormula α 0) → motive 0 φ)
  (h_2 : (_n : ℕ) → (φ : L.BoundedFormula α (_n + 1)) → motive _n.succ φ),
  (match _n.succ, φ with
    | 0, φ => h_1 φ
    | _n.succ, φ => h_2 _n φ) =
    h_2 _n φ
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Path.left.injEq : ∀ {α : Type u} (c : RBTree.RBColor) (parent : RBTree.RBNode.Path α) (v : α) (r : RBTree.RBNode α) (c_1 : RBTree.RBColor)
  (parent_1 : RBTree.RBNode.Path α) (v_1 : α) (r_1 : RBTree.RBNode α),
  (RBTree.RBNode.Path.left c parent v r = RBTree.RBNode.Path.left c_1 parent_1 v_1 r_1) =
    (c = c_1 ∧ parent = parent_1 ∧ v = v_1 ∧ r = r_1)
-- Mathlib.Data.EReal.Basic
EReal.toReal_ne_zero_iff : ∀ {x : EReal}, x.toReal ≠ 0 ↔ x ≠ 0 ∧ x ≠ ⊤ ∧ x ≠ ⊥
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.Cotangent.mk_C_mem_ker_cotangentComplex : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {σ : Type u_1}
  (G : Algebra.Generators R S σ) {r : R} (hr : MvPolynomial.C r ∈ G.ker),
  Algebra.Extension.Cotangent.mk ⟨MvPolynomial.C r, hr⟩ ∈ G.toExtension.cotangentComplex.ker
-- Mathlib.Data.Finset.SDiff
/-- `· ∪ s` is injective on finsets disjoint from `s`.  -/
Finset.disjoint_injOn_union_left : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), Set.InjOn (fun x => x ∪ s) {t | Disjoint s t}
-- Mathlib.Algebra.Category.CoalgCat.Monoidal
CoalgCat.tensorObj_isAddCommGroup : ∀ (R : Type u) [inst : CommRing R] (X Y : CoalgCat R),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).isAddCommGroup = TensorProduct.addCommGroup
-- Mathlib.Algebra.Category.Ring.Adjunctions
/-- The adjunction `G ↦ ℤ[G]` and `R ↦ Rˣ` between `CommGrpCat` and `CommRing`.  -/
CommRingCat.forget₂Adj : {R : CommRingCat} →
  CategoryTheory.Limits.IsInitial R →
    (R.monoidAlgebra.comp (CategoryTheory.Under.forget R) ⊣ CategoryTheory.forget₂ CommRingCat CommMonCat)
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithInitial.coconeLift.match_1.eq_2 : ∀ {J : Type u_1} (motive : CategoryTheory.WithInitial J → Sort u_2)
  (h_1 : (a : J) → motive (CategoryTheory.WithInitial.of a)) (h_2 : Unit → motive CategoryTheory.WithInitial.star),
  (match CategoryTheory.WithInitial.star with
    | CategoryTheory.WithInitial.of a => h_1 a
    | CategoryTheory.WithInitial.star => h_2 ()) =
    h_2 ()
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofEqOfNat.sizeOf_spec : ∀ (a b : Lean.Expr) (natStructId : ℕ) (la lb : Lean.Meta.Grind.Arith.Linear.LinExpr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofEqOfNat a b natStructId la lb) =
    1 + sizeOf a + sizeOf b + sizeOf natStructId + sizeOf la + sizeOf lb
-- Mathlib.ModelTheory.Order
FirstOrder.Language.order.relation_eq_leSymb : ∀ (R : FirstOrder.Language.order.Relations 2), R = FirstOrder.Language.leSymb
-- Init.Data.Array.MapIdx
Array.mapIdx_eq_mapFinIdx : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : ℕ → α → β}, Array.mapIdx f xs = xs.mapFinIdx fun i a x => f i a
-- Aesop.Search.Expansion
Aesop.SafeRulesResult.failed.injEq : ∀ (postponed postponed_1 : Array Aesop.PostponedSafeRule),
  (Aesop.SafeRulesResult.failed postponed = Aesop.SafeRulesResult.failed postponed_1) = (postponed = postponed_1)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getEntryGED_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : (a : α) × β a}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryGED k fallback = t₂.getEntryGED k fallback
-- Init.Data.Slice.List.Lemmas
ListSlice.toList_mkSlice_rci_eq_toList_mkSlice_rco : ∀ {α : Type u_1} {xs : ListSlice α} {lo : ℕ},
  Std.Slice.toList (Std.Rci.Sliceable.mkSlice xs lo...*) =
    Std.Slice.toList (Std.Rco.Sliceable.mkSlice xs lo...Std.Slice.size xs)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.ofRestrict_appIso : ∀ {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (U_1 : (X.restrict h).Opens),
  AlgebraicGeometry.Scheme.Hom.appIso (X.ofRestrict h) U_1 =
    CategoryTheory.Iso.refl
      (X.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor (X.ofRestrict h)).obj U_1)))
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.HasSubst.X_pow : ∀ {R : Type u_2} [inst : CommRing R] {n : ℕ}, n ≠ 0 → PowerSeries.HasSubst (PowerSeries.X ^ n)
-- Lean.Meta.Tactic.Grind.EMatch
/-- Matches pattern `pat` with term `e`  -/
Lean.Meta.Grind.EMatch.Cnstr.match : Option Lean.Meta.Grind.GenPatternInfo → Lean.Expr → Lean.Expr → Lean.Meta.Grind.EMatch.Cnstr
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.zip.denote_go : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {assign : α → Bool} {aig : Std.Sat.AIG α} (curr : ℕ)
  (hcurr : curr ≤ len) (s : aig.RefVec curr) (lhs rhs : aig.RefVec len)
  (f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [inst_3 : Std.Sat.AIG.RefVec.LawfulZipOperator α f]
  (idx : ℕ) (hidx1 : idx < len),
  curr ≤ idx →
    ⟦assign,
        { aig := (Std.Sat.AIG.RefVec.zip.go aig curr s hcurr lhs rhs f).aig,
          ref := (Std.Sat.AIG.RefVec.zip.go aig curr s hcurr lhs rhs f).vec.get idx hidx1 }⟧ =
      ⟦assign, f aig { lhs := lhs.get idx hidx1, rhs := rhs.get idx hidx1 }⟧
-- Mathlib.FieldTheory.Galois.Infinite
InfiniteGalois.mem_bot_iff_fixed : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [IsGalois k K] (x : K),
  x ∈ ⊥ ↔ ∀ (f : Gal(K/k)), f x = x
-- Mathlib.Data.Sym.Sym2
Sym2.Rel.swap : ∀ {α : Type u} (x y : α), Sym2.Rel α (x, y) (y, x)
-- Mathlib.CategoryTheory.Category.RelCat
CategoryTheory.RelCat.Hom.ext_iff : ∀ {X Y : CategoryTheory.RelCat} {f g : X ⟶ Y}, f = g ↔ f.rel = g.rel
-- Aesop.RuleSet.Filter
Aesop.RuleFilter.mk : Lean.Name → Aesop.ScopeName → Array Aesop.BuilderName → Array Aesop.PhaseName → Aesop.RuleFilter
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.rightAdjointObjIsDefined_of_isLimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {J : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} J]
  {R : CategoryTheory.Functor J D} {c : CategoryTheory.Limits.Cone R} (hc : CategoryTheory.Limits.IsLimit c)
  [CategoryTheory.Limits.HasLimitsOfShape J C],
  (∀ (j : J), F.rightAdjointObjIsDefined (R.obj j)) → F.rightAdjointObjIsDefined c.pt
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.instIsTorsionFree_1 : ∀ (K : Type u_4) (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
  Module.IsTorsionFree (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)
-- Std.Data.DTreeMap.Basic
/-- Carries out a monadic action on each mapping in the tree map in ascending order.  -/
Std.DTreeMap.forM : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {m : Type w → Type w₂} → [Monad m] → ((a : α) → β a → m PUnit.{w + 1}) → Std.DTreeMap α β cmp → m PUnit.{w + 1}
-- Mathlib.CategoryTheory.Triangulated.TStructure.Heart
CategoryTheory.Triangulated.TStructure.heart.eq_1 : ∀ {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), t.heart = t.le 0 ⊓ t.ge 0
-- Mathlib.Algebra.CubicDiscriminant
Cubic.degree_of_d_ne_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a = 0 → P.b = 0 → P.c = 0 → P.d ≠ 0 → P.toPoly.degree = 0
-- Mathlib.Analysis.Distribution.FourierMultiplier
SchwartzMap.fourierMultiplierCLM_smul : ∀ {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace ℝ E] [inst_4 : NormedSpace ℂ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℂ 𝕜 F] [inst_7 : FiniteDimensional ℝ E] [inst_8 : MeasurableSpace E] [inst_9 : BorelSpace E]
  {g : E → 𝕜},
  Function.HasTemperateGrowth g →
    ∀ (c : 𝕜), SchwartzMap.fourierMultiplierCLM F (c • g) = c • SchwartzMap.fourierMultiplierCLM F g
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.instBraidedForallEval : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] →
        [inst_2 : (i : I) → CategoryTheory.BraidedCategory (C i)] → (i : I) → (CategoryTheory.Pi.eval C i).Braided
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.toEquiv_mk : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (g : N → M)
  (h₁ : Function.LeftInverse g (↑f).toFun) (h₂ : Function.RightInverse g (↑f).toFun),
  { toLieModuleHom := f, invFun := g, left_inv := h₁, right_inv := h₂ }.toEquiv =
    { toFun := ⇑f, invFun := g, left_inv := h₁, right_inv := h₂ }
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDeriv_fun_id_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : ℕ}, iteratedDeriv n (fun a => a) 0 = if n = 1 then 1 else 0
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.natDegree_sum_le : ∀ {ι : Type w} (s : Finset ι) {S : Type u_1} [inst : Semiring S] (f : ι → Polynomial S),
  (∑ i ∈ s, f i).natDegree ≤ Finset.fold max 0 (Polynomial.natDegree ∘ f) s
-- Init.Data.Rat.Lemmas
Rat.intCast_inj : ∀ {a b : ℤ}, ↑a = ↑b ↔ a = b
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'_comp_id_inv_assoc : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ : B} (f : b₀ ⟶ b₁)
  {Z : F.obj b₀ ⟶ F.obj b₁} (h : F.map f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp' f (CategoryTheory.CategoryStruct.id b₁) f ⋯).inv h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b₁).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom h)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
/-- Auxiliary definition for `free_monoidal_category.project`.  -/
CategoryTheory.FreeMonoidalCategory.projectObj : {C : Type u} →
  {D : Type u'} →
    [inst : CategoryTheory.Category.{v', u'} D] →
      [CategoryTheory.MonoidalCategory D] → (C → D) → CategoryTheory.FreeMonoidalCategory C → D
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.Scheme.IsSeparated.mk : ∀ {X : AlgebraicGeometry.Scheme}, AlgebraicGeometry.IsSeparated (CategoryTheory.Limits.terminal.from X) → X.IsSeparated
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.homRel_equivalence_of_isCofibrant_src : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X Y : HomotopicalAlgebra.FibrantObject C} [HomotopicalAlgebra.IsCofibrant X.obj],
  Equivalence fun x1 x2 => HomotopicalAlgebra.FibrantObject.homRel C x1 x2
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eq_eRk_iff : ∀ {α : Type u_1} {M : Matroid α} {X : Set α} {n : ℕ∞},
  autoParam (X ⊆ M.E) Matroid.eq_eRk_iff._auto_1 → (M.eRk X = n ↔ ∃ I, M.IsBasis I X ∧ I.encard = n)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.ι_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  (c : CategoryTheory.Limits.PushoutCocone f g), c.ι.app CategoryTheory.Limits.WalkingSpan.right = c.inr
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.coe_asIdeal : ∀ {R : Type u_1} [inst : Ring R] {I : TwoSidedIdeal R}, ↑(TwoSidedIdeal.asIdeal I) = ↑I
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.UniversalCoprimeFactorizationRing.factor₁.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : Polynomial.MonicDegreeEq R n),
  Polynomial.UniversalCoprimeFactorizationRing.factor₁ m k hn p =
    (Polynomial.UniversalFactorizationRing.factor₁ m k hn p).map
      (algebraMap (Polynomial.UniversalFactorizationRing m k hn p)
        (Polynomial.UniversalCoprimeFactorizationRing m k hn p))
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.instConcreteCategoryAlgHomCarrier : {R : Type u} → [inst : CommRing R] → CategoryTheory.ConcreteCategory (CommAlgCat R) fun x1 x2 => ↑x1 →ₐ[R] ↑x2
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
Differentiable.clm_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {H : Type u_5} [inst_7 : NormedAddCommGroup H]
  [inst_8 : NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {d : E → F →L[𝕜] G},
  Differentiable 𝕜 c → Differentiable 𝕜 d → Differentiable 𝕜 fun y => c y ∘SL d y
-- Init.Data.UInt.Lemmas
UInt16.toUInt64_ofNat : ∀ {n : ℕ}, n < 65536 → (OfNat.ofNat n).toUInt64 = OfNat.ofNat n
-- Mathlib.GroupTheory.Nilpotent
/-- An additive group `G` is nilpotent iff there exists an ascending central series
which reaches `G` in finitely many steps.  -/
AddSubgroup.nilpotent_iff_finite_ascending_central_series : ∀ (G : Type u_1) [inst : AddGroup G], AddGroup.IsNilpotent G ↔ ∃ n H, AddSubgroup.IsAscendingCentralSeries H ∧ H n = ⊤
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.bot_def : ∀ {M : Type u_1} [inst : MulOneClass M], ⊥ = ⊥.saturation
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKeyD_eq_fallback : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = true → ∀ {fallback : α}, t.minKeyD fallback = fallback
-- Lean.Data.Lsp.Basic
Lean.Lsp.PartialResultParams : Type
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCone_π_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D)
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (j : J), (H.mapCone c).π.app j = H.map (c.π.app j)