mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Perfection
/-- **Alias** of `Perfection.subring`.

---

`Perfection R p` as a semiring of `ℕ → R`.  -/
Ring.perfectionSubring : (R : Type u_1) → [inst : CommRing R] → (p : ℕ) → [hp : Fact (Nat.Prime p)] → [CharP R p] → Subring (ℕ → R)
-- Mathlib.Topology.Order
continuous_iff_le_induced : ∀ {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace β},
  Continuous f ↔ t₁ ≤ TopologicalSpace.induced f t₂
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_le_of_le_right : ∀ {G : Type u_1} [inst : AddGroup G] {H K L : AddSubgroup G}, K ≤ L → H.relIndex L ≠ 0 → H.relIndex K ≤ H.relIndex L
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RocSliceData : (α : Type u) → [Ord α] → Type u
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.instSetoid : {X Y : AlgebraicGeometry.Scheme} → Setoid (X.PartialMap Y)
-- Mathlib.CategoryTheory.Join.Basic
/-- Any functor out of a join is naturally isomorphic to a functor of the form `mkFunctor F G α`.  -/
CategoryTheory.Join.isoMkFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (F : CategoryTheory.Functor (CategoryTheory.Join C D) E) →
              F ≅
                CategoryTheory.Join.mkFunctor ((CategoryTheory.Join.inclLeft C D).comp F)
                  ((CategoryTheory.Join.inclRight C D).comp F)
                  (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F)
-- Mathlib.Algebra.Homology.BifunctorHomotopy
/-- The homotopy between `mapBifunctorMap f₁ f₂ F c` and `mapBifunctorMap f₁ f₂' F c` that
is induced by a homotopy between `f₂` and `f₂'`.  -/
HomologicalComplex.mapBifunctorMapHomotopy₂ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      {I₁ : Type u_4} →
        {I₂ : Type u_5} →
          {J : Type u_6} →
            [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
              [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
                [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
                  [inst_3 : CategoryTheory.Preadditive C₁] →
                    [inst_4 : CategoryTheory.Preadditive C₂] →
                      [inst_5 : CategoryTheory.Preadditive D] →
                        {c₁ : ComplexShape I₁} →
                          {c₂ : ComplexShape I₂} →
                            {K₁ L₁ : HomologicalComplex C₁ c₁} →
                              (f₁ : K₁ ⟶ L₁) →
                                {K₂ L₂ : HomologicalComplex C₂ c₂} →
                                  {f₂ f₂' : K₂ ⟶ L₂} →
                                    Homotopy f₂ f₂' →
                                      (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                                        [inst_6 : F.Additive] →
                                          [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] →
                                            (c : ComplexShape J) →
                                              [inst_8 : DecidableEq J] →
                                                [inst_9 : TotalComplexShape c₁ c₂ c] →
                                                  [inst_10 : K₁.HasMapBifunctor K₂ F c] →
                                                    [inst_11 : L₁.HasMapBifunctor L₂ F c] →
                                                      Homotopy (HomologicalComplex.mapBifunctorMap f₁ f₂ F c)
                                                        (HomologicalComplex.mapBifunctorMap f₁ f₂' F c)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- Satisfying the inhabited linter  -/
CategoryTheory.Limits.instInhabitedHomZero : (J : Type v) →
  Inhabited
    (CategoryTheory.Limits.WalkingParallelFamily.Hom J CategoryTheory.Limits.WalkingParallelFamily.zero
      CategoryTheory.Limits.WalkingParallelFamily.zero)
-- Mathlib.Order.SuccPred.Basic
/-- **Alias** of `Order.succ_le_of_lt`. -/
LT.lt.succ_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α}, a < b → Order.succ a ≤ b
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.comap_lt_comap_of_root_mem_sdiff : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {f : R →+* S} {I J : Ideal S} [I.IsPrime],
  I ≤ J →
    ∀ {r : S},
      r ∈ ↑J \ ↑I →
        ∀ {p : Polynomial R},
          Polynomial.map (Ideal.Quotient.mk (Ideal.comap f I)) p ≠ 0 →
            Polynomial.eval₂ f r p ∈ I → Ideal.comap f I < Ideal.comap f J
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.one_le_order_iff_constCoeff_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R}, 1 ≤ φ.order ↔ PowerSeries.constantCoeff φ = 0
-- Mathlib.Order.Basic
Pi.hnot_def : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → HNot (π i)] (x : (i : ι) → π i), ￢x = fun i => ￢x i
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_subset_Ioo_left : ∀ {α : Type u_2} {a₁ a₂ b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α],
  a₁ < a₂ → Finset.Ico a₂ b ⊆ Finset.Ioo a₁ b
-- Mathlib.Data.Rat.Lemmas
Rat.add_den_dvd_lcm : ∀ (q₁ q₂ : ℚ), (q₁ + q₂).den ∣ q₁.den.lcm q₂.den
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
/-- The linear equivalence between `n × n` matrices and sesquilinear maps on `n → R`  -/
Matrix.toLinearMapₛₗ₂' : (R : Type u_1) →
  {R₁ : Type u_2} →
    {S₁ : Type u_3} →
      {R₂ : Type u_4} →
        {S₂ : Type u_5} →
          {N₂ : Type u_10} →
            {n : Type u_11} →
              {m : Type u_12} →
                [inst : CommSemiring R] →
                  [inst_1 : AddCommMonoid N₂] →
                    [inst_2 : Module R N₂] →
                      [inst_3 : Semiring R₁] →
                        [inst_4 : Semiring R₂] →
                          [inst_5 : Semiring S₁] →
                            [inst_6 : Semiring S₂] →
                              [inst_7 : Module S₁ N₂] →
                                [inst_8 : Module S₂ N₂] →
                                  [inst_9 : SMulCommClass S₁ R N₂] →
                                    [inst_10 : SMulCommClass S₂ R N₂] →
                                      [inst_11 : SMulCommClass S₂ S₁ N₂] →
                                        (σ₁ : R₁ →+* S₁) →
                                          (σ₂ : R₂ →+* S₂) →
                                            [Fintype n] →
                                              [Fintype m] →
                                                [DecidableEq n] →
                                                  [DecidableEq m] →
                                                    Matrix n m N₂ ≃ₗ[R] (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂
-- Mathlib.Algebra.Order.IsBotOne
/-- **Alias** of `Ne.one_lt`.

---

**Alias** of `one_lt_of_ne_one`.

---

**Alias** of the reverse direction of `one_lt_iff_ne_one`. -/
NE.ne.one_lt : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : One α] [IsBotOneClass α], a ≠ 1 → 1 < a
-- Mathlib.FieldTheory.Finite.Extension
FiniteField.instFiniteExtension_1 : ∀ (k : Type u_1) [inst : Field k] [inst_1 : Finite k] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] [inst_3 : CharP k p] (n : ℕ)
  [inst_4 : NeZero n], Module.Finite k (FiniteField.Extension k p n)
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_hom_τ₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  {T T' : CategoryTheory.Pretriangulated.Triangle C} (e : T ≅ T')
  (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
  (CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso e hT).hom.τ₂ = e.hom.hom₂
-- Mathlib.Logic.Equiv.Fin.Basic
finSumNatEquiv_symm_apply_of_lt : ∀ {n i : ℕ} (hi : i < n), (finSumNatEquiv n).symm i = Sum.inl ⟨i, hi⟩
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceTDiv : Lean.Meta.Simp.DSimproc
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPolynomial.coe_injective : ∀ (σ : Type u_1) (R : Type u_2) [inst : CommSemiring R], Function.Injective MvPolynomial.toMvPowerSeries
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_comapDomain : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {α' : Type u_7} {v : α → M} (f : α → α') (l : α' →₀ R) (hf : Set.InjOn f (f ⁻¹' ↑l.support)),
  (Finsupp.linearCombination R v) (Finsupp.comapDomain f l hf) = ∑ i ∈ l.support.preimage f hf, l (f i) • v i
-- Mathlib.Topology.NhdsKer
nhdsKer_mono : ∀ {X : Type u_2} [inst : TopologicalSpace X], Monotone nhdsKer
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
/-- Auxiliary lemma used in the proof of `setIntegral_condExpL1CLM`.  -/
MeasureTheory.setIntegral_condExpL1CLM_of_measure_ne_top : ∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] {s : Set α}
  [inst_3 : CompleteSpace F'] (f : ↥(MeasureTheory.Lp F' 1 μ)),
  MeasurableSet s → μ s ≠ ⊤ → ∫ (x : α) in s, ↑↑((MeasureTheory.condExpL1CLM F' hm μ) f) x ∂μ = ∫ (x : α) in s, ↑↑f x ∂μ
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasFDerivAt.neg : ∀ {𝕜 : 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] {f : E → F}
  {f' : E →L[𝕜] F} {x : E}, HasFDerivAt f f' x → HasFDerivAt (-f) (-f') x
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.instPreadditive : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      [inst_2 : CategoryTheory.Preadditive C] →
        [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
          CategoryTheory.Preadditive (CategoryTheory.Pretriangulated.Triangle C)
-- Mathlib.Data.Sym.Sym2
Sym2.other_spec : ∀ {α : Type u_1} {a : α} {z : Sym2 α} (h : a ∈ z), s(a, Sym2.Mem.other h) = z
-- Aesop.Frontend.Saturate
Aesop.Frontend.Parser.additionalRules : Lean.ParserDescr
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientAlgebra : {A : Type u_3} →
  [inst : Ring A] →
    {R : Type u_5} →
      [inst_1 : CommRing R] →
        {I : Ideal A} →
          [inst_2 : I.IsTwoSided] → [inst_3 : Algebra R A] → Algebra (R ⧸ Ideal.comap (algebraMap R A) I) (A ⧸ I)
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.filterMapM_cons.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.Data.Nat.Squarefree
Nat.divisors_filter_squarefree : ∀ {n : ℕ},
  n ≠ 0 →
    {d ∈ n.divisors | Squarefree d}.val =
      Multiset.map (fun x => x.val.prod) (UniqueFactorizationMonoid.normalizedFactors n).toFinset.powerset.val
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.MonOpOpToComonObj_comon_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Mon Cᵒᵖ), CategoryTheory.ComonObj.counit = CategoryTheory.MonObj.one.unop
-- Std.Time.Date.Unit.Day
/-- `OfYear` represents the day ordinal within a year, which can be bounded between 1 and 365 or 366,
depending on whether it's a leap year.
 -/
Std.Time.Day.Ordinal.OfYear : Bool → Type
-- Mathlib.Combinatorics.Additive.DoublingConst
/-- If `A` has small doubling, then it has small difference, with the constant squared.

This is a consequence of the Ruzsa triangle inequality.  -/
Finset.subConst_le_addConst_sq : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {A : Finset G}, A.subConst A ≤ A.addConst A ^ 2
-- Init.Data.String.Lemmas.Iterate
String.foldr_eq_foldr_toList : ∀ {α : Type u} {f : Char → α → α} {init : α} {s : String}, String.foldr f init s = List.foldr f init s.toList
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.exchange_mem : ∀ {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α} {e : α},
  M.IsBase B₁ → M.IsBase B₂ → e ∈ B₁ → e ∉ B₂ → ∃ y, (y ∈ B₂ ∧ y ∉ B₁) ∧ M.IsBase (insert y (B₁ \ {e}))
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.leftDistribClass : LeftDistribClass Ordinal.{u_4}
-- Std.Data.Internal.List.Associative
Std.Internal.List.Option.filter_or : ∀ {α : Type u} {o : Option α} {p q : α → Bool},
  Option.filter (fun a => p a || q a) o = (Option.filter p o).or (Option.filter q o)
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- The L-function of an even Dirichlet character vanishes at strictly negative even integers.  -/
DirichletCharacter.Even.LFunction_neg_two_mul_nat : ∀ {N : ℕ} [inst : NeZero N] {χ : DirichletCharacter ℂ N},
  χ.Even → ∀ (n : ℕ) [NeZero n], DirichletCharacter.LFunction χ (-(2 * ↑n)) = 0
-- Mathlib.Topology.UniformSpace.Basic
SetRel.image.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β) (s : Set α), R.image s = {b | ∃ a ∈ s, (a, b) ∈ R}
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.prod_ε_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E] {C' : Type u₁'}
  [inst_6 : CategoryTheory.Category.{v₁', u₁'} C'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor E C')
  [inst_7 : CategoryTheory.MonoidalCategory C'] [inst_8 : F.LaxMonoidal] [inst_9 : G.LaxMonoidal],
  (CategoryTheory.Functor.LaxMonoidal.ε (F.prod G)).2 = CategoryTheory.Functor.LaxMonoidal.ε G
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitCoyonedaHomIsoLimit_π_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (D : CategoryTheory.Functor Iᵒᵖ C) (F : CategoryTheory.Functor C (Type u₂))
  [inst_2 : CategoryTheory.Limits.HasColimit (D.rightOp.comp CategoryTheory.coyoneda)]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))]
  (f : CategoryTheory.Limits.colimit (D.rightOp.comp CategoryTheory.coyoneda) ⟶ F) (i : I),
  (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.Limits.limit.π (D.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂})) (Opposite.op i)))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimitCoyonedaHomIsoLimit D F).hom) f) =
    {
      down :=
        (CategoryTheory.ConcreteCategory.hom (f.app (D.obj (Opposite.op i))))
          ((CategoryTheory.ConcreteCategory.hom
              ((CategoryTheory.Limits.colimit.ι (D.rightOp.comp CategoryTheory.coyoneda) i).app
                (D.obj (Opposite.op i))))
            (CategoryTheory.CategoryStruct.id (D.obj (Opposite.op i)))) }
-- Init.Data.String.Lemmas.FindPos
String.Pos.prev_ofSliceTo : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {h : String.Pos.ofSliceTo p ≠ s.startPos},
  (String.Pos.ofSliceTo p).prev h = String.Pos.ofSliceTo (p.prev ⋯)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.δ_rightUnshift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {a n' : ℤ}
  (γ : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ)
  (hn : n' + a = n) (m m' : ℤ) (hm' : m' + a = m),
  CochainComplex.HomComplex.δ n m (γ.rightUnshift n hn) =
    a.negOnePow • (CochainComplex.HomComplex.δ n' m' γ).rightUnshift m hm'
-- Mathlib.Algebra.Polynomial.Eval.Algebra
Polynomial.eval₂_mul' : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (x : S)
  (p q : Polynomial R),
  Polynomial.eval₂ (algebraMap R S) x (p * q) =
    Polynomial.eval₂ (algebraMap R S) x p * Polynomial.eval₂ (algebraMap R S) x q
-- Init.Data.String.Decode
ByteArray.validateUTF8At.eq_1 : ∀ (bytes : ByteArray) (i : ℕ),
  bytes.validateUTF8At i =
    if h₀ : i < bytes.size then
      match h : ByteArray.utf8DecodeChar?.parseFirstByte bytes[i] with
      | ByteArray.utf8DecodeChar?.FirstByte.invalid => false
      | ByteArray.utf8DecodeChar?.FirstByte.done => ByteArray.utf8DecodeChar?.verify₁ bytes[i] h
      | ByteArray.utf8DecodeChar?.FirstByte.oneMore =>
        if h₁ : i + 1 < bytes.size then ByteArray.utf8DecodeChar?.verify₂ bytes[i] bytes[i + 1] else false
      | ByteArray.utf8DecodeChar?.FirstByte.twoMore =>
        if h₁ : i + 2 < bytes.size then ByteArray.utf8DecodeChar?.verify₃ bytes[i] bytes[i + 1] bytes[i + 2] else false
      | ByteArray.utf8DecodeChar?.FirstByte.threeMore =>
        if h₁ : i + 3 < bytes.size then
          ByteArray.utf8DecodeChar?.verify₄ bytes[i] bytes[i + 1] bytes[i + 2] bytes[i + 3]
        else false
    else false
-- Mathlib.CategoryTheory.PEmpty
/-- Any functor out of the empty category is isomorphic to the canonical functor from the empty
category.
 -/
CategoryTheory.Functor.uniqueFromEmpty : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1}) C) → F ≅ CategoryTheory.Functor.empty C
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {l : List α} {k : α},
  k ∉ m → l.contains k = false → (Std.ExtDHashMap.Const.insertManyIfNewUnit m l).getKey! k = default
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.BodyInfo.mk : Option Lean.Expr → Lean.Elab.Term.BodyInfo
-- Mathlib.Data.WSeq.Basic
/-- Encode a computation yielding a weak sequence into additional
`think` constructors in a weak sequence  -/
Stream'.WSeq.flatten : {α : Type u} → Computation (Stream'.WSeq α) → Stream'.WSeq α
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.rCond_of_bRiemann_eq_false : ∀ {ι : Type u_2} (l : BoxIntegral.IntegrationParams), l.bRiemann = false → ∀ {r : (ι → ℝ) → ↑(Set.Ioi 0)}, l.RCond r
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.mk'.eq_1 : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal],
  QuotientGroup.mk' N = MonoidHom.mk' QuotientGroup.mk ⋯
-- Mathlib.Order.Filter.Pointwise
Filter.HasBasis.add : ∀ {α : Type u_2} [inst : Add α] {f g : Filter α} {ιf : Type u_7} {ιg : Type u_8} {pf : ιf → Prop} {sf : ιf → Set α}
  {pg : ιg → Prop} {sg : ιg → Set α},
  f.HasBasis pf sf → g.HasBasis pg sg → (f + g).HasBasis (fun i => pf i.1 ∧ pg i.2) fun i => sf i.1 + sg i.2
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
galRestrict'_galLift : ∀ {A : Type u_1} (K : Type u_2) (L : Type u_3) (L₂ : Type u_4) {B : Type u_6} {B₂ : Type u_7} [inst : CommRing A]
  [inst_1 : CommRing B] [inst_2 : CommRing B₂] [inst_3 : Algebra A B] [inst_4 : Algebra A B₂] [inst_5 : Field K]
  [inst_6 : Field L] [inst_7 : Field L₂] [inst_8 : Algebra A K] [inst_9 : IsFractionRing A K] [inst_10 : Algebra K L]
  [inst_11 : Algebra A L] [inst_12 : IsScalarTower A K L] [inst_13 : Algebra K L₂] [inst_14 : Algebra A L₂]
  [inst_15 : IsScalarTower A K L₂] [inst_16 : Algebra B L] [inst_17 : IsScalarTower A B L]
  [inst_18 : IsIntegralClosure B A L] [inst_19 : Algebra B₂ L₂] [inst_20 : IsScalarTower A B₂ L₂]
  [inst_21 : IsIntegralClosure B₂ A L₂] [inst_22 : Algebra.IsAlgebraic K L] (σ : B →ₐ[A] B₂),
  galRestrict' A B B₂ (galLift K L L₂ σ) = σ
-- Init.Internal.Order.Basic
Lean.Order.instCCPOOptionT : {m : Type u_1 → Type u_2} →
  {α : Type u_1} → [inst : (α : Type u_1) → Lean.Order.CCPO (m α)] → Lean.Order.CCPO (OptionT m α)
-- Mathlib.Analysis.Normed.Algebra.GelfandFormula
spectrum.hasFDerivAt_resolvent : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] {a : A} {k : 𝕜},
  k ∈ resolventSet 𝕜 a →
    HasFDerivAt (fun x => resolvent x k) (((ContinuousLinearMap.mulLeftRight 𝕜 A) (resolvent a k)) (resolvent a k)) a
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.lt_sliceFrom_iff : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos} {h : p₀ ≤ q},
  p < p₀.sliceFrom q h ↔ String.Slice.Pos.ofSliceFrom p < q
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.forIn'_eq_match_step : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] {n : Type w → Type w''}
  [inst_2 : Monad m] [inst_3 : Monad n] [LawfulMonad n] [inst_5 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_7 : MonadLiftT m n] [LawfulMonadLiftT m n] {γ : Type w} {it : Std.IterM m β} {init : γ}
  {f : (out : β) → out ∈ it → γ → n (ForInStep γ)},
  forIn' it init f = do
    let __do_lift ← liftM it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ => do
        let __do_lift ← f out ⋯ init
        match __do_lift with
          | ForInStep.yield c => forIn' it' c fun out_1 h'' acc => f out_1 ⋯ acc
          | ForInStep.done c => pure c
      | ⟨Std.IterStep.skip it', h⟩ => forIn' it' init fun out h' acc => f out ⋯ acc
      | ⟨Std.IterStep.done, property⟩ => pure init
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.instDecidableEqPresburgerFunc : {a : ℕ} → DecidableEq (FirstOrder.presburgerFunc a)
-- Mathlib.Analysis.Matrix.Normed
Matrix.norm_conjTranspose : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] [inst_3 : StarAddMonoid α] [NormedStarGroup α] (A : Matrix m n α),
  ‖A.conjTranspose‖ = ‖A‖
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- If `f` embeds `X` into a compact Hausdorff space `Y`, and has exactly one point outside its
range, then `(Y, f)` is the one-point compactification of `X`.  -/
OnePoint.equivOfIsEmbeddingOfRangeEq : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        [T2Space Y] →
          [CompactSpace Y] → (y : Y) → (f : X → Y) → Topology.IsEmbedding f → Set.range f = {y}ᶜ → OnePoint X ≃ₜ Y
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanIso.mk : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {n : ℕ} {A : Set α} {B : Set β}
  {f : α → β},
  Set.BijOn f A B →
    (∀ ⦃s t : Multiset α⦄,
        (∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
          (∀ ⦃x : α⦄, x ∈ t → x ∈ A) →
            s.card = n → t.card = n → ((Multiset.map f s).prod = (Multiset.map f t).prod ↔ s.prod = t.prod)) →
      IsMulFreimanIso n A B f
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
/-- A simplicial set has dimension `≤ d` if it has dimension `< d + 1`.  -/
SSet.HasDimensionLE : SSet → ℕ → Prop
-- Mathlib.Algebra.Homology.Embedding.StupidTrunc
HomologicalComplex.stupidTruncXIso.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c')
  [inst_3 : e.IsRelIff] {i i_1 : ι} (e_i : i = i_1) {i' : ι'} (hi' : e.f i = i'),
  K.stupidTruncXIso e hi' = K.stupidTruncXIso e ⋯
-- Mathlib.GroupTheory.OrderOfElement
Pi.orderOf_eq_sInf : ∀ {ι : Type u_6} {α : ι → Type u_7} [inst : (i : ι) → Monoid (α i)] (x : (i : ι) → α i),
  orderOf x = sInf {n | n > 0 ∧ ∀ (i : ι), orderOf (x i) ∣ n}