mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.Egorov
MeasureTheory.Egorov.measure_inter_notConvergentSeq_eq_zero : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [inst : PseudoEMetricSpace β]
  {μ : MeasureTheory.Measure α} {s : Set α} {f : ι → α → β} {g : α → β} [inst_1 : SemilatticeSup ι] [Nonempty ι],
  (∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
    ∀ (n : ℕ), μ (s ∩ ⋂ j, MeasureTheory.Egorov.notConvergentSeq f g n j) = 0
-- Init.Control.Option
OptionT.instMonadExceptOfPUnit : {m : Type u → Type v} → [Monad m] → MonadExceptOf PUnit.{u_1 + 1} (OptionT m)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- A SubAddAction is a set which is closed under scalar multiplication.  -/
SubAddAction : (R : Type u) → (M : Type v) → [VAdd R M] → Type v
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.norm_algebraMap : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] (r : R),
  QuadraticAlgebra.norm ((algebraMap R (QuadraticAlgebra R a b)) r) = r ^ 2
-- Init.Data.Slice.Array.Lemmas
Array.mkSlice_ric_eq_mkSlice_rio_min : ∀ {α : Type u_1} {xs : Array α} {hi : ℕ},
  (Std.Ric.Sliceable.mkSlice xs *...=hi) = Std.Rio.Sliceable.mkSlice xs *...min (hi + 1) xs.size
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.Hom.ext : ∀ {A B : CommMonCat} {x y : A.Hom B}, x.hom' = y.hom' → x = y
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- Given a reflexive quiver `V` and a category `C`, this is the bijection
between functors `Cat.FreeRefl V ⥤ C` and refl functors `V ⥤rq C`.  -/
CategoryTheory.ReflQuiv.adj.homEquiv : {V : Type u_1} →
  [inst : CategoryTheory.ReflQuiver V] →
    {C : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_1, u_3} C] →
        CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl V) C ≃ V ⥤rq C
-- Std.Http.Data.Response
Std.Http.instInhabitedResponse.default : {t : Type} → [Inhabited t] → Std.Http.Response t
-- Init.Data.Vector.Basic
/-- The vector `#v[0, 1, 2, ..., n-1]`.  -/
Vector.range : (n : ℕ) → Vector ℕ n
-- Init.Data.SInt.Basic
instDecidableEqInt16 : DecidableEq Int16
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Ideal.nonempty_minimalPrimes : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R}, I ≠ ⊤ → Nonempty ↑I.minimalPrimes
-- Mathlib.Topology.NhdsSet
mem_nhdsSet_iff_exists : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X}, s ∈ nhdsSet t ↔ ∃ U, IsOpen U ∧ t ⊆ U ∧ U ⊆ s
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (U : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolutionUnit U]
  (F : CategoryTheory.Functor C V)
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F U] (x : C),
  (CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor U F).inv.app x =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj x)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj x)
          CategoryTheory.MonoidalCategory.DayConvolutionUnit.can)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.MonoidalCategory.DayConvolution.unit F U).app
            (x, CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
          ((CategoryTheory.MonoidalCategory.DayConvolution.convolution F U).map
            (CategoryTheory.MonoidalCategoryStruct.rightUnitor x).hom)))
-- Std.Http.Internal.Char
_private.Std.Http.Internal.Char.0.Std.Http.Internal.Char.qdtext.match_1.eq_2 : ∀ (motive : Char → Sort u_1) (h_1 : Unit → motive '\t') (h_2 : Unit → motive ' ') (h_3 : Unit → motive '!')
  (h_4 : (x : Char) → motive x),
  (match ' ' with
    | '\t' => h_1 ()
    | ' ' => h_2 ()
    | '!' => h_3 ()
    | x => h_4 x) =
    h_2 ()
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.le_iff : ∀ {α : Type u} [inst : LE α] [inst_1 : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] {a b : α},
  a ≤ b ↔ Std.PRange.UpwardEnumerable.LE a b
-- Mathlib.Data.Finsupp.ToDFinsupp
finsuppLequivDFinsupp_apply_apply : ∀ {ι : Type u_1} (R : Type u_2) {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : (m : M) → Decidable (m ≠ 0)] [inst_4 : Module R M], ⇑(finsuppLequivDFinsupp R) = Finsupp.toDFinsupp
-- Std.Http.Internal.ChunkedBuffer
/-- Append a single `ByteArray` to the `ChunkedBuffer`.
 -/
Std.Http.Internal.ChunkedBuffer.push : Std.Http.Internal.ChunkedBuffer → ByteArray → Std.Http.Internal.ChunkedBuffer
-- Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence
/-- Pull back a right dual along an equivalence.  -/
CategoryTheory.hasRightDualOfEquivalence : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              [F.Monoidal] →
                {G : CategoryTheory.Functor D C} →
                  (F ⊣ G) →
                    [F.IsEquivalence] →
                      (X : C) → [CategoryTheory.HasRightDual (F.obj X)] → CategoryTheory.HasRightDual X
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.tendsto_zero_inv_linear : ∀ (z : ℂ) (b : ℤ), Filter.Tendsto (fun d => 1 / (↑b * z + ↑d)) Filter.atTop (nhds 0)
-- Mathlib.Logic.Denumerable
Denumerable.decode_isSome : ∀ (α : Type u_3) [inst : Denumerable α] (n : ℕ), (Encodable.decode n).isSome = true
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.Eqv.of_add : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] (x : DecidableEq ι) (r : R) (f : (i : ι) → s i) (i : ι) (m₁ m₂ : s i),
  PiTensorProduct.Eqv R s (FreeAddMonoid.of (r, Function.update f i m₁) + FreeAddMonoid.of (r, Function.update f i m₂))
    (FreeAddMonoid.of (r, Function.update f i (m₁ + m₂)))
-- Init.Data.BEq
EquivBEq.mk : ∀ {α : Type u_1} [inst : BEq α] [toPartialEquivBEq : PartialEquivBEq α] [toReflBEq : ReflBEq α], EquivBEq α
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiff_finprod_cond : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {f : ι → M → G} {p : ι → Prop},
  (∀ (i : ι), p i → ContMDiff I' I n (f i)) →
    (LocallyFinite fun i => Function.mulSupport (f i)) → ContMDiff I' I n fun x => ∏ᶠ (i : ι) (_ : p i), f i x
-- Mathlib.Algebra.MvPolynomial.PDeriv
MvPolynomial.pderiv_monomial_single : ∀ {R : Type u} {σ : Type v} {a : R} [inst : CommSemiring R] {i : σ} {n : ℕ},
  (MvPolynomial.pderiv i) ((MvPolynomial.monomial fun₀ | i => n) a) = (MvPolynomial.monomial fun₀ | i => n - 1) (a * ↑n)
-- Mathlib.Algebra.Order.Field.Basic
inv_antitoneOn_Iio : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α],
  AntitoneOn (fun x => x⁻¹) (Set.Iio 0)
-- Mathlib.Topology.Order
nhds_iInf : ∀ {α : Type u} {ι : Sort u_1} {t : ι → TopologicalSpace α} {a : α}, nhds a = ⨅ i, nhds a
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.instUniformSpace : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        {σ : 𝕜₁ →+* 𝕜₂} →
          {E : Type u_3} →
            {F : Type u_4} →
              [inst_2 : AddCommGroup E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : Module 𝕜₁ E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : TopologicalSpace F] →
                        [inst_7 : Module 𝕜₂ F] →
                          [IsTopologicalAddGroup F] → [ContinuousConstSMul 𝕜₂ F] → UniformSpace (E →SWOT[σ] F)
-- Mathlib.Data.Countable.Basic
countable_right_of_prod_of_nonempty : ∀ {α : Type u} {β : Type v} [Nonempty α], Countable (α × β) → Countable β
-- Init.PropLemmas
or_congr : ∀ {a c b d : Prop}, (a ↔ c) → (b ↔ d) → (a ∨ b ↔ c ∨ d)
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.r_f : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') (i : ι),
  e.r (e.f i) = some i
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.sub_def : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : (i : ι) → Sub (G i)] (f g : (i : ι) → G i), f - g = fun i => f i - g i
-- Mathlib.Topology.Order.Monotone
/-- An antitone function continuous at the supremum of a nonempty set sends this supremum to
the infimum of the image of this set.  -/
Antitone.map_csSup_of_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β]
  {f : α → β} {A : Set α},
  ContinuousAt f (sSup A) →
    Antitone f →
      A.Nonempty → autoParam (BddAbove A) Antitone.map_csSup_of_continuousAt._auto_1 → f (sSup A) = sInf (f '' A)
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.continuous_coe : ∀ {α : Type u_1} [inst : TopologicalSpace α], Continuous SetLike.coe
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.inclusion_range : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} (h_le : H ≤ K),
  (AddSubgroup.inclusion h_le).range = H.addSubgroupOf K
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_comp_const_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {s : Set 𝕜} {f : 𝕜 → F} (c : 𝕜),
  iteratedDerivWithin n (fun z => f (c + z)) s = fun x => iteratedDerivWithin n f (c +ᵥ s) (c + x)
-- Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder
Finset.card_Ico_mul_right : ∀ {M : Type u_1} [inst : CancelCommMonoid M] [inst_1 : LinearOrder M] [IsOrderedMonoid M]
  [inst_3 : LocallyFiniteOrder M] [ExistsMulOfLE M] (a b c : M),
  (Finset.Ico (a * c) (b * c)).card = (Finset.Ico a b).card
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.BuilderOption.pattern : Lean.Term → Aesop.Frontend.BuilderOption
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.filterWithPostcondition.eq_1 : ∀ {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad n] [inst_1 : MonadLiftT m n]
  [inst_2 : Std.Iterator α m β] (f : β → Std.Iterators.PostconditionT n (ULift.{w, 0} Bool)) (it : Std.IterM m β),
  Std.IterM.filterWithPostcondition f it =
    Std.IterM.filterMapWithPostcondition
      (fun b => Std.Iterators.PostconditionT.map (fun x => if x.down = true then some b else none) (f b)) it
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- Restriction along the identity is isomorphic to the identity.  -/
AlgebraicGeometry.Scheme.Modules.restrictFunctorId : {X : AlgebraicGeometry.Scheme} →
  AlgebraicGeometry.Scheme.Modules.restrictFunctor (CategoryTheory.CategoryStruct.id X) ≅
    CategoryTheory.Functor.id X.Modules
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.sliceTo_lt_iff : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h : q ≤ p₀},
  p₀.sliceTo q h < p ↔ q < String.Slice.Pos.ofSliceTo p
-- Init.Grind.AC
Lean.Grind.AC.instBEqSeq.beq_spec_2 : ∀ (a : Lean.Grind.AC.Var) (a_1 : Lean.Grind.AC.Seq) (b : Lean.Grind.AC.Var) (b_1 : Lean.Grind.AC.Seq),
  (Lean.Grind.AC.Seq.cons a a_1 == Lean.Grind.AC.Seq.cons b b_1) = (a == b && a_1 == b_1)
-- Mathlib.Computability.Primrec.List
/-- `List.dropWhile` is primitive recursive.  -/
Primrec.list_dropWhile : ∀ {α : Type u_1} [inst : Primcodable α] {p : α → Bool}, Primrec p → Primrec (List.dropWhile p)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_inter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α],
  m₁.WF → m₂.WF → ∀ {k : α} [inst_3 : Inhabited (β k)], (m₁ ∩ m₂).get! k = if k ∈ m₂ then m₁.get! k else default
-- Mathlib.RingTheory.Unramified.Locus
Algebra.formallyUnramified_iff_forall : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.FormallyUnramified R A ↔ ∀ (q : PrimeSpectrum A), Algebra.IsUnramifiedAt R q.asIdeal
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.toFun_eq_coe : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : BumpCovering ι X s), f.toFun = ⇑f
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
GrpCat.instBraidedCategory : CategoryTheory.BraidedCategory GrpCat
-- Mathlib.Topology.Order.LocalExtr
IsLocalExtrOn.comp_antitone : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {f : α → β} {s : Set α} {a : α}, IsLocalExtrOn f s a → ∀ {g : β → γ}, Antitone g → IsLocalExtrOn (g ∘ f) s a
-- Init.Data.Range.Polymorphic.SInt
ISize.instRxiLawfulHasSize : Std.Rxi.LawfulHasSize ISize
-- Lean.Compiler.IR.Basic
Lean.IR.instInhabitedIRType.default : Lean.IR.IRType
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.powerBasisAux'_repr_apply_to_fun : ∀ {R : Type u_1} [inst : CommRing R] {g : Polynomial R} (hg : g.Monic) (f : AdjoinRoot g) (i : Fin g.natDegree),
  ((AdjoinRoot.powerBasisAux' hg).repr f) i = ((AdjoinRoot.modByMonicHom hg) f).coeff ↑i
-- Init.Guard
/-- The `guard_hyp` value specifier, one of `:=`, `:=~`, `:=ₛ`, `:=ₐ`  -/
Lean.Parser.colonEq : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.map_smul : ∀ {X : AlgebraicGeometry.Scheme} (M : X.Modules) {U V : X.Opens} (i : U ⟶ V) (r : ↑(X.presheaf.obj (Opposite.op V)))
  (x : ↑(M.presheaf.obj (Opposite.op V))),
  (CategoryTheory.ConcreteCategory.hom (M.presheaf.map i.op)) (r • x) =
    (CategoryTheory.ConcreteCategory.hom (X.presheaf.map i.op)) r •
      (CategoryTheory.ConcreteCategory.hom (M.presheaf.map i.op)) x
-- Mathlib.Logic.Function.Defs
Function.prod_ext_iff : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} {h h' : ι → α × β},
  h = h' ↔ Prod.fst ∘ h = Prod.fst ∘ h' ∧ Prod.snd ∘ h = Prod.snd ∘ h'
-- Init.Data.UInt.Lemmas
UInt64.zero_div : ∀ {a : UInt64}, 0 / a = 0
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k k' : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.1 == b.1) = false) l →
          k ∈ List.map Prod.fst l → (m.insertMany l).getKey? k' = some k
-- Init.Omega.IntList
Lean.Omega.IntList.dot_cons_cons : ∀ {x : ℤ} {xs : List ℤ} {y : ℤ} {ys : List ℤ},
  Lean.Omega.IntList.dot (x :: xs) (y :: ys) = x * y + Lean.Omega.IntList.dot xs ys
-- Init.Prelude
/-- Function composition, usually written with the infix operator `∘`. A new function is created from
two existing functions, where one function's output is used as input to the other.

Examples:
 * `Function.comp List.reverse (List.drop 2) [3, 2, 4, 1] = [1, 4]`
 * `(List.reverse ∘ List.drop 2) [3, 2, 4, 1] = [1, 4]`


Conventions for notations in identifiers:

 * The recommended spelling of `∘` in identifiers is `comp`. -/
Function.comp : {α : Sort u} → {β : Sort v} → {δ : Sort w} → (β → δ) → (α → β) → α → δ
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inr_snd : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr CategoryTheory.Limits.biprod.snd =
    CategoryTheory.CategoryStruct.id Y
-- Mathlib.RingTheory.Localization.Integer
/-- The finset of numerators after clearing the denominators of a finite set of fractions.  -/
IsLocalization.finsetIntegerMultiple : {R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Submonoid R) →
      {S : Type u_2} →
        [inst_1 : CommSemiring S] →
          [inst_2 : Algebra R S] → [IsLocalization M S] → [DecidableEq R] → Finset S → Finset R
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_mul_eq_zero_of_right : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] {p q : MvPolynomial σ R}
  (f : R →+* S₁) (g : σ → S₁), MvPolynomial.eval₂ f g q = 0 → MvPolynomial.eval₂ f g (p * q) = 0
-- Mathlib.RingTheory.RootsOfUnity.Basic
/-- The canonical isomorphism from the `n`th roots of unity in `Mˣ`
to the `n`th roots of unity in `M`.  -/
rootsOfUnityUnitsMulEquiv : (M : Type u_7) → [inst : CommMonoid M] → (n : ℕ) → ↥(rootsOfUnity n Mˣ) ≃* ↥(rootsOfUnity n M)
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.divMonomial_add_modMonomial_single : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (x : MvPolynomial σ R) (i : σ),
  ((MvPolynomial.X i * x.divMonomial fun₀ | i => 1) + x.modMonomial fun₀ | i => 1) = x
-- Mathlib.NumberTheory.FLT.Three
/-- Let `u₅ := -η ^ 2 * S.u₁ * S.u₂⁻¹`  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.u₅ : {K : Type u_1} →
  [inst : Field K] →
    {ζ : K} →
      {hζ : IsPrimitiveRoot ζ 3} →
        FermatLastTheoremForThreeGen.Solution✝ hζ →
          [inst_1 : NumberField K] → [IsCyclotomicExtension {3} ℚ K] → (NumberField.RingOfIntegers K)ˣ
-- Mathlib.RingTheory.Algebraic.StronglyTranscendental
IsStronglyTranscendental.restrictScalars : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] {x : T},
  IsStronglyTranscendental S x → IsStronglyTranscendental R x
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
sub_one_mul_padicValNat_factorial_lt_of_ne_zero : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {n : ℕ}, n ≠ 0 → (p - 1) * padicValNat p n.factorial < n
-- Mathlib.Analysis.BoxIntegral.DivergenceTheorem
/-- Auxiliary lemma for the divergence theorem.  -/
BoxIntegral.norm_volume_sub_integral_face_upper_sub_lower_smul_le : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {n : ℕ} [CompleteSpace E]
  (I : BoxIntegral.Box (Fin (n + 1))) {i : Fin (n + 1)} {f : (Fin (n + 1) → ℝ) → E} {f' : (Fin (n + 1) → ℝ) →L[ℝ] E},
  ContinuousOn f (BoxIntegral.Box.Icc I) →
    ∀ {x : Fin (n + 1) → ℝ},
      x ∈ BoxIntegral.Box.Icc I →
        ∀ {a : E} {ε : ℝ},
          0 < ε →
            (∀ y ∈ BoxIntegral.Box.Icc I, ‖f y - a - f' (y - x)‖ ≤ ε * ‖y - x‖) →
              ∀ {c : NNReal},
                I.distortion ≤ c →
                  ‖(∏ j, (I.upper j - I.lower j)) • f' (Pi.single i 1) -
                        (BoxIntegral.integral (I.face i) ⊥ (f ∘ i.insertNth (I.upper i))
                            BoxIntegral.BoxAdditiveMap.volume -
                          BoxIntegral.integral (I.face i) ⊥ (f ∘ i.insertNth (I.lower i))
                            BoxIntegral.BoxAdditiveMap.volume)‖ ≤
                    2 * ε * ↑c * ∏ j, (I.upper j - I.lower j)
-- Mathlib.Data.List.Fold
/-- **Alias** of `List.foldl1_eq_foldr1`. -/
List.foldl_op_eq_op_foldr_assoc : ∀ {α : Type u_1} {l : List α} {f : α → α → α} [ha : Std.Associative f] {a b : α},
  f (List.foldl f a l) b = f a (List.foldr f b l)
-- Init.Data.Vector.Basic
/-- Creates a vector from another with a provably equal length.  -/
Vector.cast : {n m : ℕ} → {α : Type u_1} → n = m → Vector α n → Vector α m
-- Mathlib.Data.Multiset.Basic
/-- Produces a list of the elements in the multiset using choice.  -/
Multiset.toList : {α : Type u_1} → Multiset α → List α
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.algebra₁ : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (self : Algebra.Extension R S) → Algebra R self.Ring
-- Init.Data.Nat.Power2.Basic
Nat.isPowerOfTwo_one : Nat.isPowerOfTwo 1
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.hasLeftHomology_of_epi_of_isIso_of_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasLeftHomology] [CategoryTheory.Epi φ.τ₁]
  [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃], S₂.HasLeftHomology
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.cofree_map_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) {X Y : C} (f : X ⟶ Y),
  (G.cofree.map f).f = G.map f
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.IsBlock.disjoint_smul_smul_set : ∀ {G : Type u_1} {X : Type u_2} [inst : SMul G X] {B : Set X} {s : Set G} {g : G},
  MulAction.IsBlock G B → ¬g • B ⊆ s • B → Disjoint (s • B) (g • B)
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.foldr.match_1.splitter : {α : Type u_1} →
  {β : Sort u_3} →
    (motive : Ordnode α → β → Sort u_2) →
      (x : Ordnode α) →
        (x_1 : β) →
          ((z : β) → motive Ordnode.nil z) →
            ((size : ℕ) → (l : Ordnode α) → (x : α) → (r : Ordnode α) → (z : β) → motive (Ordnode.node size l x r) z) →
              motive x x_1
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.dsimpGoal : Lean.MVarId →
  Lean.Meta.Simp.Context →
    optParam Lean.Meta.Simp.SimprocsArray #[] →
      optParam Bool true →
        optParam (Array Lean.FVarId) #[] →
          optParam Lean.Meta.Simp.Stats { } → Lean.MetaM (Option Lean.MVarId × Lean.Meta.Simp.Stats)
-- Mathlib.Algebra.Polynomial.Lifts
Polynomial.liftsRing.eq_1 : ∀ {R : Type u} [inst : Ring R] {S : Type v} [inst_1 : Ring S] (f : R →+* S),
  Polynomial.liftsRing f = (Polynomial.mapRingHom f).range
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.IsClosedImmersion.SpecMap_residue : ∀ {X : AlgebraicGeometry.Scheme} (x : ↥X),
  AlgebraicGeometry.IsClosedImmersion (AlgebraicGeometry.Spec.map (X.residue x))
-- Mathlib.Geometry.Manifold.Immersion
/-- The identity map is an immersion with complement `PUnit`.  -/
Manifold.IsImmersionOfComplement.id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_7} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_11}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I n M],
  Manifold.IsImmersionOfComplement PUnit.{u_15 + 1} I I n id
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- Auxiliary definition for `ofMonComonObj`.  -/
CategoryTheory.Bimon.ofMonComonObjX : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.Mon (CategoryTheory.Comon C) → CategoryTheory.Mon C
-- Mathlib.Algebra.MvPolynomial.CommRing
MvPolynomial.coeff_neg : ∀ {R : Type u} (σ : Type u_1) [inst : CommRing R] (m : σ →₀ ℕ) (p : MvPolynomial σ R),
  MvPolynomial.coeff m (-p) = -MvPolynomial.coeff m p
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.homeoOfIso.eq_1 : ∀ {X Y : TopCat} (f : X ≅ Y),
  TopCat.homeoOfIso f =
    { toFun := ⇑(CategoryTheory.ConcreteCategory.hom f.hom), invFun := ⇑(CategoryTheory.ConcreteCategory.hom f.inv),
      left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Init.Data.SInt.Lemmas
Int32.zero_mul : ∀ {a : Int32}, 0 * a = 0