mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- A family `𝓕 : ι → β → α` is uniformly equicontinuous iff the function `swap 𝓕 : β → ι → α` is
uniformly continuous *when `ι → α` is equipped with the uniform structure of uniform convergence*.
This is very useful for developing the equicontinuity API, but it should not be used directly
for other purposes.  -/
uniformEquicontinuous_iff_uniformContinuous : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] {F : ι → β → α},
  UniformEquicontinuous F ↔ UniformContinuous (⇑UniformFun.ofFun ∘ Function.swap F)
-- Std.Net.Addr
/-- A pair of an `IPv6Addr` and a port.
 -/
Std.Net.SocketAddressV6 : Type
-- Mathlib.Analysis.RCLike.Sqrt
/-- The square root of a complex number.  -/
Complex.sqrt : ℂ → ℂ
-- Mathlib.GroupTheory.Transfer
Subgroup.leftTransversals.diff.eq_1 : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {A : Type u_2} [inst_1 : CommGroup A] (ϕ : ↥H →* A)
  (S T : H.LeftTransversal) [inst_2 : H.FiniteIndex],
  Subgroup.leftTransversals.diff ϕ S T = ∏ q, ϕ ⟨(↑(⋯.leftQuotientEquiv q))⁻¹ * ↑(⋯.leftQuotientEquiv q), ⋯⟩
-- Mathlib.Data.List.Map2
List.zipRight'_cons_cons : ∀ {α : Type u} {β : Type v} (a : α) (as : List α) (b : β) (bs : List β),
  (a :: as).zipRight' (b :: bs) =
    have r := as.zipRight' bs;
    ((some a, b) :: r.1, r.2)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Under.Hom.mk_hom : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T}
  [inst_1 : Q.IsMultiplicative] {A B : P.Under Q X}
  (f :
    (CategoryTheory.MorphismProperty.Under.forget P Q X).obj A ⟶
      (CategoryTheory.MorphismProperty.Under.forget P Q X).obj B)
  (hf : Q (CategoryTheory.Under.Hom.right f)),
  CategoryTheory.MorphismProperty.Comma.Hom.hom (CategoryTheory.MorphismProperty.Under.Hom.mk f hf) = f
-- Mathlib.Data.Sym.Sym2
/-- "Attach" a proof `P a` that holds for all the elements of `s` to produce a new Sym2 object
with the same elements but in the type `{x // P x}`.
 -/
Sym2.attachWith : {α : Type u_1} → {P : α → Prop} → (s : Sym2 α) → (∀ a ∈ s, P a) → Sym2 { a // P a }
-- Mathlib.Data.Set.Basic
Set.decidableInter : {α : Type u} → (s t : Set α) → (a : α) → [Decidable (a ∈ s)] → [Decidable (a ∈ t)] → Decidable (a ∈ s ∩ t)
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- the underlying type of an object in `ModuleCat R`  -/
ModuleCat.carrier : {R : Type u} → [inst : Ring R] → ModuleCat R → Type v
-- Mathlib.CategoryTheory.Sites.Point.Category
CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  {Φ₁ Φ₂ Φ₃ : J.Point} (f : Φ₁ ⟶ Φ₂) (g : Φ₂ ⟶ Φ₃),
  CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber g)
      (CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber f)
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instGroup : {α : Type u_1} → [Group α] → Group αᵒᵈ
-- Mathlib.Data.List.AList
AList.mem_lookup_union_middle : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {s₁ s₂ s₃ : AList β},
  b ∈ AList.lookup a (s₁ ∪ s₃) → a ∉ s₂ → b ∈ AList.lookup a (s₁ ∪ s₂ ∪ s₃)
-- Mathlib.Order.Bounds.Basic
/-- **Alias** of `IsCofinalFor.of_subset`. -/
LE.le.isCofinalFor : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, s ⊆ t → IsCofinalFor s t
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.modify.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] (m m_1 : Std.DHashMap α β),
  m = m_1 → ∀ (a : α) (f f_1 : β a → β a), f = f_1 → m.modify a f = m_1.modify a f_1
-- Mathlib.Analysis.Calculus.Deriv.Add
derivWithin_neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) (s : Set 𝕜),
  UniqueDiffWithinAt 𝕜 s x → derivWithin Neg.neg s x = -1
-- Mathlib.Analysis.Convex.Extreme
IsExtreme.left_mem_of_mem_openSegment : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {A B : Set E},
  IsExtreme 𝕜 A B → ∀ ⦃x : E⦄, x ∈ A → ∀ ⦃y : E⦄, y ∈ A → ∀ ⦃z : E⦄, z ∈ B → z ∈ openSegment 𝕜 x y → x ∈ B
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- A set of points is collinear if and only if they can all be
expressed as multiples of the same vector, added to the same base
point.  -/
collinear_iff_exists_forall_eq_smul_vadd : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : Set P), Collinear k s ↔ ∃ p₀ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- If `ζ` is a primitive `k`-th root of unity with `k` odd, then every power of `ζ` is an even
power of `ζ`.  -/
IsPrimitiveRoot.exists_pow_eq_pow_two_mul : ∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} {ζ : M},
  IsPrimitiveRoot ζ k → Odd k → ∀ (n : ℕ), ∃ m, ζ ^ n = ζ ^ (2 * m)
-- Init.Data.Int.Gcd
Int.gcd_mul_right : ∀ (m n k : ℤ), (m * n).gcd (k * n) = m.gcd k * n.natAbs
-- Lean.Data.Lsp.Capabilities
/-- Capabilities for Lean language server extensions.  -/
Lean.Lsp.ClientCapabilities.lean? : Lean.Lsp.ClientCapabilities → Option Lean.Lsp.LeanClientCapabilities
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.isReflection_simple : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B),
  cs.IsReflection (cs.simple i)
-- Mathlib.FieldTheory.Galois.Basic
IntermediateField.finrank_fixedField_eq_card : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (H : Subgroup Gal(E/F))
  [FiniteDimensional F E], Module.finrank (↥(IntermediateField.fixedField H)) E = Nat.card ↥H
-- Mathlib.FieldTheory.IsRealClosed.Basic
IsRealClosed.exists_eq_pow_of_nonneg : ∀ {R : Type u} [inst : Field R] [IsRealClosed R] [inst_2 : LinearOrder R] [IsStrictOrderedRing R] {x : R},
  0 ≤ x → ∀ {n : ℕ}, n ≠ 0 → ∃ r, x = r ^ n
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatIso.id_hom : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} (F : CategoryTheory.BasedFunctor 𝒳 𝒴),
  (CategoryTheory.BasedNatIso.id F).hom = CategoryTheory.CategoryStruct.id F
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.OfInvertibleFactorial.dpow_comp : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} [inst_1 : DecidablePred fun x => x ∈ I] {n : ℕ},
  IsUnit ↑(n - 1).factorial →
    I ^ n = 0 →
      ∀ {m k : ℕ},
        k ≠ 0 →
          ∀ {x : A},
            x ∈ I →
              DividedPowers.OfInvertibleFactorial.dpow I m (DividedPowers.OfInvertibleFactorial.dpow I k x) =
                ↑(m.uniformBell k) * DividedPowers.OfInvertibleFactorial.dpow I (m * k) x
-- Mathlib.Computability.Primrec.Basic
Primrec.of_eq : ∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] {f g : α → σ},
  Primrec f → (∀ (n : α), f n = g n) → Primrec g
-- Mathlib.ModelTheory.Basic
/-- The type of symbols in a given language.  -/
FirstOrder.Language.Symbols : FirstOrder.Language → Type (max u v)
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag'_blockDiagonal' : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [inst : Zero α] [inst_1 : DecidableEq o]
  (M : (i : o) → Matrix (m' i) (n' i) α), (Matrix.blockDiagonal' M).blockDiag' = M
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.comap_map_comm : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel β γ) {f : α → β} {g : γ → δ}
  (hf : Measurable f), Measurable g → (κ.map g).comap f hf = (κ.comap f hf).map g
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.iso_hom_naturality_assoc : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  {x x' : X} (f : x ⟶ x') {Z : B} (h : G.obj (S.snd.obj x') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (S.fst.map f)) (CategoryTheory.CategoryStruct.comp (S.iso.hom.app x') h) =
    CategoryTheory.CategoryStruct.comp (S.iso.hom.app x) (CategoryTheory.CategoryStruct.comp (G.map (S.snd.map f)) h)
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- **Alias** of the forward direction of `SimpleGraph.isIsolated_compl_iff_isUniversal`. -/
SimpleGraph.IsUniversal.of_isIsolated_compl : ∀ {V : Type u} {G : SimpleGraph V} {v : V}, Gᶜ.IsIsolated v → G.IsUniversal v
-- Mathlib.Analysis.Convex.Topology
/-- If `s` is a convex set, then `a • interior s + b • closure s ⊆ interior s` for all `0 < a`,
`0 ≤ b`, `a + b = 1`. See also `Convex.combo_interior_self_subset_interior` for a weaker version.  -/
Convex.combo_interior_closure_subset_interior : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E},
  Convex 𝕜 s → ∀ {a b : 𝕜}, 0 < a → 0 ≤ b → a + b = 1 → a • interior s + b • closure s ⊆ interior s
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
_private.Mathlib.Analysis.InnerProductSpace.TensorProduct.0.TensorProduct.inner_definite : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  (x : TensorProduct 𝕜 E F), inner 𝕜 x x = 0 → x = 0
-- Mathlib.Data.Num.Basic
Num.pos.inj : ∀ {a a_1 : PosNum}, Num.pos a = Num.pos a_1 → a = a_1
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.norm_cpow_eq_rpow_re_of_pos : ∀ {x : ℝ}, 0 < x → ∀ (y : ℂ), ‖↑x ^ y‖ = x ^ y.re
-- Mathlib.Analysis.Complex.MeanValue
/-- The **Generalized Mean Value Property** of complex differentiable functions: If `f : ℂ → E` is
complex differentiable at all points of a closed disc of radius `R` and center `c`, then for every
point `w` in the disk, the circle average `circleAverage (fun z ↦ ((z - c) * (z - w)⁻¹) • f z) c R`
equals `f w`.
 -/
DiffContOnCl.circleAverage_smul_div : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {R : ℝ}
  {c w : ℂ},
  DiffContOnCl ℂ f (Metric.ball c |R|) →
    w ∈ Metric.ball c |R| → Real.circleAverage (fun z => ((z - c) / (z - w)) • f z) c R = f w
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso_inv_τ₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesEIso._auto_3),
  (X.cokernelSequenceCyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv.τ₁ =
    CategoryTheory.CategoryStruct.id ((X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ f₃))
-- Lean.Data.AssocList
Lean.AssocList.brecOn.go : {α : Type u} →
  {β : Type v} →
    {motive : Lean.AssocList α β → Sort u_1} →
      (t : Lean.AssocList α β) →
        ((t : Lean.AssocList α β) → Lean.AssocList.below t → motive t) → motive t ×' Lean.AssocList.below t
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.instHasIdealSupport : ∀ {F : Type u_2} [inst : Field F] (P : RingPreordering F), P.HasIdealSupport
-- Lean.Util.CollectLevelMVars
Lean.CollectLevelMVars.State.visitedLevel : Lean.CollectLevelMVars.State → Lean.LevelSet
-- Mathlib.GroupTheory.GroupAction.Basic
MulAction.fixedPoints_of_subsingleton : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [Subsingleton α],
  MulAction.fixedPoints G α = Set.univ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_eq_some : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [Std.LawfulEqOrd α], t.WF → ∀ {k : α}, k ∈ t → t.getKey? k = some k
-- Mathlib.Algebra.Lie.Weights.Linear
LieModule.Weight.toLinear_apply : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : LieModule.LinearWeights R L M] (χ : LieModule.Weight R L M) (a : L),
  (LieModule.Weight.toLinear R L M χ) a = χ a
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.range_le : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (S : StarSubalgebra R A),
  Set.range ⇑(algebraMap R A) ⊆ ↑S
-- Init.Data.BitVec.Lemmas
BitVec.add_right_eq_self : ∀ {w : ℕ} {x y : BitVec w}, x + y = x ↔ y = 0#w
-- Lean.Compiler.LCNF.Types
Lean.Compiler.LCNF.ImpureType.object : Lean.Expr
-- Mathlib.Order.TypeTags
_private.Mathlib.Order.TypeTags.0.WithTop.instRepr.match_1.splitter : {α : Type u_1} →
  (motive : WithTop α → Sort u_2) → (o : WithTop α) → (Unit → motive none) → ((a : α) → motive (some a)) → motive o
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_10 : HSub Std.Time.Millisecond.Offset Std.Time.Day.Offset Std.Time.Millisecond.Offset
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_comap_eq : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (f : F) (S : Submonoid N), Submonoid.map f (Submonoid.comap f S) = S ⊓ MonoidHom.mrange f
-- Mathlib.MeasureTheory.Measure.Regular
/-- A measure `μ` is inner regular for finite measure sets with respect to compact sets:
for any measurable set `s` with finite measure, then `μ(s) = sup {μ(K) | K ⊆ s compact}`.
The main interest of this class is that it is satisfied for both natural Haar measures (the
regular one and the inner regular one).  -/
MeasureTheory.Measure.InnerRegularCompactLTTop : {α : Type u_1} → [inst : MeasurableSpace α] → [TopologicalSpace α] → MeasureTheory.Measure α → Prop
-- Mathlib.Algebra.Algebra.Pi
/-- The opposite of a direct product is isomorphic to the direct product of the opposites as
algebras.  -/
AlgEquiv.piMulOpposite : (R : Type u_3) →
  {ι : Type u_4} →
    (A₁ : ι → Type u_5) →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → Semiring (A₁ i)] →
          [inst_2 : (i : ι) → Algebra R (A₁ i)] → ((i : ι) → A₁ i)ᵐᵒᵖ ≃ₐ[R] (i : ι) → (A₁ i)ᵐᵒᵖ
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.oreSub.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X] (r : X) (s : ↥S), r -ₒ s = Quotient.mk' (r, s)
-- Mathlib.NumberTheory.ModularForms.LFunction
_private.Mathlib.NumberTheory.ModularForms.LFunction.0.ModularForm.tendsto_ofComplex_I_mul_atTop_atImInfty : Filter.Tendsto (fun t => ↑UpperHalfPlane.ofComplex (Complex.I * ↑t)) Filter.atTop UpperHalfPlane.atImInfty
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.State.annotations : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.State → Lean.PrettyPrinter.Delaborator.OptionsPerPos
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapShortComplexH2_id_comp_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep.{u_1, u, u} k G} (φ : A ⟶ B) (ψ : B ⟶ C)
  {Z : CategoryTheory.ShortComplex (ModuleCat k)} (h : groupCohomology.shortComplexH2 C ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (groupCohomology.mapShortComplexH2 (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ)) h =
    CategoryTheory.CategoryStruct.comp (groupCohomology.mapShortComplexH2 (MonoidHom.id G) φ)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.mapShortComplexH2 (MonoidHom.id G) ψ) h)
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors' : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {t : R} {n : ℕ},
  p ≠ 0 →
    (∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t) →
      (∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R) → n < Polynomial.rootMultiplicity t p
-- Init.Data.Order.Lemmas
Std.LawfulOrderLeftLeaningMin.of_eq : ∀ {α : Type u} [inst : LE α] [inst_1 : Min α] [inst_2 : DecidableLE α],
  (∀ (a b : α), a ⊓ b = if a ≤ b then a else b) → Std.LawfulOrderLeftLeaningMin α
-- Std.Data.ByteSlice
/-- Checks if the byte slice contains a specific byte value.

Returns `true` if any byte in the slice equals the given value, `false` otherwise.
 -/
ByteSlice.contains : ByteSlice → UInt8 → Bool
-- Mathlib.Data.Seq.Basic
Stream'.Seq1.ret.eq_1 : ∀ {α : Type u} (a : α), Stream'.Seq1.ret a = (a, Stream'.Seq.nil)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.sigmaComparison_map_desc_assoc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : β → C)
  [inst_2 : CategoryTheory.Limits.HasCoproduct f] [inst_3 : CategoryTheory.Limits.HasCoproduct fun b => G.obj (f b)]
  (P : C) (g : (j : β) → f j ⟶ P) {Z : D} (h : G.obj P ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.sigmaComparison G f)
      (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Sigma.desc g)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.desc fun j => G.map (g j)) h
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- In a simplicial set, an edge from a vertex `x₀` to `x₁` is
a `1`-simplex with prescribed `0`-dimensional faces.  -/
SSet.Edge.edge : {X : SSet} → {x₀ x₁ : X.obj (Opposite.op { len := 0 })} → SSet.Edge x₀ x₁ → X.obj (Opposite.op { len := 1 })
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- Given an adjunction `L ⊣ R`, if `R ⋙ L` is isomorphic to the identity functor, then `R` is
fully faithful.
 -/
CategoryTheory.Adjunction.fullyFaithfulROfCompIsoId : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} →
          {R : CategoryTheory.Functor D C} → (L ⊣ R) → (R.comp L ≅ CategoryTheory.Functor.id D) → R.FullyFaithful
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Lazy entries that still have to be evaluated.  -/
Lean.Meta.RefinedDiscrTree.Trie.pending : {α : Type} → Lean.Meta.RefinedDiscrTree.Trie α → Array (Lean.Meta.RefinedDiscrTree.LazyEntry × α)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.QuasiCompact.of_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
  [AlgebraicGeometry.QuasiCompact (CategoryTheory.CategoryStruct.comp f g)] [AlgebraicGeometry.QuasiSeparated g],
  AlgebraicGeometry.QuasiCompact f
-- Mathlib.CategoryTheory.HomCongr
/-- If `X` is isomorphic to `X₁` and `Y` is isomorphic to `Y₁`, then
there is a bijection between `X ≅ Y` and `X₁ ≅ Y₁`.  -/
CategoryTheory.Iso.isoCongr : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {X₁ Y₁ X₂ Y₂ : C} → (X₁ ≅ X₂) → (Y₁ ≅ Y₂) → (X₁ ≅ Y₁) ≃ (X₂ ≅ Y₂)
-- Init.Data.Vector.Lemmas
Vector.contains_empty : ∀ {α : Type u_1} {a : α} [inst : BEq α], #v[].contains a = false
-- Lean.Data.Json.Basic
Lean.JsonNumber.mk.sizeOf_spec : ∀ (mantissa : ℤ) (exponent : ℕ),
  sizeOf { mantissa := mantissa, exponent := exponent } = 1 + sizeOf mantissa + sizeOf exponent
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.etale_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.Etale f ↔
    ∀ {U : Y.Opens},
      AlgebraicGeometry.IsAffineOpen U →
        ∀ {V : X.Opens},
          AlgebraicGeometry.IsAffineOpen V →
            ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
              (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).Etale
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.derives_reverse : ∀ {T : Type u_1} {g : ContextFreeGrammar T} {u v : List (Symbol T g.NT)},
  g.reverse.Derives u.reverse v.reverse ↔ g.Derives u v
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitCandidateAnchors.mk.inj : ∀ {candidates : Array Lean.Meta.Grind.SplitCandidateWithAnchor} {numDigits : ℕ}
  {candidates_1 : Array Lean.Meta.Grind.SplitCandidateWithAnchor} {numDigits_1 : ℕ},
  { candidates := candidates, numDigits := numDigits } = { candidates := candidates_1, numDigits := numDigits_1 } →
    candidates = candidates_1 ∧ numDigits = numDigits_1
-- Mathlib.Data.Finset.Union
Finset.biUnion_filter_eq_of_maps_to : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : DecidableEq α] {s : Finset α} {t : Finset β}
  {f : α → β}, (∀ x ∈ s, f x ∈ t) → (t.biUnion fun a => {c ∈ s | f c = a}) = s
-- Mathlib.Order.Antisymmetrization
AntisymmRel.le_congr : ∀ {α : Type u_1} {a b c d : α} [inst : Preorder α],
  AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → AntisymmRel (fun x1 x2 => x1 ≤ x2) c d → (a ≤ c ↔ b ≤ d)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
_private.Mathlib.Topology.ContinuousMap.Bounded.Normed.0.zpowRec.match_1.eq_2 : ∀ {G : Type u_2} (motive : ℤ → G → Sort u_1) (n : ℕ) (a : G) (h_1 : (n : ℕ) → (a : G) → motive (Int.ofNat n) a)
  (h_2 : (n : ℕ) → (a : G) → motive (Int.negSucc n) a),
  (match Int.negSucc n, a with
    | Int.ofNat n, a => h_1 n a
    | Int.negSucc n, a => h_2 n a) =
    h_2 n a
-- Aesop.Tree.Data
Aesop.Goal.instHashable : Hashable Aesop.Goal
-- Mathlib.MeasureTheory.Group.Convolution
/-- Convolution of a measure μ with the zero measure returns the zero
measure.  -/
MeasureTheory.Measure.conv_zero : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] (μ : MeasureTheory.Measure M), μ.conv 0 = 0
-- Mathlib.Analysis.CStarAlgebra.Spectrum
spectrum.subset_circle_of_unitary : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] {E : Type u_2} [inst_1 : NormedRing E] [inst_2 : StarRing E] [CStarRing E]
  [inst_4 : NormedAlgebra 𝕜 E] [CompleteSpace E] {u : E}, u ∈ unitary E → spectrum 𝕜 u ⊆ Metric.sphere 0 1
-- Mathlib.Data.PFunctor.Multivariate.W
MvPFunctor.WPath.child.injEq : ∀ {n : ℕ} {P : MvPFunctor.{u} (n + 1)} (a : P.A) (f : P.last.B a → P.last.W) (i : Fin2 n) (j : P.last.B a)
  (c : P.WPath (f j) i) (j_1 : P.last.B a) (c_1 : P.WPath (f j_1) i),
  (MvPFunctor.WPath.child a f i j c = MvPFunctor.WPath.child a f i j_1 c_1) = (j = j_1 ∧ c ≍ c_1)
-- Mathlib.Algebra.Order.Module.Defs
le_smul_of_one_le_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Monoid α] [inst_1 : Zero β] [inst_2 : MulAction α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [SMulPosMono α β], 0 ≤ b → 1 ≤ a → b ≤ a • b
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.coeff_rename_embDomain : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : σ ↪ τ) (φ : MvPolynomial σ R) (d : σ →₀ ℕ),
  MvPolynomial.coeff (Finsupp.embDomain f d) ((MvPolynomial.rename ⇑f) φ) = MvPolynomial.coeff d φ
-- Mathlib.Order.Defs.LinearOrder
le_of_not_gt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, ¬b < a → a ≤ b
-- Mathlib.RingTheory.IsGaloisGroup.Defs
IsGaloisGroup.of_mulEquiv : ∀ {G : Type u_1} {A : Type u_2} {B : Type u_4} [inst : Group G] [inst_1 : CommSemiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra A B] [inst_4 : MulSemiringAction G B] [hG : IsGaloisGroup G A B] {H : Type u_5} [inst_5 : Group H]
  [inst_6 : MulSemiringAction H B] (e : H ≃* G), (∀ (h : H) (x : B), e h • x = h • x) → IsGaloisGroup H A B