mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Grothendieck
/-- Given a functor `F : C ⥤ Cat` and an equivalence of categories `G : D ≌ C`, the functor
`pre F G.functor` is an equivalence between `Grothendieck (G.functor ⋙ F)` and `Grothendieck F`.
 -/
CategoryTheory.Grothendieck.preEquivalence : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} D] →
        (F : CategoryTheory.Functor C CategoryTheory.Cat) →
          (G : D ≌ C) → CategoryTheory.Grothendieck (G.functor.comp F) ≌ CategoryTheory.Grothendieck F
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Complex.deriv_cpow_const : ∀ {x c : ℂ}, x ∈ Complex.slitPlane → deriv (fun x => x ^ c) x = c * x ^ (c - 1)
-- Init.Data.Array.Lemmas
Array.foldl_append' : ∀ {α : Type u_1} {β : Type u_2} {f : β → α → β} {b : β} {xs ys : Array α} {stop : ℕ},
  stop = xs.size + ys.size → Array.foldl f b (xs ++ ys) 0 stop = Array.foldl f (Array.foldl f b xs) ys
-- Mathlib.Algebra.Group.AddChar
AddChar.toMonoidHomEquiv_add : ∀ {A : Type u_2} {M : Type u_3} [inst : AddMonoid A] [inst_1 : CommMonoid M] (ψ φ : AddChar A M),
  AddChar.toMonoidHomEquiv (ψ + φ) = AddChar.toMonoidHomEquiv ψ * AddChar.toMonoidHomEquiv φ
-- Mathlib.Topology.Algebra.Algebra
toLinearMap_algebraMapCLM : ∀ (R : Type u_1) (A : Type u) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : TopologicalSpace R] [inst_4 : TopologicalSpace A] [inst_5 : ContinuousSMul R A],
  ↑(algebraMapCLM R A) = Algebra.linearMap R A
-- Batteries.Lean.LawfulMonadLift
instLawfulMonadLiftTEIOExceptionCoreM_batteries : LawfulMonadLiftT (EIO Lean.Exception) Lean.CoreM
-- Mathlib.Data.Ordmap.Ordnode
_private.Mathlib.Data.Ordmap.Ordnode.0.Ordnode.ofAscListAux₁.match_3.eq_1 : ∀ {α : Type u_1} (xs : List α) (motive : Ordnode α × { l' // l'.length ≤ xs.length } → Sort u_2) (t : Ordnode α)
  (property : [].length ≤ xs.length)
  (h_1 : (t : Ordnode α) → (property : [].length ≤ xs.length) → motive (t, ⟨[], property⟩))
  (h_2 : (l : Ordnode α) → (y : α) → (ys : List α) → (h : (y :: ys).length ≤ xs.length) → motive (l, ⟨y :: ys, h⟩)),
  (match (t, ⟨[], property⟩) with
    | (t, ⟨[], property⟩) => h_1 t property
    | (l, ⟨y :: ys, h⟩) => h_2 l y ys h) =
    h_1 t property
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- The `n+1`-th iterated derivative within a set with unique derivatives can be obtained by
taking the `n`-th derivative of the derivative.  -/
iteratedDerivWithin_succ' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜},
  iteratedDerivWithin (n + 1) f s = iteratedDerivWithin n (derivWithin f s) s
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.covering_of_eq_top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X}
  (J : CategoryTheory.GrothendieckTopology C), S = ⊤ → S ∈ J X
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.forget₂_coalgebra_map : ∀ {R : Type u} [inst : CommRing R] (X Y : BialgCat R) (f : X ⟶ Y),
  (CategoryTheory.forget₂ (BialgCat R) (CoalgCat R)).map f = CoalgCat.ofHom ↑(BialgCat.Hom.toBialgHom f)
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.ext : ∀ {X Y : AddCommMonCat} {f g : X ⟶ Y},
  (∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.Data.Finset.Sum
Finset.fold_disjSum : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Finset α) (t : Finset β) (f : α ⊕ β → γ) (b₁ b₂ : γ)
  (op : γ → γ → γ) [inst : Std.Commutative op] [inst_1 : Std.Associative op],
  Finset.fold op (op b₁ b₂) f (s.disjSum t) =
    op (Finset.fold op b₁ (fun x => f (Sum.inl x)) s) (Finset.fold op b₂ (fun x => f (Sum.inr x)) t)
-- Mathlib.Data.Multiset.UnionInter
Multiset.union_zero : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Multiset α}, s ∪ 0 = s
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_div_const_Ici : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => x / a) '' Set.Ici b = Set.Ici (b / a)
-- Mathlib.Data.List.Sort
/-- A version of `insertionSort_stable` which only assumes `c <+~ l` (instead of `c <+ l`), but
additionally requires `Std.Antisymm r`, `Std.Total r` and `IsTrans α r`.
 -/
List.sublist_insertionSort' : ∀ {α : Type u_1} {r : α → α → Prop} [inst : DecidableRel r] [Std.Antisymm r] [Std.Total r] [IsTrans α r] {l c : List α},
  List.Pairwise r c → c.Subperm l → c.Sublist (List.insertionSort r l)
-- Lean.DocString.Extension
/-- A custom block element `val`. The type `α` determines how it is interpreted. In contexts where `α`
is not understood, `content` is used as a fallback.
 -/
Lean.Doc.Block.custom : {α : Type u_1} →
  [TypeName α] →
    α → Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock) → Lean.Doc.Block Lean.ElabInline Lean.ElabBlock
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k : α},
  Std.ExtDHashMap.Const.get? (Std.ExtDHashMap.Const.insertMany m l) k =
    (List.findSomeRev?
          (fun x_2 =>
            match x_2 with
            | (a, b) => if (a == k) = true then some b else none)
          l).or
      (Std.ExtDHashMap.Const.get? m k)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.brecOn_3.go : {motive_1 : Lean.Elab.Term.Do.Code → Sort u} →
  {motive_2 : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u} →
    {motive_3 : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u} →
      {motive_4 : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u} →
        {motive_5 : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u} →
          {motive_6 : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code → Sort u} →
            {motive_7 : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code → Sort u} →
              (t : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) →
                ((t : Lean.Elab.Term.Do.Code) → t.below → motive_1 t) →
                  ((t : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) →
                      Lean.Elab.Term.Do.Code.below_1 t → motive_2 t) →
                    ((t : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) →
                        Lean.Elab.Term.Do.Code.below_2 t → motive_3 t) →
                      ((t : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) →
                          Lean.Elab.Term.Do.Code.below_3 t → motive_4 t) →
                        ((t : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) →
                            Lean.Elab.Term.Do.Code.below_4 t → motive_5 t) →
                          ((t : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) →
                              Lean.Elab.Term.Do.Code.below_5 t → motive_6 t) →
                            ((t : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) →
                                Lean.Elab.Term.Do.Code.below_6 t → motive_7 t) →
                              motive_4 t ×' Lean.Elab.Term.Do.Code.below_3 t
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trLList.match_1.splitter : (motive : List (List ℕ) → Sort u_1) →
  (x : List (List ℕ)) → (Unit → motive []) → ((l : List ℕ) → (ls : List (List ℕ)) → motive (l :: ls)) → motive x
-- Mathlib.Logic.Function.Basic
/-- Evaluate a function at an argument. Useful if you want to talk about the partially applied
`Function.eval x : (∀ x, β x) → β x`.  -/
Function.eval : {α : Sort u_1} → {β : α → Sort u_4} → (x : α) → ((x : α) → β x) → β x
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.fromCostructuredArrow_obj_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)) {X : C}
  (f : CategoryTheory.yoneda.obj X ⟶ F),
  (CategoryTheory.CategoryOfElements.fromCostructuredArrow F).obj
      (Opposite.op (CategoryTheory.CostructuredArrow.mk f)) =
    ⟨Opposite.op X, CategoryTheory.yonedaEquiv.toFun f⟩
-- Mathlib.Algebra.Group.Basic
one_sub_natCast_zsmul : ∀ {G : Type u_3} [inst : AddGroup G] (a : G) (n : ℕ), (1 - ↑n) • a = a - n • a
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.forIn_filterWithPostcondition : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w}
  [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Monad o]
  [inst_5 : Std.Internal.Do.Assertion Pred] [inst_6 : Std.Internal.Do.Assertion EPred]
  [inst_7 : Std.Internal.Do.WPMonad o Pred EPred] [inst_8 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst_10 : MonadLiftT n o] [LawfulMonadLiftT n o] [inst_12 : Std.Iterator α m β] [Std.Iterators.Finite α m]
  [inst_14 : Std.IteratorLoop α m o] [Std.LawfulIteratorLoop α m o] {it : Std.IterM m β}
  {f : β → Std.Iterators.PostconditionT n (ULift.{w, 0} Bool)} {init : γ} {g : β → γ → o (ForInStep γ)} {P : Pred}
  {Q : γ → Pred} {eQ : EPred},
  ⦃ P ⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out).run
        if __do_lift.down = true then g out acc else pure (ForInStep.yield acc) ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ forIn (Std.IterM.filterWithPostcondition f it) init g ⦃ Q; eQ ⦄
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.smul_set_subset_iff₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α},
  a ≠ 0 → ∀ {A B : Set β}, a • A ⊆ B ↔ A ⊆ a⁻¹ • B
-- Mathlib.Topology.UniformSpace.Path
/-- The space of paths between two points in a complete uniform space
is a complete uniform space.  -/
Path.instCompleteSpace : ∀ {X : Type u_1} [inst : UniformSpace X] {x y : X} [CompleteSpace X], CompleteSpace (Path x y)
-- Mathlib.RingTheory.Congruence.Opposite
/-- If `c` is a `RingCon R`, then `(a, b) ↦ c b.unop a.unop` is a `RingCon Rᵐᵒᵖ`.
 -/
RingCon.op : {R : Type u_1} → [inst : Add R] → [inst_1 : Mul R] → RingCon R → RingCon Rᵐᵒᵖ
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.instInhabitedIndGroupInfo.default : Lean.Elab.Structural.IndGroupInfo
-- Mathlib.MeasureTheory.Category.MeasCat
MeasCat.instLargeCategory : CategoryTheory.LargeCategory MeasCat
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.ker.condition_assoc : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] {Z : CategoryTheory.Functor (CategoryTheory.Arrow C) C}
  (h : CategoryTheory.Arrow.rightFunc ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.ker.ι C)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Arrow.leftToRight h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Algebra.Ring.Divisibility.Basic
/-- If an element `a` divides another element `b` in a ring, `a` divides the sum of `b` and another
element `c` iff `a` divides `c`.  -/
dvd_add_right : ∀ {α : Type u_1} [inst : NonUnitalRing α] {a b c : α}, a ∣ b → (a ∣ b + c ↔ a ∣ c)
-- Mathlib.Data.Holor
Holor.slice_zero : ∀ {α : Type} {d : ℕ} {ds : List ℕ} [inst : Zero α] (i : ℕ) (hid : i < d), Holor.slice 0 i hid = 0
-- Mathlib.Data.List.Sort
/-- The list `List.ofFn f` is strictly sorted with respect to `(· ≥ ·)` if and only if `f` is
strictly antitone.  -/
List.sortedGT_ofFn_iff : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ} {f : Fin n → α}, (List.ofFn f).SortedGT ↔ StrictAnti f
-- Mathlib.MeasureTheory.Function.LpSpace.Complete
MeasureTheory.Lp.cauchy_tendsto_of_tendsto : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {E : Type u_3}
  [inst : NormedAddCommGroup E] {f : ℕ → α → E},
  (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
    ∀ (f_lim : α → E) {B : ℕ → ENNReal},
      ∑' (i : ℕ), B i ≠ ⊤ →
        (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → MeasureTheory.eLpNorm (f n - f m_1) p μ < B N) →
          (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (f_lim x))) →
            Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - f_lim) p μ) Filter.atTop (nhds 0)
-- Init.Data.List.Attach
List.attachWith_map : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β} {P : β → Prop} (H : ∀ b ∈ List.map f l, P b),
  (List.map f l).attachWith P H =
    List.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, h⟩)
      (l.attachWith (P ∘ f) ⋯)
-- Mathlib.Topology.Bases
/-- If `f` has a dense range and its domain is countable, then its codomain is a separable space.
See also `DenseRange.separableSpace`.  -/
TopologicalSpace.SeparableSpace.of_denseRange : ∀ {α : Type u} [t : TopologicalSpace α] {ι : Type u_2} [Countable ι] (u : ι → α),
  DenseRange u → TopologicalSpace.SeparableSpace α
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivAt.isBigO_sub : ∀ {𝕜 : 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₀ → (fun x => f x - f x₀) =O[nhds x₀] fun x => x - x₀
-- Mathlib.Topology.UniformSpace.Closeds
UniformSpace.hausdorff.instDiscreteUniformitySet : ∀ {α : Type u_1} [inst : UniformSpace α] [DiscreteUniformity α], DiscreteUniformity (Set α)
-- Mathlib.Algebra.BigOperators.Group.List.Defs
List.sum_eq_card_nsmul : ∀ {M : Type u_2} [inst : AddMonoid M] (l : List M) (m : M), (∀ x ∈ l, x = m) → l.sum = l.length • m
-- Mathlib.Analysis.Seminorm
Seminorm.mem_ball : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p : Seminorm 𝕜 E) {x y : E} {r : ℝ}, y ∈ p.ball x r ↔ p (y - x) < r
-- Mathlib.MeasureTheory.Function.LpSeminorm.Count
MeasureTheory.enorm_le_eLpNorm_count : ∀ {α : Type u_1} {ε : Type u_2} [inst : MeasurableSpace α] [MeasurableSingletonClass α] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {p : ENNReal} (f : α → ε) (i : α),
  p ≠ 0 → ‖f i‖ₑ ≤ MeasureTheory.eLpNorm f p MeasureTheory.Measure.count
-- Mathlib.Data.Nat.Find
Nat.findGreatest_mono : ∀ {m : ℕ} {P Q : ℕ → Prop} [inst : DecidablePred P] {n : ℕ} [inst_1 : DecidablePred Q],
  (∀ (n : ℕ), P n → Q n) → m ≤ n → Nat.findGreatest P m ≤ Nat.findGreatest Q n
-- Mathlib.Data.Matrix.Basic
Matrix.transpose_sum : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} [inst : AddCommMonoid α] {ι : Type u_14} (s : Finset ι)
  (M : ι → Matrix m n α), (∑ i ∈ s, M i).transpose = ∑ i ∈ s, (M i).transpose
-- Std.Data.ExtDTreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or `fallback` if `n` is at least `t.size`.  -/
Std.ExtDTreeMap.Const.entryAtIdxD : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Std.TransCmp cmp] → Std.ExtDTreeMap α (fun x => β) cmp → ℕ → α × β → α × β
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.getSEvalSimprocs : Lean.CoreM Lean.Meta.Simprocs
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingHom.coe_rangeS : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S),
  ↑f.rangeS = Set.range ⇑f
-- Mathlib.Tactic.NormNum.Basic
/-- The `norm_num` extension which identifies the expression `One.one`, returning `1`.  -/
Mathlib.Meta.NormNum.evalOne : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.ofConjAct_inv : ∀ {G : Type u_3} [inst : DivInvMonoid G] (x : ConjAct G), ConjAct.ofConjAct x⁻¹ = (ConjAct.ofConjAct x)⁻¹
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
/-- The smallest balanced superset of `s`.  -/
balancedHull : (𝕜 : Type u_1) → {E : Type u_2} → [SeminormedRing 𝕜] → [SMul 𝕜 E] → Set E → Set E
-- Mathlib.Data.Prod.Lex
WCovBy.fst_ofLex : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a b : Lex (α × β)},
  a ⩿ b → (ofLex a).1 ⩿ (ofLex b).1
-- Init.Data.UInt.Lemmas
UInt8.toNat_neg : ∀ (a : UInt8), (-a).toNat = (UInt8.size - a.toNat) % UInt8.size
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- Continuous multilinear maps themselves form a normed group with respect to
the operator norm.  -/
ContinuousMultilinearMap.normedAddCommGroup : {𝕜 : Type u} →
  {ι : Type v} →
    {E : ι → Type wE} →
      {G : Type wG} →
        [Fintype ι] →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
              [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
                [inst_3 : NormedAddCommGroup G] →
                  [inst_4 : NormedSpace 𝕜 G] → NormedAddCommGroup (ContinuousMultilinearMap 𝕜 E G)
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
DerivedCategory.Plus.instIsLEObjιOfIsLE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (X : DerivedCategory.Plus C) (n : ℤ) [X.IsLE n], (DerivedCategory.Plus.ι.obj X).IsLE n
-- Mathlib.Topology.Algebra.GroupWithZero
Filter.Tendsto.zpow₀ : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [ContinuousInv₀ G₀]
  [ContinuousMul G₀] {f : α → G₀} {l : Filter α} {a : G₀},
  Filter.Tendsto f l (nhds a) → ∀ (m : ℤ), a ≠ 0 ∨ 0 ≤ m → Filter.Tendsto (fun x => f x ^ m) l (nhds (a ^ m))
-- Mathlib.NumberTheory.LucasLehmer
succ_mersenne : ∀ (k : ℕ), mersenne k + 1 = 2 ^ k
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.HoCat.exists_resolution : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] (X : C),
  ∃ X',
    ∃ (_ : HomotopicalAlgebra.IsCofibrant X'),
      ∃ p, HomotopicalAlgebra.Fibration p ∧ HomotopicalAlgebra.WeakEquivalence p
-- Mathlib.Algebra.Order.Interval.Basic
Interval.zero_mem_zero : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : Zero α], 0 ∈ 0
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
isLUB_neg' : ∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G} {a : G},
  IsLUB (-s) (-a) ↔ IsGLB s a
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- The root pairing homomorphism underlying an equivalence.  -/
RootPairing.Equiv.toHom : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {ι₂ : Type u_5} →
                    {M₂ : Type u_6} →
                      {N₂ : Type u_7} →
                        [inst_5 : AddCommGroup M₂] →
                          [inst_6 : Module R M₂] →
                            [inst_7 : AddCommGroup N₂] →
                              [inst_8 : Module R N₂] →
                                {P : RootPairing ι R M N} → {Q : RootPairing ι₂ R M₂ N₂} → P.Equiv Q → P.Hom Q
-- Std.Do.SPred.SPred
Std.Do.SPred.iff_cons : ∀ {σs : List (Type u)} {σ : Type u} {s : σ} {P Q : Std.Do.SPred (σ :: σs)}, spred(P ↔ Q) s = spred(P s ↔ Q s)
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.gramSchmidt_def'' : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] (f : ι → E)
  (n : ι),
  f n =
    InnerProductSpace.gramSchmidt 𝕜 f n +
      ∑ i < n,
        (inner 𝕜 (InnerProductSpace.gramSchmidt 𝕜 f i) (f n) / ↑‖InnerProductSpace.gramSchmidt 𝕜 f i‖ ^ 2) •
          InnerProductSpace.gramSchmidt 𝕜 f i
-- Mathlib.Order.Comparable
not_incompRel_iff : ∀ {α : Type u_1} {a b : α} {r : α → α → Prop}, ¬IncompRel r a b ↔ CompRel r a b
-- Mathlib.Combinatorics.SimpleGraph.UniversalVerts
SimpleGraph.deleteUniversalVerts_verts : ∀ {V : Type u_1} (G : SimpleGraph V), G.deleteUniversalVerts.verts = Set.univ \ G.universalVerts
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
/-- `FreeSimplexQuiver.σ i` represents `i`-th degeneracy map `.mk (n + 1) ⟶ .mk n`.  -/
FreeSimplexQuiver.σ : {n : ℕ} → Fin (n + 1) → (FreeSimplexQuiver.mk (n + 1) ⟶ FreeSimplexQuiver.mk n)
-- Mathlib.Data.Nat.Fib.Basic
Nat.fib_two_mul_add_two : ∀ (n : ℕ), Nat.fib (2 * n + 2) = Nat.fib (n + 1) * (2 * Nat.fib n + Nat.fib (n + 1))
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.instSymmModEq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {p : M}, Std.Symm (AddCommGroup.ModEq p)
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.continuousOn_toFun : ∀ {X : Type u_7} {Y : Type u_8} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (self : PartialHomeomorph X Y), ContinuousOn (↑self.toPartialEquiv) self.source
-- Std.Time.Format.Basic
Std.Time.instInhabitedFormatConfig : Inhabited Std.Time.FormatConfig
-- Mathlib.Data.ENat.Pow
ENat.epow_mul : ∀ {x y z : ℕ∞}, x ^ (y * z) = (x ^ y) ^ z
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
/-- The induced map of the right projection map X × Y → Y  -/
FundamentalGroupoidFunctor.projRight : (A : TopCat) →
  (B : TopCat) →
    CategoryTheory.Functor ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of (↑A × ↑B)))
      ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj B)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β}, (m.insert k v).contains a = (k == a || m.contains a)
-- Mathlib.Order.Minimal
/-- **Alias** of the reverse direction of `minimal_toDual`. -/
Minimal.dual : ∀ {α : Type u_2} {P : α → Prop} {x : α} [inst : LE α],
  Maximal P x → Minimal (fun x => P (OrderDual.ofDual x)) (OrderDual.toDual x)
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.AddContent.onIocAux_empty : ∀ {α : Type u_1} [inst : LinearOrder α] {G : Type u_3} [inst_1 : AddCommGroup G] (f : α → G),
  MeasureTheory.AddContent.onIocAux f ∅ = 0
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.norm_setToFun_le' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} {f : α → E} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (hf : MeasureTheory.Integrable f μ),
  ‖MeasureTheory.setToFun μ T hT f‖ ≤ max C 0 * ‖MeasureTheory.Integrable.toL1 f hf‖
-- Mathlib.Data.Set.Card
Set.ncard_lt_ncard_iff_ncard_sdiff_lt_ncard_sdiff : ∀ {α : Type u_1} {s t : Set α},
  autoParam s.Finite Set.ncard_lt_ncard_iff_ncard_sdiff_lt_ncard_sdiff._auto_1 →
    autoParam t.Finite Set.ncard_lt_ncard_iff_ncard_sdiff_lt_ncard_sdiff._auto_3 →
      (s.ncard < t.ncard ↔ (s \ t).ncard < (t \ s).ncard)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom_apply : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (e : X ≅ Y) (x : ↑X.toTopCat)
  (y :
    ↑(X.presheaf.stalk
        ((CategoryTheory.ConcreteCategory.hom e.inv.base) ((CategoryTheory.ConcreteCategory.hom e.hom.base) x)))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.hom x))
      ((CategoryTheory.ConcreteCategory.hom
          (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.inv
            ((CategoryTheory.ConcreteCategory.hom e.hom.base) x)))
        y) =
    (CategoryTheory.ConcreteCategory.hom (X.presheaf.stalkSpecializes ⋯)) y
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.instHasTensorTensorUnit_1 : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : DecidableEq I] [inst_4 : CategoryTheory.Limits.HasInitial C]
  [∀ (X₁ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)]
  (X : CategoryTheory.GradedObject I C), X.HasTensor CategoryTheory.GradedObject.Monoidal.tensorUnit