mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finsupp.ToDFinsupp
finsuppAddEquivDFinsupp_symm_apply : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddZeroClass M] [inst_2 : (m : M) → Decidable (m ≠ 0)],
  ⇑finsuppAddEquivDFinsupp.symm = DFinsupp.toFinsupp
-- Mathlib.RingTheory.Ideal.Operations
Ideal.isCoprime_iff_codisjoint : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R}, IsCoprime I J ↔ Codisjoint I J
-- Mathlib.Topology.MetricSpace.Infsep
Set.Nontrivial.le_infsep_iff : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Set α} {d : ℝ},
  s.Nontrivial → (d ≤ s.infsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y)
-- Std.Time.Date.Unit.Year
Std.Time.Year.instDecidableLtOffset : {x y : Std.Time.Year.Offset} → Decidable (x < y)
-- Mathlib.CategoryTheory.Sites.LocalSite
/-- The only covering sieve of the terminal object is the trivial sieve.  -/
CategoryTheory.GrothendieckTopology.IsLocalSite.eq_top_of_mem : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.GrothendieckTopology C}
  [self : J.IsLocalSite], ∀ S ∈ J (⊤_ C), S = ⊤
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.Slice.Pos.nextFast.eq_1 : ∀ {s : String.Slice} (pos : s.Pos) (h : pos ≠ s.endPos), pos.nextFast h = String.Slice.Pos.ofStr (pos.str.next ⋯) ⋯ ⋯
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.commShiftIso_hom_naturality_assoc : ∀ {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] (F : CategoryTheory.Functor C D) {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] {X Y : C}
  (f : X ⟶ Y) (a : A) {Z : D} (h : (CategoryTheory.shiftFunctor D a).obj (F.obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C a).map f))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).hom.app Y) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).hom.app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (F.map f)) h)
-- Mathlib.RingTheory.QuasiFinite.Basic
/-- [Stacks Tag 00PM](https://stacks.math.columbia.edu/tag/00PM) -/
Algebra.quasiFinite_iff : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Algebra.QuasiFinite R S ↔
    autoParam (∀ (P : Ideal R) [inst_3 : P.IsPrime], Module.Finite P.ResidueField (P.Fiber S))
      Algebra.QuasiFinite.finite_fiber._autoParam
-- Mathlib.Analysis.Convex.Basic
/-- Convexity of sets.  -/
Convex : (𝕜 : Type u_1) → {E : Type u_2} → [Semiring 𝕜] → [PartialOrder 𝕜] → [AddCommMonoid E] → [SMul 𝕜 E] → Set E → Prop
-- Mathlib.RingTheory.Finiteness.FinitePresentationLocal
/-- Finite-presentation can be checked on a standard covering of the target.  -/
Algebra.FinitePresentation.of_span_eq_top_target_of_isLocalizationAway : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_3}
  (s : ι → S),
  Ideal.span (Set.range s) = ⊤ →
    ∀ (T : ι → Type u_4) [inst_3 : (i : ι) → CommRing (T i)] [inst_4 : (i : ι) → Algebra R (T i)]
      [inst_5 : (i : ι) → Algebra S (T i)] [∀ (i : ι), IsScalarTower R S (T i)]
      [∀ (i : ι), IsLocalization.Away (s i) (T i)] [∀ (i : ι), Algebra.FinitePresentation R (T i)],
      Algebra.FinitePresentation R S
-- Mathlib.LinearAlgebra.BilinearForm.Hom
/-- Two bilinear forms are equal when they are equal on all basis vectors.  -/
LinearMap.BilinForm.ext_basis : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B F₂ : LinearMap.BilinForm R M} {ι : Type u_9} (b : Module.Basis ι R M),
  (∀ (i j : ι), (B (b i)) (b j) = (F₂ (b i)) (b j)) → B = F₂
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.S.subcomplex_eq_of_epi : ∀ {X : SSet} (x y : X.S) (f : { len := x.dim } ⟶ { len := y.dim }) [CategoryTheory.Epi f],
  (CategoryTheory.ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex → x.subcomplex = y.subcomplex
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.point_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (X :
    CategoryTheory.Comma (CategoryTheory.CosimplicialObject.const C)
      (CategoryTheory.Functor.id (CategoryTheory.CosimplicialObject C))),
  CategoryTheory.CosimplicialObject.Augmented.point.obj X = X.left
-- Mathlib.Order.Filter.CountableInter
/-- **Alias** of `Filter.EventuallyEq.countable_bInter`. -/
EventuallyEq.countable_bInter : ∀ {α : Type u_2} {l : Filter α} [CountableInterFilter l] {ι : Type u_4} {S : Set ι},
  S.Countable →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi) → ⋂ i, ⋂ (h : i ∈ S), s i h =ᶠ[l] ⋂ i, ⋂ (h : i ∈ S), t i h
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.Transversal.mk.injEq : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} (injective : ∀ (i : ι), Function.Injective ⇑(φ i)) (set : (i : ι) → Set (G i))
  (one_mem : ∀ (i : ι), 1 ∈ set i) (compl : ∀ (i : ι), Subgroup.IsComplement (↑(φ i).range) (set i))
  (injective_1 : ∀ (i : ι), Function.Injective ⇑(φ i)) (set_1 : (i : ι) → Set (G i))
  (one_mem_1 : ∀ (i : ι), 1 ∈ set_1 i) (compl_1 : ∀ (i : ι), Subgroup.IsComplement (↑(φ i).range) (set_1 i)),
  ({ injective := injective, set := set, one_mem := one_mem, compl := compl } =
      { injective := injective_1, set := set_1, one_mem := one_mem_1, compl := compl_1 }) =
    (set = set_1)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterMap.match_1.eq_2 : ∀ {β' : Type u_1} (motive : Option β' → Sort u_2) (out' : β') (h_1 : some out' = none → motive none)
  (h_2 : (out'_1 : β') → some out' = some out'_1 → motive (some out'_1)),
  (match h' : some out' with
    | none => h_1 h'
    | some out'_1 => h_2 out'_1 h') =
    h_2 out' ⋯
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.eraseMany_list : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → ∀ (l : List α), (t₁.eraseMany l).Equiv (t₂.eraseMany l)
-- Mathlib.Algebra.Group.Basic
sub_ne_zero_of_ne : ∀ {α : Type u_1} [inst : SubtractionMonoid α] {a b : α}, a ≠ b → a - b ≠ 0
-- Lean.Server.Completion.CompletionUtils
Lean.Server.Completion.HoverInfo.after : Lean.Server.Completion.HoverInfo
-- Mathlib.Order.Sublattice
/-- A sublattice of a lattice is a set containing the suprema and infima of any of its elements.  -/
Sublattice : (α : Type u_2) → [Lattice α] → Type u_2
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.prod_principal : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {la : Filter α} {pa : ι → Prop} {sa : ι → Set α},
  la.HasBasis pa sa → ∀ (sb : Set β), (la ×ˢ Filter.principal sb).HasBasis pa fun x => sa x ×ˢ sb
-- Init.Data.Int.Order
Int.pos_of_mul_neg_right : ∀ {a b : ℤ}, a * b < 0 → a < 0 → 0 < b
-- Init.Data.List.Basic
List.mem_append_left : ∀ {α : Type u} {a : α} {as : List α} (bs : List α), a ∈ as → a ∈ as ++ bs
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- If `F : C ⥤ Type w` and `C` is locally `w`-small, then for any `X : C`,
`F.obj X` identifies to the colimit of
`(CategoryOfElements.π F).op ⋙ shrinkYoneda.obj X`.  -/
CategoryTheory.Functor.Elements.isColimitCoconeπOpCompShrinkYonedaObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] →
      (F : CategoryTheory.Functor C (Type w)) →
        (X : C) → CategoryTheory.Limits.IsColimit (CategoryTheory.Functor.Elements.coconeπOpCompShrinkYonedaObj F X)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
Submodule.adjoint_orthogonalProjectionOnto : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] (U : Submodule 𝕜 E) [inst_4 : CompleteSpace ↥U],
  ContinuousLinearMap.adjoint U.orthogonalProjectionOnto = U.subtypeL
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- Suppose `f : ℝ → ℝ` is continuous at `a` and `b`, the derivative `f'` is nonpositive on
`Ioo a b` and nonnegative on `Ioo b c`. Then `f` attains its minimum on `Ico a c` at `b`.  -/
isMinOn_Ico_of_deriv : ∀ {f : ℝ → ℝ} {a b c : ℝ},
  ContinuousAt f a →
    ContinuousAt f b →
      DifferentiableOn ℝ f (Set.Ioo a b) →
        DifferentiableOn ℝ f (Set.Ioo b c) →
          (∀ x ∈ Set.Ioo a b, deriv f x ≤ 0) → (∀ x ∈ Set.Ioo b c, 0 ≤ deriv f x) → IsMinOn f (Set.Ico a c) b
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- Additive subgroups of an additive group `A` are isomorphic to subgroups of `Multiplicative A`.
 -/
AddSubgroup.toSubgroup : {A : Type u_2} → [inst : AddGroup A] → AddSubgroup A ≃o Subgroup (Multiplicative A)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.rightUnitorNatIso_hom_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b : B) (X : a ⟶ b),
  (CategoryTheory.Bicategory.rightUnitorNatIso a b).hom.app X = (CategoryTheory.Bicategory.rightUnitor X).hom
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.or_of_add : ∀ {α : Type u_1} [inst : Semiring α] {p a b : α},
  FiniteMultiplicity p (a + b) → FiniteMultiplicity p a ∨ FiniteMultiplicity p b
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonCompletionIdentifier : Lean.FromJson Lean.Lsp.CompletionIdentifier
-- Batteries.Data.Fin.Fold
Fin.dfoldlM.loop.eq_1 : ∀ {m : Type u_1 → Type u_2} [inst : Monad m] (n : ℕ) (α : Fin (n + 1) → Type u_1)
  (f : (i : Fin n) → α i.castSucc → m (α i.succ)) (i : ℕ) (h : i < n + 1) (x : α ⟨i, h⟩),
  Fin.dfoldlM.loop n α f i h x =
    if h' : i < n then f ⟨i, h'⟩ x >>= Fin.dfoldlM.loop n α f (i + 1) ⋯ else cast ⋯ (pure x)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.comp.eq_5 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], CategoryTheory.WithInitial.comp = fun x x_1 => PUnit.unit
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.shrink.eq_1 : ∀ {α : Type u} (xs : Array α) (n : ℕ), xs.shrink n = Array.shrink.loop✝ (xs.size - n) xs
-- Mathlib.RingTheory.Nullstellensatz
MvPolynomial.pointToPoint_zeroLocus_le : ∀ {K : Type u_2} [inst : Field K] {σ : Type u_3} (I : Ideal (MvPolynomial σ K)),
  MvPolynomial.pointToPoint '' MvPolynomial.zeroLocus K I ⊆ PrimeSpectrum.zeroLocus ↑I
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.id_apply : ∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α), (ContinuousMap.id α) a = a
-- Mathlib.RingTheory.PowerSeries.Order
/-- The order of the formal power series `X^n` is `n`.  -/
PowerSeries.order_X_pow : ∀ {R : Type u_1} [inst : Semiring R] [Nontrivial R] (n : ℕ), (PowerSeries.X ^ n).order = ↑n
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] (i j : 𝒰.I₀)
  {Z_1 : AlgebraicGeometry.Scheme}
  (h : CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV 𝒰 f g i j)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
          (𝒰.f i))
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd
        (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.f i))
        ((AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι j))
      h
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.CompStruct.exists_of_simplex : ∀ {X : SSet.Truncated 2}
  (s : X.obj (Opposite.op { obj := { len := 2 }, property := SSet.Truncated.Edge.CompStruct._proof_1 })),
  ∃ x₀ x₁ x₂ e₀₁ e₁₂ e₀₂ h, h.simplex = s
-- Init.Data.AC
Lean.Data.AC.sort : List ℕ → List ℕ
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
SheafOfModules.bijective_pushforwardSections : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) (M : SheafOfModules R)
  [F.Final], Function.Bijective (SheafOfModules.pushforwardSections φ)
-- Aesop.Index
Aesop.Index.applicableRules : {α : Type} →
  [Ord α] →
    Aesop.Index α →
      Lean.MVarId →
        Aesop.RulePatternSubstMap →
          Array (Aesop.IndexMatchResult (Aesop.Rule α)) →
            (Aesop.Rule α → Bool) → Lean.MetaM (Array (Aesop.IndexMatchResult (Aesop.Rule α)))
-- Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
ContinuousLinearMapWOT.ext_inner : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F] {A B : E →WOT[𝕜] F},
  (∀ (x : E) (y : F), inner 𝕜 y (A x) = inner 𝕜 y (B x)) → A = B
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measureReal_def : ∀ {α : Type u_6} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α), μ.real s = (μ s).toReal
-- Lean.Elab.MutualInductive
/-- Takes a binder list and interprets the prefix to see if any could be construed to be binder info updates.
Returns the binder list without these updates along with the new binder infos for these parameters.

- `params` are the parameters appearing in the header
- `binders` is the binder list to process
- `maybeParam` should return true for every local that could be a parameter
  (for example, in structures we check that the ids don't refer to previously defined fields)
 -/
Lean.Elab.Command.elabParamInfoUpdates : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadError m] →
      [Lean.MonadLCtx m] →
        [MonadLiftT Lean.Elab.TermElabM m] →
          Array Lean.Expr →
            Array Lean.Syntax →
              (Lean.FVarId → m Bool) → m (Array Lean.Syntax × Lean.ExprMap (Lean.Syntax × Lean.BinderInfo))
-- Mathlib.Logic.Equiv.Prod
Equiv.prodCongrLeft_apply : ∀ {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) (b : β₁) (a : α₁),
  (Equiv.prodCongrLeft e) (b, a) = ((e a) b, a)
-- Lean.Elab.SyntheticMVars
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.synthesizeUsingDefaultPrio.synthesizeSomeUsingDefault? : List Lean.MVarId → Lean.Elab.TermElabM (Option (List Lean.MVarId))
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.Cardinal.leastExt.congr_simp : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] [inst_3 : Algebra.IsAlgebraic F E]
  (a a_1 : (Module.rank F E).ord.ToType),
  a = a_1 → Field.Emb.Cardinal.leastExt F E a = Field.Emb.Cardinal.leastExt F E a_1
-- Std.Data.DTreeMap.Slice
Std.DTreeMap.toList_roo : ∀ {α : Type u} {β : α → Type v} (cmp : autoParam (α → α → Ordering) Std.DTreeMap.toList_roo._auto_1) [Std.TransCmp cmp]
  {t : Std.DTreeMap α β cmp} {lowerBound upperBound : α},
  Std.Slice.toList (Std.Roo.Sliceable.mkSlice t lowerBound<...upperBound) =
    List.filter (fun e => decide ((cmp e.fst lowerBound).isGT = true ∧ (cmp e.fst upperBound).isLT = true)) t.toList
-- Mathlib.Topology.CompactOpen
/-- The coevaluation map `Y → C(X, Y × X)` is continuous (always).  -/
ContinuousMap.continuous_coev : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Continuous (ContinuousMap.coev X Y)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
/-- The conjugate transpose of a matrix defined in term of `star`.  -/
CStarMatrix.conjTranspose : {m : Type u_1} → {n : Type u_2} → {A : Type u_5} → [Star A] → CStarMatrix m n A → CStarMatrix n m A
-- Mathlib.Data.PNat.Factors
PrimeMultiset.toPNatMultiset.eq_1 : ∀ (v : PrimeMultiset), v.toPNatMultiset = Multiset.map Nat.Primes.toPNat v
-- Std.Data.TreeSet.Iterator
Std.TreeSet.toList.eq_1 : ∀ {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet α cmp), t.toList = t.inner.keys
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.instFinitenessRelation₂ : {m : Type w → Type w'} →
  {α₁ β₁ : Type w} →
    [inst : Std.Iterator α₁ m β₁] →
      {α₂ β₂ : Type w} →
        [inst_1 : Std.Iterator α₂ m β₂] →
          [inst_2 : Monad m] →
            [Std.Iterators.Productive α₁ m] →
              [Std.Iterators.Finite α₂ m] → Std.Iterators.FinitenessRelation (Std.Iterators.Types.Zip α₁ m α₂ β₂) m
-- Mathlib.RingTheory.WittVector.Teichmuller
_private.Mathlib.RingTheory.WittVector.Teichmuller.0.WittVector.teichmuller_mul_aux₂ : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {R : Type u_3} (x y : MvPolynomial R ℤ),
  WittVector.teichmullerFun p (x * y) = WittVector.teichmullerFun p x * WittVector.teichmullerFun p y
-- Mathlib.Algebra.Group.MinimalAxioms
/-- Define an `AddGroup` structure on a Type by proving `∀ a, 0 + a = a` and
`∀ a, -a + a = 0`.
Note that this uses the default definitions for `nsmul`, `zsmul` and `sub`.
See note [reducible non-instances].  -/
AddGroup.ofLeftAxioms : {G : Type u} →
  [inst : Add G] →
    [inst_1 : Neg G] →
      [inst_2 : Zero G] →
        (∀ (a b c : G), a + b + c = a + (b + c)) → (∀ (a : G), 0 + a = a) → (∀ (a : G), -a + a = 0) → AddGroup G
-- Mathlib.Data.Multiset.MapFold
Multiset.Nodup.of_map : ∀ {α : Type u_1} {β : Type v} {s : Multiset α} (f : α → β), (Multiset.map f s).Nodup → s.Nodup
-- Mathlib.Algebra.Group.Torsion
IsAddTorsionFree.zsmul_eq_zero_iff_left : ∀ {G : Type u_2} [inst : AddGroup G] [IsAddTorsionFree G] {n : ℤ} {a : G}, a ≠ 0 → (n • a = 0 ↔ n = 0)
-- Std.Http.Data.Status
Std.Http.Status.temporaryRedirect.sizeOf_spec : sizeOf Std.Http.Status.temporaryRedirect = 1
-- Mathlib.Data.Set.Sigma
Set.sigma_nonempty_iff : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)},
  (s.sigma t).Nonempty ↔ ∃ i ∈ s, (t i).Nonempty
-- Mathlib.Order.LiminfLimsup
sInfHom.le_apply_bliminf : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α}
  [inst_1 : CompleteLattice γ] (g : sInfHom α γ), Filter.bliminf (⇑g ∘ u) f p ≤ g (Filter.bliminf u f p)
-- Mathlib.Analysis.Normed.Group.Uniform
dist_mul_mul_le_of_le : ∀ {E : Type u_2} [inst : SeminormedCommGroup E] {a₁ a₂ b₁ b₂ : E} {r₁ r₂ : ℝ},
  dist a₁ b₁ ≤ r₁ → dist a₂ b₂ ≤ r₂ → dist (a₁ * a₂) (b₁ * b₂) ≤ r₁ + r₂
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.add_extMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.ProjectiveResolution X) {n : ℕ}
  (f g : R.complex.X n ⟶ Y) (m : ℕ) (hm : n + 1 = m) (hf : CategoryTheory.CategoryStruct.comp (R.complex.d m n) f = 0)
  (hg : CategoryTheory.CategoryStruct.comp (R.complex.d m n) g = 0),
  R.extMk f m hm hf + R.extMk g m hm hg = R.extMk (f + g) m hm ⋯
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `{ m_i }` is an `R`-basis of `M`, which is also `N`-linearly independent,
then `M` and `N` are linearly disjoint.  -/
Submodule.LinearDisjoint.of_basis_left : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (M N : Submodule R S)
  {ι : Type u_1} (m : Module.Basis ι R ↥M), (Submodule.mulLeftMap N ⇑m).ker = ⊥ → M.LinearDisjoint N
-- Init.Data.Option.List
Option.length_toList_eq_zero_iff : ∀ {α : Type u_1} {o : Option α}, o.toList.length = 0 ↔ o = none
-- Std.Sat.AIG.If
Std.Sat.AIG.RefVec.IfInput.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {w : ℕ} (discr : aig.Ref)
  (lhs rhs : aig.RefVec w) (discr_1 : aig.Ref) (lhs_1 rhs_1 : aig.RefVec w),
  ({ discr := discr, lhs := lhs, rhs := rhs } = { discr := discr_1, lhs := lhs_1, rhs := rhs_1 }) =
    (discr = discr_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
CategoryTheory.lift_comp_preservesLimitIso_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.PreservesLimit F G]
  [inst_4 : CategoryTheory.Limits.HasLimit F] (t : CategoryTheory.Limits.Cone F) {Z : D}
  (h : CategoryTheory.Limits.limit (F.comp G) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.limit.lift F t))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesLimitIso G F).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.lift (F.comp G) (G.mapCone t)) h
-- Mathlib.NumberTheory.LSeries.RiemannZeta
/-- A formal statement of the **Riemann hypothesis** – constructing a term of this type is worth a
million dollars.  -/
RiemannHypothesis : Prop
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.toMonoidHom_injective : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : Monoid A]
  [inst_3 : MulDistribMulAction M A] {B : Type u_5} [inst_4 : Monoid B] [inst_5 : MulDistribMulAction N B]
  {f g : A →ₑ*[φ] B}, ↑f = ↑g → f = g
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
/-- Constructor for `Total` to guide type checking.  -/
CategoryTheory.Limits.ColimitPresentation.Total.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u_1} →
      {I : J → Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
          [inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] →
            {D : CategoryTheory.Functor J C} →
              (P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)) →
                (i : J) → I i → CategoryTheory.Limits.ColimitPresentation.Total P
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.dualAnnihilator_dualAnnihilator_eq_map : ∀ {K : Type u_4} {V : Type u_5} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (W : Subspace K V)
  [FiniteDimensional K ↥W], (Submodule.dualAnnihilator W).dualAnnihilator = Submodule.map (Module.Dual.eval K V) W
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key in the tree map, panicking if the map is
empty.
 -/
Std.ExtTreeMap.minEntry! : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited (α × β)] → Std.ExtTreeMap α β cmp → α × β
-- Mathlib.Algebra.Ring.InjSurj
/-- Pullback a `Distrib` instance along an injective function.  -/
Function.Injective.distrib : {R : Type u_1} →
  {S : Type u_2} →
    (f : S → R) →
      Function.Injective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Distrib R] →
              (∀ (x y : S), f (x + y) = f x + f y) → (∀ (x y : S), f (x * y) = f x * f y) → Distrib S
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Polarization identity: The real part of the inner product, in terms of the norm.  -/
re_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), RCLike.re (inner 𝕜 x y) = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isSome_max?_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, k ∈ t → t.max?.isSome = true
-- Mathlib.Tactic.Linter.FindDeprecations
/-- `getPosAfterImports fname` parses the imports of `fname` and returns the position just after them.

This position is after all trailing whitespace and comments that may follow the imports of `fname`.
 -/
_private.Mathlib.Tactic.Linter.FindDeprecations.0.Mathlib.Tactic.getPosAfterImports : String → Lean.Elab.Command.CommandElabM String.Pos.Raw