mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
StrictAntiOn.add_const : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} {s : Set β}
  [AddRightStrictMono α], StrictAntiOn f s → ∀ (c : α), StrictAntiOn (fun x => f x + c) s
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- The `𝕜`-subalgebra of elements of `∀ i : α, B i` whose `lp` norm is finite. This is `lp E ∞`,
with extra structure.  -/
lpInftySubalgebra : (𝕜 : Type u_1) →
  {I : Type u_5} →
    (B : I → Type u_6) →
      [inst : NormedField 𝕜] →
        [inst_1 : (i : I) → NormedRing (B i)] →
          [inst_2 : (i : I) → NormedAlgebra 𝕜 (B i)] → [∀ (i : I), NormOneClass (B i)] → Subalgebra 𝕜 (PreLp B)
-- Mathlib.Topology.Covering.Quotient
AddSubgroup.isAddQuotientCoveringMap : ∀ {G : Type u_4} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] (S : AddSubgroup G),
  IsDiscrete ↑S → IsAddQuotientCoveringMap QuotientAddGroup.mk ↥S.op
-- Std.Data.ExtTreeSet.Basic
/-- Tries to retrieve the largest element that is less than or equal to the
given element, returning `fallback` if no such element exists.
 -/
Std.ExtTreeSet.getLED : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → α → α → α
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_neg_iff : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β}, MeasureTheory.Integrable (-f) μ ↔ MeasureTheory.Integrable f μ
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.height_of_isClosed : ∀ {X : AlgebraicGeometry.Scheme} {x : ↥X}, IsClosed {x} → Order.height x = 0
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.forall_mem_keys_iff_forall_contains_getKey : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF → ∀ {p : α → Prop}, (∀ k ∈ (↑m).keys, p k) ↔ ∀ (k : α) (h : m.contains k = true), p (m.getKey k h)
-- Mathlib.AlgebraicGeometry.Sites.Etale
AlgebraicGeometry.Scheme.ofArrows_mem_smallEtaleTopology_iff : ∀ {X : AlgebraicGeometry.Scheme} {W : X.Etale} {ι : Type u_1} {Z : ι → X.Etale} (f : (i : ι) → Z i ⟶ W),
  CategoryTheory.Sieve.ofArrows Z f ∈ X.smallEtaleTopology W ↔ ⋃ i, Set.range ⇑(f i).left = Set.univ
-- Mathlib.Order.Interval.Finset.Fin
Fin.Icc_sub_one_eq_Ico : ∀ {n : ℕ} {a b : Fin n}, 0 < b → Finset.Icc a (b - 1) = Finset.Ico a b
-- Init.PropLemmas
Decidable.peirce : ∀ (a b : Prop) [Decidable a], ((a → b) → a) → a
-- Mathlib.Algebra.Order.Hom.TypeTags
/-- Reinterpret `G ≃+o Additive H` as `Multiplicative G ≃*o H`.  -/
OrderAddMonoidIso.toMultiplicativeLeft : {G : Type u_1} →
  {H : Type u_2} →
    [inst : AddCommMonoid G] →
      [inst_1 : PartialOrder G] →
        [inst_2 : CommMonoid H] → [inst_3 : PartialOrder H] → (G ≃+o Additive H) ≃ (Multiplicative G ≃*o H)
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charmatrix.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} {inst_1 : DecidableEq n} [inst_2 : DecidableEq n]
  [inst_3 : Fintype n] (M M_1 : Matrix n n R),
  M = M_1 → ∀ (a a_1 : n), a = a_1 → ∀ (a_2 a_3 : n), a_2 = a_3 → M.charmatrix a a_2 = M_1.charmatrix a_1 a_3
-- Lean.Meta.Tactic.Grind.Internalize
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.internalizeImpl : Lean.Expr → ℕ → optParam (Option Lean.Expr) none → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.div_empty : ∀ {α : Type u_2} [inst : Div α] {s : Set α}, s / ∅ = ∅
-- Init.Data.Int.LemmasAux
Int.sub_max_sub_left : ∀ (a b c : ℤ), max (a - b) (a - c) = a - min b c
-- Mathlib.Algebra.BigOperators.Finprod
/-- The sum of `f y` over `y ∈ g '' s` equals the sum of `f (g i)` over `s` provided that
`g` is injective on `s ∩ support (f ∘ g)`.  -/
finsum_mem_image' : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s : Set β} {g : β → α},
  Set.InjOn g (s ∩ Function.support (f ∘ g)) → ∑ᶠ (i : α) (_ : i ∈ g '' s), f i = ∑ᶠ (j : β) (_ : j ∈ s), f (g j)
-- Mathlib.Probability.Moments.Variance
/-- **Chebyshev's inequality** for `ℝ≥0∞`-valued variance.  -/
ProbabilityTheory.meas_ge_le_evariance_div_sq : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ},
  MeasureTheory.AEStronglyMeasurable X μ →
    ∀ {c : NNReal}, c ≠ 0 → μ {ω | ↑c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤ ProbabilityTheory.evariance X μ / ↑c ^ 2
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_eq_isEmpty_erase_and_not_contains : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  (k : α),
  t.isEmpty = ((Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.isEmpty && !Std.DTreeMap.Internal.Impl.contains k t)
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.measurable_bind' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {g : α → MeasureTheory.Measure β},
  Measurable g → Measurable fun m => m.bind g
-- Mathlib.Geometry.Manifold.Algebra.SMul
/-- Basic typeclass stating that the additive action of `G` on `M` is Cⁿ as a function `G × M → M`.
Unlike with `ContMDiffAdd` (the class stating that addition `G × G → G` within a single type `G` is
Cⁿ), we do not extend `IsManifold` because `ContMDiffVAdd` contains more
explicit arguments than `IsManifold` and so `ContMDiffVAdd.toIsManifold` could not be an instance
anyway: this means that in order for `ContMDiffVAdd` to be meaningful, smoothness of `G` and `M`
have to be required separately. For example, to state that `G` is a Cⁿ additive Lie group with a Cⁿ
additive action on a Cⁿ manifold `M`, one can use the typeclasses
`[LieAddGroup I n G] [IsManifold I' n M] [ContMDiffVAdd I I' n G M]`.  -/
ContMDiffVAdd : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              ModelWithCorners 𝕜 E H →
                {H' : Type u_4} →
                  [inst_4 : TopologicalSpace H'] →
                    {E' : Type u_5} →
                      [inst_5 : NormedAddCommGroup E'] →
                        [inst_6 : NormedSpace 𝕜 E'] →
                          ModelWithCorners 𝕜 E' H' →
                            WithTop ℕ∞ →
                              (G : Type u_6) →
                                [inst : TopologicalSpace G] →
                                  [ChartedSpace H G] →
                                    (M : Type u_7) →
                                      [inst : TopologicalSpace M] → [ChartedSpace H' M] → [VAdd G M] → Prop
-- Mathlib.RingTheory.Polynomial.Opposites
Polynomial.coeff_opRingEquiv : ∀ {R : Type u_1} [inst : Semiring R] (p : (Polynomial R)ᵐᵒᵖ) (n : ℕ),
  ((Polynomial.opRingEquiv R) p).coeff n = MulOpposite.op ((MulOpposite.unop p).coeff n)
-- Mathlib.RingTheory.Localization.BaseChange
/-- If `A` is a localization of `R`, tensoring an `A`-algebra with `A` over `R` does nothing.  -/
IsLocalization.algebraLid : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Submonoid R) →
      (A : Type u_2) →
        [inst_1 : CommSemiring A] →
          [inst_2 : Algebra R A] →
            [IsLocalization S A] →
              (B : Type u_5) →
                [inst_4 : Semiring B] →
                  [inst_5 : Algebra R B] → [inst_6 : Algebra A B] → [IsScalarTower R A B] → TensorProduct R A B ≃ₐ[A] B
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb'_toNat : ∀ {n : ℕ} (s m : ℕ) (x : BitVec n), (BitVec.extractLsb' s m x).toNat = x.toNat >>> s % 2 ^ m
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The composition of two ContinuousAddEquiv.  -/
ContinuousAddEquiv.trans : {M : Type u_1} →
  {N : Type u_2} →
    [inst : TopologicalSpace M] →
      [inst_1 : TopologicalSpace N] →
        [inst_2 : Add M] →
          [inst_3 : Add N] →
            {L : Type u_3} → [inst_4 : Add L] → [inst_5 : TopologicalSpace L] → M ≃ₜ+ N → N ≃ₜ+ L → M ≃ₜ+ L
-- Std.Time.Internal.Bounded
/-- Convert a `Fin` to a `Bounded.LE`.
 -/
Std.Time.Internal.Bounded.LE.ofFin : {hi : ℕ} → Fin hi.succ → Std.Time.Internal.Bounded.LE 0 ↑hi
-- Mathlib.Data.Finset.Sym
Finset.monotone_sym2 : ∀ {α : Type u_1}, Monotone Finset.sym2
-- Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Dynamics.mem_ball_dynEntourage_comp : ∀ {X : Type u_1} (T : X → X) (n : ℕ) {U : SetRel X X} [U.IsSymm] (x y : X),
  (UniformSpace.ball x (Dynamics.dynEntourage T U n) ∩ UniformSpace.ball y (Dynamics.dynEntourage T U n)).Nonempty →
    x ∈ UniformSpace.ball y (Dynamics.dynEntourage T (U.comp U) n)
-- Init.Data.Fin.Lemmas
Fin.add_def : ∀ {n : ℕ} (a b : Fin n), a + b = ⟨(↑a + ↑b) % n, ⋯⟩
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.valuation_surjective : ∀ {K : Type u_3} [inst : DivisionRing K] [inst_1 : ValuativeRel K], Function.Surjective ⇑(ValuativeRel.valuation K)
-- Mathlib.MeasureTheory.Group.LIntegral
/-- Translating a function by left-multiplication does not change its Lebesgue integral
with respect to a left-invariant measure.  -/
MeasureTheory.lintegral_mul_left_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : Group G] [MeasurableMul G]
  [μ.IsMulLeftInvariant] (f : G → ENNReal) (g : G), ∫⁻ (x : G), f (g * x) ∂μ = ∫⁻ (x : G), f x ∂μ
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- **Alias** of `FunLike.coe_neg`. -/
MeasureTheory.VectorMeasure.coe_neg : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Neg F] [inst_2 : Neg β]
  [IsNegApply F α β] (f : F), ⇑(-f) = -⇑f
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.ofPrime_idealOfLE : ∀ {K : Type u} [inst : Field K] (R S : ValuationSubring K) (h : R ≤ S), R.ofPrime (R.idealOfLE S h) = S
-- Init.Data.Nat.Lemmas
Nat.add_left_inj : ∀ {m k n : ℕ}, m + n = k + n ↔ m = k
-- Mathlib.Topology.Compactification.StoneCech
instTopologicalSpacePreStoneCech : {α : Type u} → [inst : TopologicalSpace α] → TopologicalSpace (PreStoneCech α)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd_pullback_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Y : C) (Z : CategoryTheory.Over Y),
  (CategoryTheory.ChosenPullbacksAlong.pullback (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)).obj Z =
    CategoryTheory.Over.mk (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X Z.hom)
-- Mathlib.Data.Nat.Prime.Factorial
Nat.coprime_factorial_iff : ∀ {m n : ℕ}, m ≠ 1 → (m.Coprime n.factorial ↔ n < m.minFac)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.erase.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (p : SkewPolynomial R),
  SkewPolynomial.erase n p = (SkewMonoidAlgebra.erase (Multiplicative.ofAdd n)) p
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.norm.eq_2 : ∀ (k : ℤ) (v : Lean.Grind.Linarith.Var) (p_2 : Lean.Grind.Linarith.Poly),
  (Lean.Grind.Linarith.Poly.add k v p_2).norm = Lean.Grind.Linarith.Poly.insert k v p_2.norm
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.topEquiv_symm_apply_coe : ∀ {M : Type u_1} [inst : Mul M] (x : M), ↑(Subsemigroup.topEquiv.symm x) = x
-- Mathlib.Data.Finset.MulAntidiagonal
Finset.isPWO_support_mulAntidiagonal : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelMonoid α] {s t : Set α}
  {hs : s.IsPWO} {ht : t.IsPWO}, {a | (Finset.mulAntidiagonal hs ht a).Nonempty}.IsPWO
-- Mathlib.Algebra.Homology.ConcreteCategory
/-- In the short exact sequence of complexes
```
       0            0            0
       |            |            |
       v            v            v
...-> X_1,i -----> X_1,j --d--> X_1,k ->...
       |            |            |
       |          f |            |
       v            v            v
...-> X_2,i --d--> X_2,j -----> X_2,k ->...
       |            |            |
       v            v            v
...-> X_3,i -----> X_3,j -----> X_3,k ->...
       |            |            |
       v            v            v
       0            0            0
```
if `x₁ ∈ X_1,j` and `x₂ ∈ X_2,i` and if `f(x₁) = d(x₂)` then `d(x₁) = 0`.  -/
CategoryTheory.ShortComplex.ShortExact.d_eq_zero_of_f_eq_d_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.HasForget₂ C Ab] [inst_4 : CategoryTheory.Abelian C]
  [inst_5 : (CategoryTheory.forget₂ C Ab).Additive] [(CategoryTheory.forget₂ C Ab).PreservesHomology] {ι : Type u_2}
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)},
  S.ShortExact →
    ∀ (i j : ι) (x₂ : ↑((CategoryTheory.forget₂ C Ab).obj (S.X₂.X i)))
      (x₁ : ↑((CategoryTheory.forget₂ C Ab).obj (S.X₁.X j))),
      (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map (S.f.f j))) x₁ =
          (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map (S.X₂.d i j))) x₂ →
        ∀ (k : ι), (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map (S.X₁.d j k))) x₁ = 0
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
CategoryTheory.Limits.hasBinaryProduct_zero_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.Limits.HasZeroMorphisms C] (X : C), CategoryTheory.Limits.HasBinaryProduct X 0
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.instIteratorRxcIteratorIdSigma : {α : Type u} →
  {β : α → Type v} → [inst : Ord α] → Std.Iterator (Std.DTreeMap.Internal.RxcIterator α β) Id ((a : α) × β a)
-- Mathlib.Tactic.DepRewrite
/-- Apply `rewrite!` to the goal.  -/
Mathlib.Tactic.DepRewrite.Conv.depRewriteTarget : Lean.Syntax → Bool → optParam Mathlib.Tactic.DepRewrite.Config { } → Lean.Elab.Tactic.TacticM Unit
-- Init.Data.Array.Find
Array.findIdx?_eq_some_iff_findIdx_eq : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool} {i : ℕ},
  Array.findIdx? p xs = some i ↔ i < xs.size ∧ Array.findIdx p xs = i
-- Init.Data.Range.Polymorphic.Lemmas
Std.toList_roo_eq_toList_rco_of_isSome_succ? : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α] {lo hi : α} (h : (Std.PRange.succ? lo).isSome = true),
  (lo<...hi).toList = (((Std.PRange.succ? lo).get h)...hi).toList
-- Mathlib.CategoryTheory.ObjectProperty.Equivalence
CategoryTheory.Equivalence.congrFullSubcategory_inverse : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {P : CategoryTheory.ObjectProperty C} {Q : CategoryTheory.ObjectProperty D} (e : C ≌ D)
  [inst_2 : Q.IsClosedUnderIsomorphisms] (h : Q.inverseImage e.functor = P),
  (e.congrFullSubcategory h).inverse = P.lift (Q.ι.comp e.inverse) ⋯
-- Mathlib.Data.Finset.Range
Finset.range_subset_range : ∀ {n m : ℕ}, Finset.range n ⊆ Finset.range m ↔ n ≤ m
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.fg_bot : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E], ⊥.FG
-- Mathlib.Algebra.Module.Submodule.Range
Submodule.coe_mapIic_apply : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M)
  (q : Submodule R ↥p), ↑(p.mapIic q) = Submodule.map p.subtype q
-- Lean.Namespace
/-- Environment extension for tracking all `namespace` declared by users.
 -/
_private.Lean.Namespace.0.Lean.namespacesExt : Lean.PersistentEnvExtension Lean.Name Lean.Name Lean.State✝
-- Mathlib.Data.Finset.Sum
Finset.map_disjSum : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Finset α} {t : Finset β} (f : α ⊕ β ↪ γ),
  Finset.map f (s.disjSum t) =
    (Finset.map (Function.Embedding.inl.trans f) s).disjUnion (Finset.map (Function.Embedding.inr.trans f) t) ⋯
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_snd_comp_fst_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {W X Y Z : C} (g : W ⟶ X) (g' : Y ⟶ Z),
  CategoryTheory.CartesianMonoidalCategory.lift
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd W Y) g')
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst W Y) g) =
    CategoryTheory.CategoryStruct.comp (β_ W Y).hom (CategoryTheory.MonoidalCategoryStruct.tensorHom g' g)
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.weightEquiv_inv : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (g : P.Aut),
  RootPairing.Equiv.weightEquiv P P g⁻¹ = (RootPairing.Equiv.weightEquiv P P g)⁻¹
-- Mathlib.Algebra.Polynomial.Roots
/-- The product `∏ (X - a)` for `a` inside the multiset `p.roots` divides `p`.  -/
Polynomial.prod_multiset_X_sub_C_dvd : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (p : Polynomial R),
  (Multiset.map (fun a => Polynomial.X - Polynomial.C a) p.roots).prod ∣ p
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
/-- The distortion of a tagged prepartition is the maximum of distortions of its boxes.  -/
BoxIntegral.TaggedPrepartition.distortion : {ι : Type u_1} → {I : BoxIntegral.Box ι} → BoxIntegral.TaggedPrepartition I → [Fintype ι] → NNReal
-- Mathlib.RingTheory.IsTensorProduct
IsBaseChange.eq_1 : ∀ {R : Type u_1} {M : Type v₁} {N : Type v₂} (S : Type v₃) [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] (f : M →ₗ[R] N),
  IsBaseChange S f = IsTensorProduct (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] N))).flip f))
-- Init.Data.UInt.Lemmas
UInt64.toUSize_sub : ∀ (a b : UInt64), (a - b).toUSize = a.toUSize - b.toUSize
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Matrix.ProjectiveSpecialLinearGroup.toPGL_mk : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  (g : Matrix.SpecialLinearGroup n R),
  Matrix.ProjectiveSpecialLinearGroup.toPGL ↑g = Matrix.ProjGenLinGroup.mk (Matrix.SpecialLinearGroup.toGL g)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- A homomorphism from a uniform additive group to a discrete uniform additive group
is continuous if and only if its kernel is open.  -/
IsUniformAddGroup.uniformContinuous_iff_isOpen_ker : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {hom : Type u_3}
  [inst_3 : UniformSpace β] [DiscreteTopology β] [inst_5 : AddGroup β] [IsUniformAddGroup β] [inst_7 : FunLike hom α β]
  [inst_8 : AddMonoidHomClass hom α β] {f : hom}, UniformContinuous ⇑f ↔ IsOpen ↑(↑f).ker
-- Mathlib.Topology.Algebra.Monoid
Filter.Tendsto.units.eq_1 : ∀ {ι : Type u_1} {N : Type u_4} [inst : TopologicalSpace N] [inst_1 : Monoid N] [inst_2 : ContinuousMul N]
  [inst_3 : T2Space N] {f : ι → Nˣ} {r₁ r₂ : N} {l : Filter ι} [inst_4 : l.NeBot]
  (h₁ : Filter.Tendsto (fun x => ↑(f x)) l (nhds r₁)) (h₂ : Filter.Tendsto (fun x => ↑(f x)⁻¹) l (nhds r₂)),
  h₁.units h₂ = { val := r₁, inv := r₂, val_inv := ⋯, inv_val := ⋯ }
-- Mathlib.Algebra.Ring.InjSurj
/-- Pushforward a `NonUnitalNonAssocRing` instance along a surjective function.  -/
Function.Surjective.nonUnitalNonAssocRing : {R : Type u_1} →
  {S : Type u_2} →
    (f : R → S) →
      Function.Surjective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : Neg S] →
                [inst_4 : Sub S] →
                  [inst_5 : SMul ℕ S] →
                    [inst_6 : SMul ℤ S] →
                      [inst_7 : NonUnitalNonAssocRing R] →
                        f 0 = 0 →
                          (∀ (x y : R), f (x + y) = f x + f y) →
                            (∀ (x y : R), f (x * y) = f x * f y) →
                              (∀ (x : R), f (-x) = -f x) →
                                (∀ (x y : R), f (x - y) = f x - f y) →
                                  (∀ (n : ℕ) (x : R), f (n • x) = n • f x) →
                                    (∀ (n : ℤ) (x : R), f (n • x) = n • f x) → NonUnitalNonAssocRing S
-- Mathlib.Topology.Algebra.Group.Pointwise
IsClosed.add_left_of_isCompact : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {s t : Set G},
  IsClosed t → IsCompact s → IsClosed (s + t)
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.coroot_reflectionPerm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i j : ι),
  P.coroot ((P.reflectionPerm i) j) = (P.coreflection i) (P.coroot j)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- The right inclusion into the disjoint union.  -/
CategoryTheory.PreZeroHypercover.sumInr : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} → (E : CategoryTheory.PreZeroHypercover S) → (F : CategoryTheory.PreZeroHypercover S) → F.Hom (E.sum F)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
PosMulStrictMono.toPosMulMono : ∀ {α : Type u_1} [inst : MulZeroClass α] [inst_1 : PartialOrder α] [PosMulStrictMono α], PosMulMono α
-- Lean.Meta.Tactic.Util
/-- Return all propositions in the local context.  -/
Lean.Meta.getPropHyps : Lean.MetaM (Array Lean.FVarId)
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.mk.injEq : ∀ {X : Type u_7} {Y : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (toPartialEquiv : PartialEquiv X Y) (continuousOn_toFun : ContinuousOn (↑toPartialEquiv) toPartialEquiv.source)
  (continuousOn_invFun : ContinuousOn toPartialEquiv.invFun toPartialEquiv.target) (toPartialEquiv_1 : PartialEquiv X Y)
  (continuousOn_toFun_1 : ContinuousOn (↑toPartialEquiv_1) toPartialEquiv_1.source)
  (continuousOn_invFun_1 : ContinuousOn toPartialEquiv_1.invFun toPartialEquiv_1.target),
  ({ toPartialEquiv := toPartialEquiv, continuousOn_toFun := continuousOn_toFun,
        continuousOn_invFun := continuousOn_invFun } =
      { toPartialEquiv := toPartialEquiv_1, continuousOn_toFun := continuousOn_toFun_1,
        continuousOn_invFun := continuousOn_invFun_1 }) =
    (toPartialEquiv = toPartialEquiv_1)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.module : {m : Type u_2} →
  {n : Type u_3} →
    {R : Type u_7} →
      {α : Type v} → [inst : Semiring R] → [inst_1 : AddCommMonoid α] → [Module R α] → Module R (Matrix m n α)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Two products which differ by an equivalence in the indexing type,
and up to isomorphism in the factors, are isomorphic.
 -/
CategoryTheory.Limits.Pi.whiskerEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u_1} →
      {K : Type u_2} →
        {f : J → C} →
          {g : K → C} →
            (e : J ≃ K) →
              ((j : J) → g (e j) ≅ f j) →
                [inst_1 : CategoryTheory.Limits.HasProduct f] →
                  [inst_2 : CategoryTheory.Limits.HasProduct g] → ∏ᶜ f ≅ ∏ᶜ g
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_ofNat' : ∀ (n : ℕ), (UInt64.ofNat n).toBitVec = BitVec.ofNat 64 n
-- Mathlib.Data.FP.Basic
FP.Float.Zero.valid : ∀ [C : FP.FloatCfg], FP.ValidFinite FP.emin 0