mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Sub.Defs
le_add_tsub : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b : α},
  a ≤ b + (a - b)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- **Alias** of `differentiableWithinAt_fun_id`.

---

Eta-expanded form of `differentiableWithinAt_id` -/
differentiableWithinAt_id' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {x : E} {s : Set E}, DifferentiableWithinAt 𝕜 (fun x => x) s x
-- Mathlib.Data.Finset.Card
Finset.card_attach : ∀ {α : Type u_1} {s : Finset α}, s.attach.card = s.card
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
/-- `trailingDegree p` is the multiplicity of `x` in the polynomial `p`, i.e. the smallest
`X`-exponent in `p`.
`trailingDegree p = some n` when `p ≠ 0` and `n` is the smallest power of `X` that appears
in `p`, otherwise
`trailingDegree 0 = ⊤`.  -/
Polynomial.trailingDegree : {R : Type u} → [inst : Semiring R] → Polynomial R → ℕ∞
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.IsSeparating.mk_of_exists_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C},
  (∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, CategoryTheory.Epi p) → P.IsSeparating
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
/-- **Alias** of the forward direction of `Units.inv_le_one`. -/
Units.le_of_inv_le_one : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulLeftMono M] (u : Mˣ), ↑u⁻¹ ≤ 1 → 1 ≤ ↑u
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.card_norm_le_eq_card_norm_le_add_one : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] [Module.Finite ℤ S]
  (n : ℕ) [CharZero S], Nat.card { I // Ideal.absNorm I ≤ n } = Nat.card { I // Ideal.absNorm ↑I ≤ n } + 1
-- Mathlib.Tactic.Choose
/-- The name to use for the introduced variable  -/
Mathlib.Tactic.Choose.ChooseArg.name : Mathlib.Tactic.Choose.ChooseArg → Lean.Name
-- Batteries.Tactic.HelpCmd
/-- The command `#help cat C` shows all syntaxes that have been defined in syntax category `C` in the
current environment.
Each syntax has a format like:
```
syntax "first"... [Parser.tactic.first]
  `first | tac | ...` runs each `tac` until one succeeds, or else fails.
```
The quoted string is the leading token of the syntax, if applicable. It is followed by the full
name of the syntax (which you can also click to go to the definition), and the documentation.

* The form `#help cat C id` will show only attributes that begin with `id`.
* The form `#help cat+ C` will also show information about any `macro`s and `elab`s
  associated to the listed syntaxes.
 -/
Batteries.Tactic.«command#help_Cat+______» : Lean.ParserDescr
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.opowAux.match_1.eq_2 : ∀ (motive : ℕ → ℕ → Sort u_1) (m : ℕ) (h_1 : (x : ℕ) → motive x 0) (h_2 : (m : ℕ) → motive 0 m.succ)
  (h_3 : (k m : ℕ) → motive k.succ m),
  (match 0, m.succ with
    | x, 0 => h_1 x
    | 0, m.succ => h_2 m
    | k.succ, m => h_3 k m) =
    h_2 m
-- Mathlib.RingTheory.Smooth.IntegralClosure
_private.Mathlib.RingTheory.Smooth.IntegralClosure.0.TensorProduct.toIntegralClosure_bijective_of_isStandardEtale : ∀ {R : Type u_1} {S : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.IsStandardEtale R S],
  Function.Bijective ⇑(TensorProduct.toIntegralClosure R S B)
-- Init.Prelude
instInhabitedUInt16 : Inhabited UInt16
-- Mathlib.Order.PartialSups
partialSups_eq_biSup : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : LocallyFiniteOrderBot ι] [inst_2 : CompleteLattice α]
  (f : ι → α) (i : ι), (partialSups f) i = ⨆ j, ⨆ (_ : j ≤ i), f j
-- Mathlib.RingTheory.DedekindDomain.SelmerGroup
IsDedekindDomain.selmerGroup.monotone : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type v} [inst_2 : Field K] [inst_3 : Algebra R K]
  [inst_4 : IsFractionRing R K] {S S' : Set (IsDedekindDomain.HeightOneSpectrum R)} {n : ℕ},
  S ⊆ S' → IsDedekindDomain.selmerGroup ≤ IsDedekindDomain.selmerGroup
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.nhds_zero_basis : (nhds 0).HasBasis (fun a => 0 < a) fun a => Set.Iio a
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerLeftIso_hom_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ : CategoryTheory.Arrow C) {W : C}
  [inst_3 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
      (CategoryTheory.MonoidalCategory.tensorLeft W)],
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerLeftIso X₁ X₂).hom.left =
    CategoryTheory.CategoryStruct.comp ⋯.isoPushout.hom
      (CategoryTheory.Limits.HasColimit.isoOfNatIso
          (CategoryTheory.Limits.spanExt (CategoryTheory.MonoidalCategoryStruct.associator W X₁.left X₂.left).symm
            (CategoryTheory.MonoidalCategoryStruct.associator W X₁.right X₂.left).symm
            (CategoryTheory.MonoidalCategoryStruct.associator W X₁.left X₂.right).symm ⋯ ⋯)).hom
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
CategoryTheory.Limits.IsLimit.mk.congr_simp : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F}
  (lift lift_1 : (s : CategoryTheory.Limits.Cone F) → s.pt ⟶ t.pt) (e_lift : lift = lift_1)
  (fac :
    ∀ (s : CategoryTheory.Limits.Cone F) (j : J), CategoryTheory.CategoryStruct.comp (lift s) (t.π.app j) = s.π.app j)
  (uniq :
    ∀ (s : CategoryTheory.Limits.Cone F) (m : s.pt ⟶ t.pt),
      (∀ (j : J), CategoryTheory.CategoryStruct.comp m (t.π.app j) = s.π.app j) → m = lift s),
  { lift := lift, fac := fac, uniq := uniq } = { lift := lift_1, fac := ⋯, uniq := ⋯ }
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
ContinuousLinearEquiv.uniformConvergenceCLMCongr_apply : ∀ {𝕜 : Type u_6} {E : Type u_7} {F : Type u_8} {G : Type u_9} {H : Type u_10} [inst : AddCommGroup E]
  [inst_1 : AddCommGroup F] [inst_2 : AddCommGroup G] [inst_3 : AddCommGroup H] [inst_4 : NormedField 𝕜]
  [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 F] [inst_7 : Module 𝕜 G] [inst_8 : Module 𝕜 H] [inst_9 : TopologicalSpace E]
  [inst_10 : TopologicalSpace F] [inst_11 : TopologicalSpace G] [inst_12 : TopologicalSpace H]
  [inst_13 : IsTopologicalAddGroup G] [inst_14 : IsTopologicalAddGroup H] [inst_15 : ContinuousConstSMul 𝕜 G]
  [inst_16 : ContinuousConstSMul 𝕜 H] (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G) (𝔖 : Set (Set E)) (𝔗 : Set (Set F))
  (h : ∀ (t : Set F), t ∈ 𝔗 ↔ ⇑e₁ ⁻¹' t ∈ 𝔖) (φ : UniformConvergenceCLM (RingHom.id 𝕜) H 𝔖) (f : F),
  ((e₁.uniformConvergenceCLMCongr e₂ 𝔖 𝔗 h) φ) f = e₂ (φ (e₁.symm f))
-- Batteries.Control.Nondet.Basic
/-- All iterations of a non-deterministic function on an initial value.

(That is, depth first search.)
 -/
Nondet.iterate : {σ : Type} →
  {m : Type → Type} → [Monad m] → [inst : Lean.MonadBacktrack σ m] → {α : Type} → (α → Nondet m α) → α → Nondet m α
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.leftUnitor_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G : CategoryTheory.AddGrp C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor G).hom.hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor G.X).hom
-- Mathlib.Control.Fold
Monoid.Foldl.get : {α : Type u} → Monoid.Foldl α → α → α
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.instances : Lean.Option Bool
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_le_iff : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {n : σ} {f : MvPolynomial σ R} {d : ℕ},
  MvPolynomial.degreeOf n f ≤ d ↔ ∀ m ∈ f.support, m n ≤ d
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The initial state, given a finite input that is placed on the tape starting at the TM head and
going to the right.  -/
Turing.TM1.init : {Γ : Type u_1} →
  {Λ : Type u_2} → {σ : Type u_3} → [Inhabited Λ] → [inst : Inhabited Γ] → [Inhabited σ] → List Γ → Turing.TM1.Cfg Γ Λ σ
-- Mathlib.Topology.Separation.Regular
instRegularSpaceProd : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [RegularSpace X] [inst_2 : TopologicalSpace Y]
  [RegularSpace Y], RegularSpace (X × Y)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.insertMany_empty_list_cons_eq_insertMany! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {k : α} {v : β k} {tl : List ((a : α) × β a)},
  ↑(Std.DTreeMap.Internal.Impl.empty.insertMany (⟨k, v⟩ :: tl) ⋯) =
    ↑((Std.DTreeMap.Internal.Impl.insert! k v Std.DTreeMap.Internal.Impl.empty).insertMany! tl)
-- Mathlib.Data.Finset.Sups
Finset.image_subset_diffs_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {s t : Finset α} {a : α},
  a ∈ s → Finset.image (fun x => a \ x) t ⊆ s.diffs t
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.Term.realize.match_1.splitter : {L : FirstOrder.Language} →
  {α : Type u_3} →
    (motive : L.Term α → Sort u_4) →
      (x : L.Term α) →
        ((k : α) → motive (FirstOrder.Language.var k)) →
          ((l : ℕ) → (f : L.Functions l) → (ts : Fin l → L.Term α) → motive (FirstOrder.Language.func f ts)) → motive x
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.toRingHom_id : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_6} [inst : Semiring A] [inst_1 : SetLike σ A] {𝒜 : ι → σ},
  ↑(GradedRingHom.id 𝒜) = RingHom.id A
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.isBasis : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α}, l.HasBasis p s → Filter.IsBasis p s
-- Aesop.RuleSet.Filter
/-- `#[]` means 'match any phase'
 -/
Aesop.RuleFilter.phases : Aesop.RuleFilter → Array Aesop.PhaseName
-- Mathlib.Analysis.Calculus.Rademacher
LipschitzWith.locallyIntegrable_lineDeriv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {C : NNReal} {f : E → ℝ} {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure],
  LipschitzWith C f → ∀ (v : E), MeasureTheory.LocallyIntegrable (fun x => lineDeriv ℝ f x v) μ
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.factors_one : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [Nontrivial α],
  Associates.factors 1 = 0
-- Mathlib.Algebra.Star.LinearMap
LinearMap.intrinsicStar_lTensor : ∀ {R : Type u_5} {E : Type u_6} {F : Type u_7} {G : Type u_8} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : AddCommMonoid E] [inst_3 : StarAddMonoid E] [inst_4 : Module R E] [inst_5 : StarModule R E]
  [inst_6 : AddCommMonoid F] [inst_7 : StarAddMonoid F] [inst_8 : Module R F] [inst_9 : StarModule R F]
  [inst_10 : AddCommMonoid G] [inst_11 : StarAddMonoid G] [inst_12 : Module R G] [inst_13 : StarModule R G]
  (f : WithConv (F →ₗ[R] G)),
  star (WithConv.toConv (LinearMap.lTensor E f.ofConv)) = WithConv.toConv (LinearMap.lTensor E (star f).ofConv)
-- Mathlib.Algebra.Order.Group.Action.Synonym
Lex.instVAddAssocClass' : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : VAdd M N] [inst_1 : VAdd M α] [inst_2 : VAdd N α]
  [VAddAssocClass M N α], VAddAssocClass M (Lex N) α
-- Mathlib.Combinatorics.Additive.Energy
/-- The multiplicative energy of two finsets `s` and `t` in a group is the number of quadruples
`(a₁, a₂, b₁, b₂) ∈ s × s × t × t` such that `a₁ * b₁ = a₂ * b₂`.  -/
Combinatorics.Additive.«termEₘ[_,_]» : Lean.ParserDescr
-- Init.Meta.Defs
Lean.TSyntax.instCoeScientificLitTerm : Coe Lean.ScientificLit Lean.Term
-- Mathlib.CategoryTheory.Limits.FinallySmall
/-- The converse is true if `J` is cofiltered, see `initiallySmall_of_small_weakly_initial_set`.  -/
CategoryTheory.InitiallySmall.exists_small_weakly_initial_set : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.InitiallySmall J],
  ∃ s, ∃ (_ : Small.{w, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)
-- Mathlib.Util.Superscript
_private.Mathlib.Util.Superscript.0.Mathlib.Tactic.Superscript.isValid.valid : Mathlib.Tactic.Superscript.Mapping → String → Bool
-- Mathlib.Order.CompleteLattice.Basic
sInf_image' : ∀ {α : Type u_1} {β : Type u_2} [inst : InfSet α] {s : Set β} {f : β → α}, sInf (f '' s) = ⨅ a, f ↑a
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.isNoetherian_zero : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K], IsNoetherian R₁ ↥↑0
-- Mathlib.Algebra.Algebra.Hom
AlgHom.coe_ringHom_mk : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {f : A →+* B}
  (h : ∀ (r : R), (↑↑f).toFun ((algebraMap R A) r) = (algebraMap R B) r), ↑{ toRingHom := f, commutes' := h } = f
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.State.readBody.injEq : ∀ {dir : Std.Http.Protocol.H1.Direction} (a a_1 : Std.Http.Protocol.H1.Reader.BodyState),
  (Std.Http.Protocol.H1.Reader.State.readBody a = Std.Http.Protocol.H1.Reader.State.readBody a_1) = (a = a_1)
-- Mathlib.Data.Stream.Init
Stream'.take_succ_cons : ∀ {α : Type u} {a : α} (n : ℕ) (s : Stream' α), Stream'.take (n + 1) (Stream'.cons a s) = a :: Stream'.take n s
-- Init.Data.Array.Bootstrap
Array.foldrM_eq_reverse_foldlM_toList.aux : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {f : α → β → m β} {xs : Array α} {init : β}
  {i : ℕ} (h : i ≤ xs.size),
  List.foldlM (fun x y => f y x) init (List.take i xs.toList).reverse = Array.foldrM.fold f xs 0 i h init
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Subtype.opensMeasurableSpace : ∀ {α : Type u_6} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [h : OpensMeasurableSpace α] (p : α → Prop),
  OpensMeasurableSpace (Subtype p)
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_16 : HSub Std.Time.Second.Offset Std.Time.Day.Offset Std.Time.Second.Offset
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_sep : ∀ {p : ZFSet.{u} → Prop} {x y : ZFSet.{u}}, y ∈ ZFSet.sep p x ↔ y ∈ x ∧ p y
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.toInt'.toIntBin : Lean.Expr →
  Lean.Meta.Grind.Arith.Cutsat.ToIntThms →
    (Lean.Expr → Lean.Expr → Lean.Expr) →
      Lean.Expr → Lean.Expr → Lean.Meta.Grind.Arith.Cutsat.ToIntM (Lean.Expr × Lean.Expr)
-- Mathlib.RingTheory.Localization.Defs
/-- The localization of an integral domain to a set of non-zero elements is an integral domain.  -/
IsLocalization.isDomain_localization : ∀ {R : Type u_1} [inst : CommSemiring R] [IsDomain R] {M : Submonoid R},
  M ≤ nonZeroDivisors R → IsDomain (Localization M)
-- Mathlib.Topology.UniformSpace.Cauchy
Filter.totallyBounded_iff_ultrafilter : ∀ {α : Type u} [uniformSpace : UniformSpace α] {g : Filter α},
  g.TotallyBounded ↔ ∀ (f : Ultrafilter α), ↑f ≤ g → Cauchy ↑f
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
Std.IterM.step_zip : ∀ {α₁ α₂ β₁ β₂ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α₁ m β₁]
  [inst_2 : Std.Iterator α₂ m β₂] {it₁ : Std.IterM m β₁} {it₂ : Std.IterM m β₂},
  (it₁.zip it₂).step = do
    let __do_lift ← it₁.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it₁' out, hp⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.Intermediate.zip it₁' (some ⟨out, ⋯⟩) it₂) ⋯))
      | ⟨Std.IterStep.skip it₁', hp⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.Intermediate.zip it₁' none it₂) ⋯))
      | ⟨Std.IterStep.done, hp⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.Tactic.Sat.FromLRAT
/-- Returns `a` and `pr : reify v l a` given a literal `c`  -/
Mathlib.Tactic.Sat.buildReify.reifyLiteral : ℕ → Lean.Expr → Lean.Expr × Lean.Expr
-- Mathlib.RingTheory.WittVector.Basic
_private.Mathlib.RingTheory.WittVector.Basic.0.WittVector.ghostFun_mul : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (x y : WittVector p R),
  WittVector.ghostFun✝ (x * y) = WittVector.ghostFun✝ x * WittVector.ghostFun✝ y
-- Mathlib.Combinatorics.Colex
/-- `{a} ≤ s` in colex iff `s` contains an element greater than or equal to `a`.  -/
Finset.Colex.singleton_le_toColex : ∀ {α : Type u_1} [inst : PartialOrder α] {s : Finset α} {a : α}, toColex {a} ≤ toColex s ↔ ∃ x ∈ s, a ≤ x
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
/-- Representation function for `Cofix F α`  -/
MvQPF.Cofix.repr : {n : ℕ} → {F : TypeVec.{u} (n + 1) → Type u} → [q : MvQPF F] → {α : TypeVec.{u} n} → MvQPF.Cofix F α → (MvQPF.P F).M α
-- Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
/-- The first multivariate polynomial used in the proof of Erdős–Ginzburg–Ziv.  -/
_private.Mathlib.Combinatorics.Additive.ErdosGinzburgZiv.0.f₁ : {ι : Type u_1} → {p : ℕ} → [inst : Fact (Nat.Prime p)] → (s : Finset ι) → (ι → ZMod p) → MvPolynomial (↥s) (ZMod p)
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.ext' : ∀ {M : Type u_1} [inst : MulOneClass M] {s₁ s₂ : SaturatedSubmonoid M}, (∀ (x : M), x ∈ s₁ ↔ x ∈ s₂) → s₁ = s₂
-- Init.Data.Nat.Bitwise.Lemmas
Nat.or_lt_two_pow : ∀ {x y n : ℕ}, x < 2 ^ n → y < 2 ^ n → x ||| y < 2 ^ n
-- Mathlib.Analysis.Normed.Operator.Prod
ContinuousLinearMap.opNNNorm_prod : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : SeminormedAddCommGroup F] [inst_3 : SeminormedAddCommGroup G]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedSpace 𝕜 G] (f : E →L[𝕜] F) (g : E →L[𝕜] G),
  ‖f.prod g‖₊ = ‖(f, g)‖₊
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
IsLocalDiffeomorphAt.localInverse_mdifferentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (hf : IsLocalDiffeomorphAt I J n f x), n ≠ 0 → MDiffAt ↑hf.localInverse.toPartialEquiv (f x)
-- Std.Data.Internal.List.Associative
Std.Internal.List.self_le_maxKeyD_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k} {fallback : α},
      (compare k (Std.Internal.List.maxKeyD (Std.Internal.List.insertEntryIfNew k v l) fallback)).isLE = true
-- Mathlib.GroupTheory.Nilpotent
/-- A custom induction principle for nilpotent additive groups.
The base case is a trivial group (`subsingleton G`), and in the induction step, one can assume the
hypothesis for the additive group quotiented by its center.  -/
AddGroup.nilpotent_center_quotient_ind : ∀ {P : (G : Type u_2) → [inst : AddGroup G] → [AddGroup.IsNilpotent G] → Prop} (G : Type u_2) [inst : AddGroup G]
  [inst_1 : AddGroup.IsNilpotent G],
  (∀ (G : Type u_2) [inst : AddGroup G] [inst_2 : Subsingleton G], P G) →
    (∀ (G : Type u_2) [inst : AddGroup G] [inst_2 : AddGroup.IsNilpotent G], P (G ⧸ AddSubgroup.center G) → P G) → P G
-- Mathlib.RingTheory.Perfection
PerfectionMap.equiv.congr_simp : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u₁} [inst_1 : CommSemiring R] [inst_2 : CharP R p] {P : Type u₃}
  [inst_3 : CommSemiring P] [inst_4 : CharP P p] [inst_5 : PerfectRing P p] {π π_1 : P →+* R} (e_π : π = π_1)
  (m : PerfectionMap p π), m.equiv = ⋯.equiv
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Inner
Measurable.inner_const : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {x : MeasurableSpace α} [inst_3 : MeasurableSpace E] [OpensMeasurableSpace E]
  [SecondCountableTopology E] {c : E} {f : α → E}, Measurable f → Measurable fun t => inner 𝕜 (f t) c
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Fintype.prod_subtype_mul_prod_subtype : ∀ {M : Type u_4} {ι : Type u_7} [inst : Fintype ι] [inst_1 : CommMonoid M] (p : ι → Prop) (f : ι → M)
  [inst_2 : DecidablePred p], (∏ i, f ↑i) * ∏ i, f ↑i = ∏ i, f i
-- Mathlib.FieldTheory.SeparableDegree
/-- If a monic irreducible polynomial over a field `F` of exponential characteristic `q` has
separable degree one, then it is of the form `X ^ (q ^ n) - C y` for some natural number `n`,
and some element `y` of `F`, such that either `n = 0` or `y` has no `q`-th root in `F`.  -/
Polynomial.Monic.eq_X_pow_char_pow_sub_C_of_natSepDegree_eq_one_of_irreducible : ∀ {F : Type u} [inst : Field F] {f : Polynomial F} (q : ℕ) [inst_1 : ExpChar F q],
  f.Monic →
    Irreducible f →
      f.natSepDegree = 1 → ∃ n y, (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = Polynomial.X ^ q ^ n - Polynomial.C y
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- The localization functor to the constructed localized category for a morphism property
that has left calculus of fractions.  -/
CategoryTheory.MorphismProperty.LeftFraction.Localization.Q : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (W : CategoryTheory.MorphismProperty C) →
      [inst_1 : W.HasLeftCalculusOfFractions] →
        CategoryTheory.Functor C (CategoryTheory.MorphismProperty.LeftFraction.Localization W)
-- Mathlib.Analysis.Normed.Group.Continuity
NormedAddCommGroup.toENormedAddCommMonoid : {E : Type u_4} → [inst : NormedAddCommGroup E] → ENormedAddCommMonoid E
-- Mathlib.Analysis.Distribution.DerivNotation
/-- The notation typeclass for the line derivative.
 -/
LineDeriv : Type u → Type v → outParam (Type w) → Type (max (max u v) w)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.getElem_toList_eq : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α] {i : ℕ} {h : i < r.toList.length},
  r.toList[i] = (Std.PRange.succMany? (i + 1) r.lower).get ⋯
-- Mathlib.Data.Multiset.Find
Multiset.choose.congr_simp : ∀ {α : Type u_1} (p p_1 : α → Prop) (e_p : p = p_1) {inst : DecidablePred p} [inst_1 : DecidablePred p_1]
  (l l_1 : Multiset α) (e_l : l = l_1) (hp : ∃! a, a ∈ l ∧ p a), Multiset.choose p l hp = Multiset.choose p_1 l_1 ⋯
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_nsmul : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} [inst : NormedAddCommGroup E] [NormedSpace ℝ E]
  (n : ℕ) (f : α → E) (μ : MeasureTheory.Measure α), MeasureTheory.lpNorm (n • f) p μ = n • MeasureTheory.lpNorm f p μ
-- Mathlib.Algebra.GroupWithZero.Units.Basic
isUnit_iff_ne_zero : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, IsUnit a ↔ a ≠ 0
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.covarianceOperator.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] [inst_4 : CompleteSpace E] (μ μ_1 : MeasureTheory.Measure E),
  μ = μ_1 → ProbabilityTheory.covarianceOperator μ = ProbabilityTheory.covarianceOperator μ_1
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.equiv_symm_sub : ∀ {A : Type u_3} {E : Type u_4} (x' y' : E) [inst : AddCommGroup E],
  (WithCStarModule.equiv A E).symm (x' - y') = (WithCStarModule.equiv A E).symm x' - (WithCStarModule.equiv A E).symm y'