mathlib-initiative/mathlib-types huggingface dataset:
-- Init.System.CancelToken
/-- Creates a new cancellation token.

Note: cannot be called from `initialize` blocks because the underlying task manager is not yet
running at that point. Construct lazily on first use instead.
 -/
IO.CancelToken.new : BaseIO IO.CancelToken
-- Init.Data.UInt.Bitwise
UInt32.neg_one_shiftLeft_or_shiftLeft : ∀ {a b : UInt32}, (-1) <<< b ||| a <<< b = (-1) <<< b
-- Mathlib.Data.Set.MulAntidiagonal
Set.AddAntidiagonal.eq_of_snd_eq_snd : ∀ {α : Type u_1} [inst : AddCommMonoid α] [IsCancelAdd α] {s t : Set α} {a : α} {x y : ↑(s.antidiagonal t a)},
  (↑x).2 = (↑y).2 → x = y
-- Mathlib.Data.Quot
Quotient.out_inj : ∀ {α : Sort u_1} {s : Setoid α} {x y : Quotient s}, x.out = y.out ↔ x = y
-- Init.Data.List.Int.Prod
List.prod_append_int : ∀ {l₁ l₂ : List ℤ}, (l₁ ++ l₂).prod = l₁.prod * l₂.prod
-- Mathlib.Algebra.BigOperators.Fin
Finset.sum_range : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (f : ℕ → M), ∑ i ∈ Finset.range n, f i = ∑ i, f ↑i
-- Mathlib.Algebra.Polynomial.Laurent
Polynomial.trunc_toLaurent : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R), LaurentPolynomial.trunc (Polynomial.toLaurent f) = f
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.monad : Monad Ultrafilter
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_inter_le_size_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁ ∩ t₂).size ≤ t₁.size
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.baseChange_polynomialZ : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) {S : Type s} [inst_1 : CommRing S] {A : Type u}
  [inst_2 : CommRing A] {B : Type v} [inst_3 : CommRing B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B), (W'.baseChange B).polynomialZ = (MvPolynomial.map ↑f) (W'.baseChange A).polynomialZ
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.limitUnopIsoUnopColimit_inv_comp_π_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) [inst_2 : CategoryTheory.Limits.HasColimit F] (j : J) {Z : C}
  (h : F.unop.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitUnopIsoUnopColimit F).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F.unop j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F (Opposite.op j)).unop h
-- Init.Data.Nat.Lemmas
/-- `n` is not divisible by `a` iff it is between `a * k` and `a * (k + 1)` for some `k`.  -/
Nat.not_dvd_iff_lt_mul_succ : ∀ (n : ℕ) {a : ℕ}, 0 < a → (¬a ∣ n ↔ ∃ k, a * k < n ∧ n < a * (k + 1))
-- Mathlib.Analysis.Normed.Lp.Matrix
/-- `Matrix.toLinAlgEquiv'` adapted for `PiLp R _`.  -/
Matrix.toLpLinAlgEquiv : {n : Type u_2} →
  {R : Type u_4} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] →
        [inst_2 : CommRing R] → (p : ENNReal) → Matrix n n R ≃ₐ[R] Module.End R (WithLp p (n → R))
-- Mathlib.LinearAlgebra.TensorProduct.Pi
/-- Tensor product commutes with finite products on the left.
TODO: generalize to `S`-linear.  -/
TensorProduct.piLeft : (R : Type u_1) →
  [inst : CommSemiring R] →
    (N : Type u_3) →
      [inst_1 : AddCommMonoid N] →
        [inst_2 : Module R N] →
          {ι : Type u_4} →
            (M : ι → Type u_5) →
              [inst_3 : (i : ι) → AddCommMonoid (M i)] →
                [inst_4 : (i : ι) → Module R (M i)] →
                  [Fintype ι] →
                    [DecidableEq ι] → TensorProduct R ((i : ι) → M i) N ≃ₗ[R] (i : ι) → TensorProduct R (M i) N
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insert.match_1.splitter : {n : ℕ} →
  (motive : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n → Sort u_1) →
    (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) →
      ((clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))) →
          (rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) →
            (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) →
              motive { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments }) →
        motive f
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- The right adjoint mate `fᘁ : Xᘁ ⟶ Yᘁ` of a morphism `f : X ⟶ Y`.  -/
CategoryTheory.rightAdjointMate : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X Y : C} →
        [inst_2 : CategoryTheory.HasRightDual X] → [inst_3 : CategoryTheory.HasRightDual Y] → (X ⟶ Y) → (Yᘁ ⟶ Xᘁ)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_alter_eq_sub_one : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : Option β → Option β}, m.WF → k ∈ m → (f m[k]?).isNone = true → (m.alter k f).size = m.size - 1
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey_eq_getLast_keys : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    List.Pairwise (fun a b => compare a.fst b.fst = Ordering.lt) l →
      ∀ {he : l.isEmpty = false}, Std.Internal.List.maxKey l he = (Std.Internal.List.keys l).getLast ⋯
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.genWeightSpaceChain.eq_1 : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ₁ χ₂ : L → R) (p q : ℤ),
  LieModule.genWeightSpaceChain M χ₁ χ₂ p q = ⨆ k ∈ Set.Ioo p q, LieModule.genWeightSpace M (k • χ₁ + χ₂)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_filter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k fallback : α},
  (Std.DHashMap.filter f m).getKeyD k fallback = ((m.getKey? k).pfilter fun x_2 h' => f x_2 (m.get x_2 ⋯)).getD fallback
-- Std.Data.Iterators.Producers.Array
/-- Returns a finite iterator for the given array.
The iterator yields the elements of the array in order and then terminates.

The monadic version of this iterator is `Array.iterM`.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Array.iter : {α : Type w} → Array α → Std.Iter α
-- Mathlib.Algebra.Order.Sub.Defs
AddLECancellable.lt_add_of_tsub_lt_right : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α},
  AddLECancellable c → a - c < b → a < b + c
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
/-- Given a limiting pullback cone, the fork in `SingleEqualizerCondition` is limiting iff the diagram
in `Presheaf.isSheaf_iff_isLimit_coverage` is limiting.
 -/
CategoryTheory.regularTopology.isLimit_forkOfι_equiv : {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] →
        (P : CategoryTheory.Functor Cᵒᵖ D) →
          {X B : C} →
            (π : X ⟶ B) →
              (c : CategoryTheory.Limits.PullbackCone π π) →
                CategoryTheory.Limits.IsLimit c →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (P.map π.op) ⋯) ≃
                    CategoryTheory.Limits.IsLimit
                      (P.mapCone (CategoryTheory.Sieve.ofArrows (fun x => X) fun x => π).arrows.cocone.op)
-- Mathlib.CategoryTheory.Adjunction.Reflective
/-- The adjunction `j ⊣ coreflector j` when `j` is coreflective.  -/
CategoryTheory.coreflectorAdjunction : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (j : CategoryTheory.Functor C D) → [inst_2 : CategoryTheory.Coreflective j] → j ⊣ CategoryTheory.coreflector j
-- Mathlib.CategoryTheory.Endomorphism
/-- Automorphisms of an object in a category.

The order of arguments in multiplication agrees with
`Function.comp`, not with `CategoryTheory.CategoryStruct.comp`.
 -/
CategoryTheory.Aut : {C : Type u} → [CategoryTheory.Category.{v, u} C] → C → Type v
-- Mathlib.Data.Finset.Sym
Finset.sym_fill_mem : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α] {n : ℕ} (a : α) {i : Fin (n + 1)} {m : Sym α (n - ↑i)},
  m ∈ s.sym (n - ↑i) → Sym.fill a i m ∈ (insert a s).sym n
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.Flat.instResLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens)
  (e : U ≤ (TopologicalSpace.Opens.map f.base).obj V) [AlgebraicGeometry.Flat f],
  AlgebraicGeometry.Flat (AlgebraicGeometry.Scheme.Hom.resLE f V U e)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal.0.Polynomial.Chebyshev.negOnePow_mul_le : ∀ {α : ℝ} {i : ℕ}, |α| ≤ 1 → (-1) ^ i * α ≤ 1
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.instInhabited : {A : Type u_2} → [inst : Mul A] → [inst_1 : Star A] → Inhabited (A ≃⋆* A)
-- Mathlib.Data.EReal.Basic
EReal.preimage_coe_Ioo_bot : ∀ (y : ℝ), Real.toEReal ⁻¹' Set.Ioo ⊥ ↑y = Set.Iio y
-- Mathlib.Order.Hom.Lattice
SupHom.instSupHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Max β], SupHomClass (SupHom α β) α β
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.nonempty : ∀ {X : Type u_1} [inst : MetricSpace X] [Nonempty X] (D : Delone.DeloneSet X), (↑D).Nonempty
-- Mathlib.NumberTheory.Height.Projectivization
Projectivization.mulHeight_pos : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [inst_2 : Finite ι]
  (x : Projectivization K (ι → K)), 0 < x.mulHeight
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
/-- **Alias** of `Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes`.

---

**Krull's height theorem** (also known as **Krullscher Höhensatz**) :
In a commutative Noetherian ring `R`, any prime ideal that is minimal over an ideal generated
by `n` elements has height at most `n`.  -/
Ideal.height_le_spanRank_toENat_of_mem_minimal_primes : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (I p : Ideal R),
  p ∈ I.minimalPrimes → p.height ≤ Cardinal.toENat (Submodule.spanRank I)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.pi_proj : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_4} {φ : ι → Type u_5} [inst_1 : (i : ι) → TopologicalSpace (φ i)]
  [inst_2 : (i : ι) → AddCommMonoid (φ i)] [inst_3 : (i : ι) → Module R (φ i)],
  ContinuousLinearMap.pi ContinuousLinearMap.proj = ContinuousLinearMap.id R ((i : ι) → φ i)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.ins.eq_4 : ∀ {α : Type u_1} (x : RBTree.RBNode α) (parent : RBTree.RBNode.Path α) (y : α) (b : RBTree.RBNode α),
  (RBTree.RBNode.Path.left RBTree.RBColor.black parent y b).ins x = parent.ins (x.balance1 y b)
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_inter_add_sdiff₀ : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α),
  MeasureTheory.NullMeasurableSet t μ → μ.restrict (s ∩ t) + μ.restrict (s \ t) = μ.restrict s
-- Mathlib.LinearAlgebra.Complex.Module
Complex.coe_algebraMap : ⇑(algebraMap ℝ ℂ) = Complex.ofReal
-- Mathlib.Topology.Connected.TotallyDisconnected
Topology.IsEmbedding.isTotallyDisconnected_range : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Topology.IsEmbedding f → (IsTotallyDisconnected (Set.range f) ↔ TotallyDisconnectedSpace α)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
StrictMono.mul_const' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α}
  [MulRightStrictMono α], StrictMono f → ∀ (c : α), StrictMono fun x => f x * c
-- Mathlib.RingTheory.Derivation.Basic
Derivation.mk : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Algebra R A] →
              [inst_4 : Module A M] →
                [inst_5 : Module R M] →
                  (toLinearMap : A →ₗ[R] M) →
                    toLinearMap 1 = 0 →
                      (∀ (a b : A), toLinearMap (a * b) = a • toLinearMap b + b • toLinearMap a) → Derivation R A M
-- Std.Data.HashMap.Lemmas
Std.HashMap.any_keys : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulHashable α] [EquivBEq α]
  {p : α → Bool}, m.keys.any p = m.any fun a x => p a
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_subset_sdiff_iff_subset`. -/
Set.diff_subset_diff_iff_subset : ∀ {α : Type u_1} {s t r : Set α}, s ⊆ r → t ⊆ r → (r \ s ⊆ r \ t ↔ t ⊆ s)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Replace the indexing type of a `0`-hypercover.  -/
CategoryTheory.Precoverage.ZeroHypercover.reindex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} →
      {T : C} → (E : J.ZeroHypercover T) → {ι : Type w'} → ι ≃ E.I₀ → J.ZeroHypercover T
-- Mathlib.Topology.Separation.Regular
/-- A space is completely normal iff all open subspaces are normal.
 -/
completelyNormalSpace_iff_forall_isOpen_normalSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X], CompletelyNormalSpace X ↔ ∀ (s : Set X), IsOpen s → NormalSpace ↑s
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.tr.match_1.eq_6 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (q : Turing.PartrecToTM2.Λ')
  (h_1 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k₁ k₂ : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (k : Turing.PartrecToTM2.K') →
      (f : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
        (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.push k f q))
  (h_3 : (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (q : Turing.PartrecToTM2.Λ') → motive q.copy) (h_6 : (q : Turing.PartrecToTM2.Λ') → motive q.succ)
  (h_7 : (q₁ q₂ : Turing.PartrecToTM2.Λ') → motive (q₁.pred q₂))
  (h_8 :
    (fs : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k)))
  (h_9 : (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret k.cons₂))
  (h_10 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k)))
  (h_11 :
    (f : Turing.ToPartrec.Code) →
      (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k)))
  (h_12 : Unit → motive (Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt)),
  (match q.succ with
    | Turing.PartrecToTM2.Λ'.move p k₁ k₂ q => h_1 p k₁ k₂ q
    | Turing.PartrecToTM2.Λ'.push k f q => h_2 k f q
    | Turing.PartrecToTM2.Λ'.read q => h_3 q
    | Turing.PartrecToTM2.Λ'.clear p k q => h_4 p k q
    | q.copy => h_5 q
    | q.succ => h_6 q
    | q₁.pred q₂ => h_7 q₁ q₂
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.cons₁ fs k) => h_8 fs k
    | Turing.PartrecToTM2.Λ'.ret k.cons₂ => h_9 k
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.comp f k) => h_10 f k
    | Turing.PartrecToTM2.Λ'.ret (Turing.PartrecToTM2.Cont'.fix f k) => h_11 f k
    | Turing.PartrecToTM2.Λ'.ret Turing.PartrecToTM2.Cont'.halt => h_12 ()) =
    h_6 q
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.quotientSubgroupOfEmbeddingOfLE.eq_1 : ∀ {α : Type u_1} [inst : Group α] {s t : Subgroup α} (H : Subgroup α) (h : s ≤ t),
  Subgroup.quotientSubgroupOfEmbeddingOfLE H h = { toFun := Quotient.map' ⇑(Subgroup.inclusion h) ⋯, inj' := ⋯ }
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.op_f₁₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C), sq.op.f₁₂ = sq.f₂₄.op
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
Valuation.Integers.maximalIdeal_pow_eq_setOfPred_le_v_algebraMap_pow : ∀ {K : Type u_1} {Γ₀ : Type u_2} {O : Type u_3} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : CommRing O] [inst_3 : Algebra O K] {v : Valuation K Γ₀} (hv : v.Integers O)
  [inst_4 : IsDiscreteValuationRing O] {ϖ : O},
  Irreducible ϖ →
    ∀ (n : ℕ), ↑(IsLocalRing.maximalIdeal O ^ n) = {y | v ((algebraMap O K) y) ≤ v ((algebraMap O K) ϖ) ^ n}
-- Mathlib.Topology.Algebra.Equicontinuity
equicontinuous_of_equicontinuousAt_one : ∀ {ι : Type u_1} {G : Type u_2} {M : Type u_3} {hom : Type u_4} [inst : TopologicalSpace G] [inst_1 : UniformSpace M]
  [inst_2 : Group G] [inst_3 : Group M] [IsTopologicalGroup G] [IsUniformGroup M] [inst_6 : FunLike hom G M]
  [MonoidHomClass hom G M] (F : ι → hom), EquicontinuousAt (DFunLike.coe ∘ F) 1 → Equicontinuous (DFunLike.coe ∘ F)
-- Lean.DocString.Extension
Lean.VersoModuleDocs.add : Lean.VersoModuleDocs → Lean.VersoModuleDocs.Snippet → Except String Lean.VersoModuleDocs
-- Init.Data.Vector.Lemmas
Vector.forall_mem_ne' : ∀ {α : Type u_1} {n : ℕ} {a : α} {xs : Vector α n}, (∀ a' ∈ xs, ¬a' = a) ↔ a ∉ xs
-- Mathlib.Algebra.Lie.TraceForm
/-- A variant of `LieModule.traceForm_eq_sum_finrank_nsmul` in which the sum is taken only over the
non-zero weights.  -/
LieModule.traceForm_eq_sum_finrank_nsmul' : ∀ (K : Type u_2) (L : Type u_3) (M : Type u_4) [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M]
  [inst_3 : Field K] [inst_4 : LieAlgebra K L] [inst_5 : Module K M] [inst_6 : LieModule K L M]
  [inst_7 : FiniteDimensional K M] [inst_8 : LieRing.IsNilpotent L] [inst_9 : LieModule.LinearWeights K L M]
  [LieModule.IsTriangularizable K L M],
  LieModule.traceForm K L M =
    ∑ χ with χ.IsNonZero,
      Module.finrank K ↥(LieModule.genWeightSpace M ⇑χ) •
        (LieModule.Weight.toLinear K L M χ).smulRight (LieModule.Weight.toLinear K L M χ)
-- Mathlib.FieldTheory.PerfectClosure
_private.Mathlib.FieldTheory.PerfectClosure.0.PerfectClosure.add_aux_right : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (x y1 y2 : ℕ × K),
  PerfectClosure.R K p y1 y2 →
    PerfectClosure.mk K p (x.1 + y1.1, (⇑(frobenius K p))^[y1.1] x.2 + (⇑(frobenius K p))^[x.1] y1.2) =
      PerfectClosure.mk K p (x.1 + y2.1, (⇑(frobenius K p))^[y2.1] x.2 + (⇑(frobenius K p))^[x.1] y2.2)
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroupClass.toAddCommGroup.eq_1 : ∀ {S : Type u_4} (H : S) {G : Type u_5} [inst : AddCommGroup G] [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G],
  AddSubgroupClass.toAddCommGroup H = { toAddGroup := AddSubgroupClass.toAddGroup H, add_comm := ⋯ }
-- Init.Control.Except
instMonadControlExceptTOfMonad : (ε : Type u) → (m : Type u → Type v) → [Monad m] → MonadControl m (ExceptT ε m)
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_singleton_zero : ∀ {α : Type u} [inst : Semiring α], Ideal.span {0} = ⊥
-- Init.Data.Array.Lemmas
Array.foldr_flatten : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → β} {b : β} {xss : Array (Array α)},
  Array.foldr f b xss.flatten = Array.foldr (fun xs b => Array.foldr f b xs) b xss
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.instMonoCoprodOfFinitaryExtensive : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.FinitaryExtensive C],
  CategoryTheory.Limits.MonoCoprod C
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.instInfSet : {G : Type u_1} → [inst : AddGroup G] → InfSet (AddSubgroup G)
-- Init.Prelude
/-- The notation typeclass for negation.
This enables the notation `-a : α` where `a : α`.
 -/
Neg : Type u → Type u
-- Mathlib.Data.Finset.Card
/-- Given a function `f` which sends the finite set `s` to itself, the sequence of images of `s` under
iterates of `f` is eventually constant. Furthermore, the sequence of images stabilises in at most
`#s` steps.
 -/
Finset.image_iterate_stabilises_le_card : ∀ {α : Type u_1} [inst : DecidableEq α] {f : α → α} {s : Finset α},
  Set.MapsTo f ↑s ↑s → ∃ n ≤ s.card, ∀ (m : ℕ), n ≤ m → Finset.image f^[m] s = Finset.image f^[n] s
-- Mathlib.MeasureTheory.Function.LpOrder
MeasureTheory.Lp.instAddLeftMono : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal}
  [inst : NormedAddCommGroup E] [inst_1 : PartialOrder E] [IsOrderedAddMonoid E], AddLeftMono ↥(MeasureTheory.Lp E p μ)
-- Mathlib.Algebra.Category.CommAlgCat.Basic
/-- Build an `AlgEquiv` from an isomorphism in the category `CommAlgCat R`.  -/
CommAlgCat.algEquivOfIso : {R : Type u} → [inst : CommRing R] → {A B : CommAlgCat R} → (A ≅ B) → ↑A ≃ₐ[R] ↑B
-- Aesop.BuiltinRules.DestructProducts
_private.Aesop.BuiltinRules.DestructProducts.0.Aesop.BuiltinRules.destructProductsCore.go : Lean.Meta.TransparencyMode → ℕ → Lean.MVarId → Aesop.ScriptM Lean.MVarId
-- Mathlib.Data.DFinsupp.Defs
/-- Reindexing (and possibly removing) terms of a dfinsupp.  -/
DFinsupp.comapDomain : {ι : Type u} →
  {β : ι → Type v} →
    {κ : Type u_1} →
      [inst : (i : ι) → Zero (β i)] → (h : κ → ι) → Function.Injective h → (Π₀ (i : ι), β i) → Π₀ (k : κ), β (h k)
-- Init.Data.String.Basic
/-- Returns the next position in a string after position `p`. If `p` is not a valid position or
`p = s.endPos`, returns the position one byte after `p`.

A run-time bounds check is performed to determine whether `p` is at the end of the string. If a
bounds check has already been performed, use `String.next'` to avoid a repeated check.

This is a legacy function. The recommended alternative is `String.Pos.next` or one of its
variants like `String.Pos.next?`, combined with `String.pos` or another means of obtaining
a `String.ValisPos`.

Some examples of edge cases:
* `"abc".next ⟨3⟩ = ⟨4⟩`, since `3 = "abc".endPos`
* `"L∃∀N".next ⟨2⟩ = ⟨3⟩`, since `2` points into the middle of a multi-byte UTF-8 character

Examples:
* `"abc".get ("abc".next 0) = 'b'`
* `"L∃∀N".get (0 |> "L∃∀N".next |> "L∃∀N".next) = '∀'`
 -/
String.Pos.Raw.next : String → String.Pos.Raw → String.Pos.Raw
-- Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
/-- The value of a convex function applied at a Radon-Nikodym derivative can be bounded by the
integral of the function applied to the Radon-Nikodym derivative of composition-products.  -/
ConvexOn.apply_rnDeriv_ae_le_integral : ∀ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} {𝓨 : Type u_2} {m𝓨 : MeasurableSpace 𝓨}
  {κ η : ProbabilityTheory.Kernel 𝓧 𝓨} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν]
  [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η],
  MeasureTheory.StronglyMeasurable f →
    ConvexOn ℝ (Set.Ici 0) f →
      ContinuousWithinAt f (Set.Ici 0) 0 →
        MeasureTheory.Integrable (fun p => f ((μ.compProd κ).rnDeriv (ν.compProd η) p).toReal) (ν.compProd η) →
          (μ.compProd κ).AbsolutelyContinuous (μ.compProd η) →
            (fun a => f (μ.rnDeriv ν a).toReal) ≤ᵐ[ν] fun a =>
              ∫ (b : 𝓨), f ((μ.compProd κ).rnDeriv (ν.compProd η) (a, b)).toReal ∂η a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.keysArray.size = t.size