mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.mul_one : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ}
  (a : TensorPower R n M), (TensorPower.cast R M ⋯) (GradedMonoid.GMul.mul a GradedMonoid.GOne.one) = a
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
CategoryTheory.ShortComplex.quasiIso_opMap : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂)
  [CategoryTheory.ShortComplex.QuasiIso φ], CategoryTheory.ShortComplex.QuasiIso (CategoryTheory.ShortComplex.opMap φ)
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
/-- Given two family of morphisms `f : X i ⟶ S` and `f' : X' j ⟶ S`,
two objects `D₁ D₂ : F.DescentData f`, a morphism `φ` between the images in
`F.DescentData f'` of `D₁` and `D₂` by a functor `pullFunctor`. This is
a family of elements of the sheaf of morphisms from `D₁.obj i` to `D₂.obj i`
that is deduced from `φ` over a covering sieve. See `hom` below for the glued
morphism `D₁.obj i ⟶ D₂.obj i` when `f'` is a covering family and `F` is a prestack.  -/
_private.Mathlib.CategoryTheory.Sites.Descent.Precoverage.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.familyOfElements : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              {ι' : Type t'} →
                {X' : ι' → C} →
                  {f' : (j : ι') → X' j ⟶ S} →
                    {α : ι' → ι} →
                      {p' : (j : ι') → X' j ⟶ X (α j)} →
                        (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = f' j) →
                          {D₁ D₂ : F.DescentData f} →
                            ((CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₁ ⟶
                                (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₂) →
                              (i : ι) →
                                CategoryTheory.Presieve.FamilyOfElements (F.presheafHom (D₁.obj i) (D₂.obj i))
                                  (CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve✝ f f' i).arrows
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPCoercions : Lean.Options → Bool
-- Init.Data.Range.Polymorphic.UInt
UInt8.instLawfulHasSize_1 : Std.Rxo.LawfulHasSize UInt8
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKeyD_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k} {fallback : α},
      Std.Internal.List.maxKeyD (Std.Internal.List.insertEntry k v l) fallback =
        (Std.Internal.List.maxKey? l).elim k fun k' => if (compare k' k).isLE = true then k else k'
-- Init.Data.String.Lemmas.Pattern.Find.Char
String.Slice.contains_char_eq : ∀ {c : Char} {s : String.Slice}, s.contains c = decide (c ∈ s.copy.toList)
-- Init.Data.UInt.Bitwise
UInt32.toUInt64_or : ∀ (a b : UInt32), (a ||| b).toUInt64 = a.toUInt64 ||| b.toUInt64
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.instInhabitedAtom₁ : Inhabited Mathlib.Tactic.BicategoryLike.Atom₁
-- Init.Data.BitVec.Basic
/-- `umulOverflow x y` returns `true` if multiplying `x` and `y` results in *unsigned* overflow.

SMT-Lib name: `bvumulo`.
 -/
BitVec.umulOverflow : {w : ℕ} → BitVec w → BitVec w → Bool
-- Mathlib.Data.Set.Pairwise.Basic
Set.Pairwise.eq_1 : ∀ {α : Type u_1} (s : Set α) (r : α → α → Prop), s.Pairwise r = ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → r x y
-- Mathlib.Algebra.GroupWithZero.Subgroup
AddSubgroup.smul_mem_pointwise_smul_iff : ∀ {G : Type u_2} {A : Type u_4} [inst : Group G] [inst_1 : AddGroup A] [inst_2 : DistribMulAction G A]
  {S : AddSubgroup A} {a : G} {x : A}, a • x ∈ a • S ↔ x ∈ S
-- Mathlib.CategoryTheory.Abelian.Images
/-- The inclusion of the image into the codomain.  -/
CategoryTheory.Abelian.image.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} →
        (f : P ⟶ Q) →
          [inst_2 : CategoryTheory.Limits.HasCokernel f] →
            [inst_3 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)] →
              CategoryTheory.Abelian.image f ⟶ Q
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.hopfAlgebra : {R : Type u} → [inst : CommRing R] → (self : CommHopfAlgCat R) → HopfAlgebra R ↑self
-- Mathlib.Tactic.Choose
Mathlib.Tactic.Choose.ChooseArg.mk : Lean.Syntax → Lean.Name → Option Lean.Term → Mathlib.Tactic.Choose.ChooseArg
-- Init.Prelude
instNatPowNat : NatPow ℕ
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesMap_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology] (φ : S₁ ⟶ S₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ) S₂.iCycles =
    CategoryTheory.CategoryStruct.comp S₁.iCycles φ.τ₂
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_eq_set_inter : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t s' t' : Set α}, s =ᵐ[μ] t → s' =ᵐ[μ] t' → s ∩ s' =ᵐ[μ] t ∩ t'
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.curryObjProdComp_inv_app_app : ∀ {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] {C' : Type u_1} {D' : Type u_2}
  [inst_3 : CategoryTheory.Category.{v_1, u_1} C'] [inst_4 : CategoryTheory.Category.{v_2, u_2} D']
  (F₁ : CategoryTheory.Functor C D) (F₂ : CategoryTheory.Functor C' D') (G : CategoryTheory.Functor (D × D') E) (X : C)
  (X_1 : C'),
  ((F₁.curryObjProdComp F₂ G).inv.app X).app X_1 = CategoryTheory.CategoryStruct.id (G.obj (F₁.obj X, F₂.obj X_1))
-- Lean.Declaration
Lean.ConstructorVal.isUnsafeEx : Lean.ConstructorVal → Bool
-- Mathlib.Probability.Independence.BoundedContinuousFunction
/-- Two stochastic processes $(X_s)_{s \in S}$ and $(Y_t)_{t \in T}$ are independent if
for all $s_1, ..., s_p \in S, t_1, ..., t_q \in T$ and
for all real bounded continuous functions $f$ and $g$,
$$P[f(X_{s_1}, ..., X_{s_p}) g(Y_{t_1}, ..., Y_{t_q})] =
P[f(X_{s_1}, ..., X_{s_p})] * P[g(Y_{t_1}, ..., Y_{t_q})].$$  -/
process_indepFun_process_of_bcf : ∀ {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : S → Type u_4}
  {F : T → Type u_5} [inst : (s : S) → TopologicalSpace (E s)] [inst_1 : (s : S) → MeasurableSpace (E s)]
  [∀ (s : S), BorelSpace (E s)] [∀ (s : S), HasOuterApproxClosed (E s)] [inst_4 : (t : T) → TopologicalSpace (F t)]
  [inst_5 : (t : T) → MeasurableSpace (F t)] [∀ (t : T), BorelSpace (F t)] [∀ (t : T), HasOuterApproxClosed (F t)]
  {X : (s : S) → Ω → E s} {Y : (t : T) → Ω → F t} [MeasureTheory.IsZeroOrProbabilityMeasure P],
  (∀ (s : S), AEMeasurable (X s) P) →
    (∀ (t : T), AEMeasurable (Y t) P) →
      (∀ (I : Finset S) (J : Finset T) (f : BoundedContinuousFunction ((s : ↥I) → E ↑s) ℝ)
          (g : BoundedContinuousFunction ((t : ↥J) → F ↑t) ℝ),
          ∫ (x : Ω), (fun ω => (f fun x => X (↑x) ω) * g fun x => Y (↑x) ω) x ∂P =
            (∫ (x : Ω), (fun ω => f fun x => X (↑x) ω) x ∂P) * ∫ (x : Ω), (fun ω => g fun x => Y (↑x) ω) x ∂P) →
        ProbabilityTheory.IndepFun (fun ω s => X s ω) (fun ω t => Y t ω) P
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderiv_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {g g' : M → F} {x : M}, MDiffAt g x → MDiffAt g' x → d% (g - g') x = d% g x - d% g' x
-- Lean.Util.PtrSet
Lean.PtrSet.contains : {α : Type} → Lean.PtrSet α → α → Bool
-- Mathlib.Order.OmegaCompletePartialOrder
ScottContinuous.ωScottContinuous : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β] {f : α → β},
  ScottContinuous f → OmegaCompletePartialOrder.ωScottContinuous f
-- Lean.Widget.UserWidget
Lean.Widget.instToModuleUserWidgetDefinition : Lean.Widget.ToModule Lean.Widget.UserWidgetDefinition
-- Mathlib.Analysis.Normed.Lp.Finsupp
Finsupp.dist_def : ∀ {ι : Type u_1} {X : Type u_2} [inst : Zero X] {p : NNReal} [inst_1 : Fact (1 ≤ p)] [inst_2 : PseudoMetricSpace X]
  (f g : WithLp (↑p) (ι →₀ X)), dist f g = ((Finsupp.zipWith dist ⋯ f.ofLp g.ofLp).sum fun _i r => r ^ ↑p) ^ (↑p)⁻¹
-- Mathlib.Logic.Equiv.Finset
Denumerable.lower_raise' : ∀ (l : List ℕ) (n : ℕ), Denumerable.lower' (Denumerable.raise' l n) n = l
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
HasFDerivWithinAt.eventually_notMem : ∀ {𝕜 : 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] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x →
    (∃ C, AntilipschitzWith C ⇑f') →
      ∀ (t : Set F), ¬AccPt (f x) (Filter.principal t) → ∀ᶠ (z : E) in nhdsWithin x (s \ {x}), f z ∉ t
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.alt : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Name →
    Array (Lean.Compiler.LCNF.Param pu) →
      Lean.Compiler.LCNF.Code pu →
        autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.Alt._auto_1 → Lean.Compiler.LCNF.Alt pu
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- the index type of the covering  -/
SheafOfModules.QuasicoherentData.I : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] →
          [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] →
            {M : SheafOfModules R} → M.QuasicoherentData → Type w
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.sigmaFiberAddEquiv_apply_apply : ∀ {ι₁ ι₂ : Type v} [inst : DecidableEq ι₂] (f : ι₁ → ι₂) {β : ι₁ → Type w} [inst_1 : (i : ι₁) → AddCommMonoid (β i)]
  (x : DirectSum ι₁ fun i => β i) (j : ι₂) (i' : { i // f i = j }), (((DirectSum.sigmaFiberAddEquiv f) x) j) i' = x ↑i'
-- Mathlib.Data.Set.Basic
Set.eq_of_forall_subset_iff : ∀ {α : Type u} {s t : Set α}, (∀ (u : Set α), s ⊆ u ↔ t ⊆ u) → s = t
-- Lean.Meta.Sym.Arith.Poly
Lean.Grind.CommRing.Poly.divConst : Lean.Grind.CommRing.Poly → ℤ → Lean.Grind.CommRing.Poly
-- Init.Data.String.Basic
String.Pos.Raw.extract.go₁ : List Char → String.Pos.Raw → String.Pos.Raw → String.Pos.Raw → List Char
-- Mathlib.CategoryTheory.Adjunction.Limits
/-- The unit for the adjunction for `Cone.functoriality K G : Cone K ⥤ Cone (K ⋙ G)`.

Auxiliary definition for `functorialityAdjunction'`.
 -/
CategoryTheory.Adjunction.functorialityUnit' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (adj : F ⊣ G) →
              {J : Type u} →
                [inst_2 : CategoryTheory.Category.{v, u} J] →
                  (K : CategoryTheory.Functor J D) →
                    CategoryTheory.Functor.id (CategoryTheory.Limits.Cone (K.comp G)) ⟶
                      (adj.functorialityLeftAdjoint K).comp (CategoryTheory.Limits.Cone.functoriality K G)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.unitOfList_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {k : α},
  Std.ExtDTreeMap.Const.unitOfList [k] cmp = ∅.insertIfNew k ()
-- Init.Data.Int.Order
Int.sign_neg_iff : ∀ {x : ℤ}, x.sign < 0 ↔ x < 0
-- Mathlib.Analysis.Convolution
MeasureTheory.convolution_congr : ∀ {𝕜 : 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' : 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] [MeasurableAdd₂ G] [MeasurableNeg G] [MeasureTheory.SFinite μ] [μ.IsAddRightInvariant],
  f =ᵐ[μ] f' → g =ᵐ[μ] g' → MeasureTheory.convolution f g L μ = MeasureTheory.convolution f' g' L μ
-- Mathlib.Geometry.Manifold.ChartedSpace
chart_target_mem_nhds : ∀ (H : Type u) {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  (x : M), (chartAt H x).target ∈ nhds (↑(chartAt H x) x)
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
/-- Constructor for Mayer-Vietoris squares taking as an input
a square `sq` such that `sq.f₁₃` is a mono and that for every
sheaf of types `F`, the square `sq.op.map F.val` is a pullback square.  -/
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] →
        (sq : CategoryTheory.Square C) →
          [CategoryTheory.Mono sq.f₁₃] →
            (∀ (F : CategoryTheory.Sheaf J (Type v)), (sq.op.map F.obj).IsPullback) → J.MayerVietorisSquare
-- Mathlib.Data.Bundle
Bundle.TotalSpace.mk.injEq : ∀ {B : Type u_1} {F : Type u_4} {E : B → Type u_5} (proj : B) (snd : E proj) (proj_1 : B) (snd_1 : E proj_1),
  (⟨proj, snd⟩ = ⟨proj_1, snd_1⟩) = (proj = proj_1 ∧ snd ≍ snd_1)
-- Mathlib.Algebra.Order.Floor.Defs
Nat.le_floor_iff : ∀ {α : Type u_2} [inst : Semiring α] [inst_1 : PartialOrder α] [inst_2 : FloorSemiring α] {a : α} {n : ℕ},
  0 ≤ a → (n ≤ ⌊a⌋₊ ↔ ↑n ≤ a)
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.prod_target : ∀ {X : Type u_1} {X' : Type u_2} {Y : Type u_3} {Y' : Type u_4} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace X'] [inst_2 : TopologicalSpace Y] [inst_3 : TopologicalSpace Y']
  (eX : OpenPartialHomeomorph X X') (eY : OpenPartialHomeomorph Y Y'), (eX.prod eY).target = eX.target ×ˢ eY.target
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderivWithin_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {s : Set M} {x : M} {f : M → E'}, UniqueMDiffAt[s] x → mfderiv[s] (-f) x = -mfderiv[s] f x
-- Mathlib.Tactic.Attr.Register
/-- A simp set for the `fin_omega` wrapper around `omega`.  -/
Parser.Attr.fin_omega : Lean.ParserDescr
-- Mathlib.Topology.Order.Rolle
/-- A continuous function on a closed interval with `f a = f b`
takes either its maximum or its minimum value at a point in the interior of the interval.  -/
exists_Ioo_extr_on_Icc : ∀ {X : Type u_1} {Y : Type u_2} [inst : ConditionallyCompleteLinearOrder X] [DenselyOrdered X]
  [inst_2 : TopologicalSpace X] [OrderTopology X] [inst_4 : LinearOrder Y] [inst_5 : TopologicalSpace Y]
  [OrderTopology Y] {f : X → Y} {a b : X},
  a < b → ContinuousOn f (Set.Icc a b) → f a = f b → ∃ c ∈ Set.Ioo a b, IsExtrOn f (Set.Icc a b) c
-- Mathlib.CategoryTheory.Comma.Presheaf.Colimit
_private.Mathlib.CategoryTheory.Comma.Presheaf.Colimit.0.CategoryTheory.«termE.obj» : Lean.ParserDescr
-- Mathlib.Order.BoundedOrder.Basic
Pi.instBoundedOrder : {ι : Type u_1} →
  {α' : ι → Type u_2} → [inst : (i : ι) → LE (α' i)] → [(i : ι) → BoundedOrder (α' i)] → BoundedOrder ((i : ι) → α' i)
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.op_sSup : ∀ {R : Type u_2} [inst : NonAssocRing R] (S : Set (Subring R)), (sSup S).op = sSup (Subring.unop ⁻¹' S)
-- Lean.Parser.Extra
/-- The parser `scientific` parses a scientific-notation literal, such as `1.3e-24`.

This parser has arity 1: it produces a `scientificLitKind` node containing an atom with the text
of the literal.
You can use `TSyntax.getScientific` to extract the parts from the resulting syntax object.  -/
Lean.Parser.scientificLit : Lean.Parser.Parser
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.zero_notMem_multiset_map_X_add_C : ∀ {R : Type u} [Nontrivial R] [inst : Semiring R] {α : Type u_1} (m : Multiset α) (f : α → R),
  0 ∉ Multiset.map (fun a => Polynomial.X + Polynomial.C (f a)) m
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.SplitIterator.instIteratorIdSubslice.match_3.eq_3 : ∀ {σ : String.Slice → Type} [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  {s : String.Slice} (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)) (motive : searcher.Step → Sort u_1)
  (searcher' : Std.Iter (String.Slice.Pattern.SearchStep s))
  (hps : searcher.IsPlausibleStep (Std.IterStep.skip searcher'))
  (h_1 :
    (searcher'_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (startPos endPos : s.Pos) →
        (hps_1 :
            searcher.IsPlausibleStep
              (Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos endPos))) →
          ⟨Std.IterStep.skip searcher', hps⟩ =
              ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos endPos), hps_1⟩ →
            motive ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos endPos), hps_1⟩)
  (h_2 :
    (searcher'_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (startPos endPos : s.Pos) →
        (hps_1 :
            searcher.IsPlausibleStep
              (Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos endPos))) →
          ⟨Std.IterStep.skip searcher', hps⟩ =
              ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps_1⟩ →
            motive ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps_1⟩)
  (h_3 :
    (searcher'_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
      (hps_1 : searcher.IsPlausibleStep (Std.IterStep.skip searcher'_1)) →
        ⟨Std.IterStep.skip searcher', hps⟩ = ⟨Std.IterStep.skip searcher'_1, hps_1⟩ →
          motive ⟨Std.IterStep.skip searcher'_1, hps_1⟩)
  (h_4 :
    (property : searcher.IsPlausibleStep Std.IterStep.done) →
      ⟨Std.IterStep.skip searcher', hps⟩ = ⟨Std.IterStep.done, property⟩ → motive ⟨Std.IterStep.done, property⟩),
  (match h : ⟨Std.IterStep.skip searcher', hps⟩ with
    | ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.matched startPos endPos), hps_1⟩ =>
      h_1 searcher'_1 startPos endPos hps_1 h
    | ⟨Std.IterStep.yield searcher'_1 (String.Slice.Pattern.SearchStep.rejected startPos endPos), hps_1⟩ =>
      h_2 searcher'_1 startPos endPos hps_1 h
    | ⟨Std.IterStep.skip searcher'_1, hps_1⟩ => h_3 searcher'_1 hps_1 h
    | ⟨Std.IterStep.done, property⟩ => h_4 property h) =
    h_3 searcher' hps ⋯
-- Std.Time.Time.PlainTime
/-- Represents a specific point in a day, including hours, minutes, seconds, and nanoseconds.
 -/
Std.Time.PlainTime : Type
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
instLTAdditive : {α : Type u_1} → [LT α] → LT (Additive α)
-- Mathlib.Analysis.Real.Sqrt
Real.div_sqrt : ∀ {x : ℝ}, x / √x = √x
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- The parametrized adjunction between `curriedTensor C : C ⥤ C ⥤ C`
and `internalHom : Cᵒᵖ ⥤ C ⥤ C`  -/
CategoryTheory.MonoidalClosed.internalHomAdjunction₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.MonoidalClosed C] →
        CategoryTheory.MonoidalCategory.curriedTensor C ⊣₂ CategoryTheory.MonoidalClosed.internalHom
-- Init.Data.Option.Lemmas
Option.merge_lt : ∀ {α : Type u_1} [inst : LT α] {f : α → α → α} {o₁ o₂ o₃ : Option α},
  (∀ (a b c : α), a < c → b < c → f a b < c) → o₁ < o₃ → o₂ < o₃ → Option.merge f o₁ o₂ < o₃
-- Mathlib.Data.Set.Finite.Basic
/-- A `Fintype` structure on `insert a s` when inserting a new element.  -/
Set.fintypeInsertOfNotMem : {α : Type u} → {a : α} → (s : Set α) → [Fintype ↑s] → a ∉ s → Fintype ↑(insert a s)
-- Lean.ProjFns
Lean.AuxParentProjectionInfo.mk.sizeOf_spec : ∀ (numParams : ℕ) (fromClass : Bool),
  sizeOf { numParams := numParams, fromClass := fromClass } = 1 + sizeOf numParams + sizeOf fromClass
-- Lean.Compiler.IR.Basic
Lean.IR.instHashableVarId : Hashable Lean.IR.VarId
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.hasColimitCompEvaluation : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (k : K) [CategoryTheory.Limits.HasColimit (F.flip.obj k)],
  CategoryTheory.Limits.HasColimit (F.comp ((CategoryTheory.evaluation K C).obj k))
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.IsCycle.ncard_neighborSet_toSubgraph_eq_two : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u u},
  p.IsCycle → v ∈ p.support → (p.toSubgraph.neighborSet v).ncard = 2
-- Mathlib.Analysis.Distribution.Support
Distribution.IsVanishingOn.eq_1 : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [inst : FunLike F α β] [inst_1 : TopologicalSpace α]
  [inst_2 : Zero β] [inst_3 : Zero V] (f : F → V) (s : Set α),
  Distribution.IsVanishingOn f s = ∀ (u : F), tsupport ⇑u ⊆ s → f u = 0
-- Mathlib.Order.Filter.CountableSeparatingOn
HasCountableSeparatingOn.of_subtype : ∀ {α : Type u_1} {p : Set α → Prop} {t : Set α} {q : Set ↑t → Prop} [h : HasCountableSeparatingOn (↑t) q Set.univ],
  (∀ (U : Set ↑t), q U → ∃ V, p V ∧ Subtype.val ⁻¹' V = U) → HasCountableSeparatingOn α p t
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits_zero_succ' : ∀ {n : ℕ}, n ≠ 0 → Nat.digits 0 n = [n]
-- Mathlib.CategoryTheory.Bicategory.Coherence
CategoryTheory.FreeBicategory.normalizeIso_id : ∀ {B : Type u} [inst : Quiver B] {a : B} {b : CategoryTheory.FreeBicategory B} (p : Quiver.Path a b),
  CategoryTheory.FreeBicategory.normalizeIso p (CategoryTheory.CategoryStruct.id b) =
    CategoryTheory.Bicategory.rightUnitor ((CategoryTheory.FreeBicategory.preinclusion B).map { as := p })
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
Real.smoothTransition.lt_one_of_lt_one : ∀ {x : ℝ}, x < 1 → x.smoothTransition < 1
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rco_eq_if_append : ∀ {m n : ℕ}, (m...n).toList = if m < n then (m...n - 1).toList ++ [n - 1] else []
-- Mathlib.Topology.SeparatedMap
IsSeparatedMap.comp_left : ∀ {X : Type u_2} {Y : Sort u_3} [inst : TopologicalSpace X] {A : Sort u_1} {f : X → Y},
  IsSeparatedMap f → ∀ {g : Y → A}, Function.Injective g → IsSeparatedMap (g ∘ f)
-- Mathlib.Order.CompleteLattice.Finset
Finset.iInf_union : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice β] [inst_1 : DecidableEq α] {f : α → β} {s t : Finset α},
  ⨅ x ∈ s ∪ t, f x = (⨅ x ∈ s, f x) ⊓ ⨅ x ∈ t, f x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent.0.iteratedDerivWithin_cot_pi_mul_sub_inv : ∀ (k : ℕ) {z : ℂ},
  z ∈ UpperHalfPlane.upperHalfPlaneSet →
    iteratedDerivWithin k (fun x => ↑Real.pi * (↑Real.pi * x).cot - 1 / x) UpperHalfPlane.upperHalfPlaneSet z =
      iteratedDerivWithin k (fun x => ↑Real.pi * (↑Real.pi * x).cot) UpperHalfPlane.upperHalfPlaneSet z -
        (-1) ^ k * ↑k.factorial * z ^ (-1 - ↑k)