mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.Deriv
ContDiff.iterate_deriv : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (n : ℕ) {f : 𝕜 → F}, ContDiff 𝕜 (↑⊤) f → ContDiff 𝕜 (↑⊤) (deriv^[n] f)
-- Mathlib.Data.List.Cycle
/-- Given an element `x : α` of `l : List α` such that `x ∈ l`, get the previous
element of `l`. This works from head to tail, (including a check for last element)
so it will match on first hit, ignoring later duplicates.

* `prev [1, 2, 3] 2 _ = 1`
* `prev [1, 2, 3] 1 _ = 3`
* `prev [1, 2, 3, 2, 4] 2 _ = 1`
* `prev [1, 2, 3, 4, 2] 2 _ = 1`
* `prev [1, 1, 2] 1 _ = 2`
 -/
List.prev : {α : Type u_1} → [DecidableEq α] → (l : List α) → (x : α) → x ∈ l → α
-- Mathlib.Algebra.DirectSum.Module
DirectSum.lid_symm_apply : ∀ (R : Type u) [inst : Semiring R] {M : Type v} {ι : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Unique ι] (x : M), (DirectSum.lid R M ι).symm x = (DirectSum.lof R ι (fun i => M) default) x
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosSemidef.transpose : ∀ {n : Type u_2} {R' : Type u_4} [inst : CommRing R'] [inst_1 : PartialOrder R'] [inst_2 : StarRing R']
  {M : Matrix n n R'}, M.PosSemidef → M.transpose.PosSemidef
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
_private.Mathlib.GroupTheory.SpecificGroups.Dihedral.0.instDecidableEqDihedralGroup.decEq.match_1.eq_3 : ∀ {n : ℕ} (motive : DihedralGroup n → DihedralGroup n → Sort u_1) (a a_1 : ZMod n)
  (h_1 : (a b : ZMod n) → motive (DihedralGroup.r a) (DihedralGroup.r b))
  (h_2 : (a a_2 : ZMod n) → motive (DihedralGroup.r a) (DihedralGroup.sr a_2))
  (h_3 : (a a_2 : ZMod n) → motive (DihedralGroup.sr a) (DihedralGroup.r a_2))
  (h_4 : (a b : ZMod n) → motive (DihedralGroup.sr a) (DihedralGroup.sr b)),
  (match DihedralGroup.sr a, DihedralGroup.r a_1 with
    | DihedralGroup.r a, DihedralGroup.r b => h_1 a b
    | DihedralGroup.r a, DihedralGroup.sr a_2 => h_2 a a_2
    | DihedralGroup.sr a, DihedralGroup.r a_2 => h_3 a a_2
    | DihedralGroup.sr a, DihedralGroup.sr b => h_4 a b) =
    h_3 a a_1
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_congr_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α}, s ∩ u ⊆ t → s ∩ t ⊆ u → s ∩ t = s ∩ u
-- Lean.Data.JsonRpc
Lean.JsonRpc.instHashableRequestID.hash : Lean.JsonRpc.RequestID → UInt64
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.factorThruImage_comp_coimageIsoImage'_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f)
      (CategoryTheory.Abelian.coimageIsoImage' f).inv =
    CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.kernel.ι f)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
ContinuousLinearMap.domRestrict_comp_codRestrict : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {M₁ : Type u_4}
  {M₂ : Type u_5} {M₃ : Type u_6} [inst_4 : TopologicalSpace M₁] [inst_5 : AddCommMonoid M₁] [inst_6 : Module R₁ M₁]
  [inst_7 : TopologicalSpace M₂] [inst_8 : AddCommMonoid M₂] [inst_9 : Module R₂ M₂] [inst_10 : TopologicalSpace M₃]
  [inst_11 : AddCommMonoid M₃] [inst_12 : Module R₃ M₃] (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂)
  (h : ∀ (x : M₁), f x ∈ p), g.domRestrict p ∘SL f.codRestrict p h = g ∘SL f
-- Lean.Declaration
/-- Number of parameters  -/
Lean.RecursorVal.numParams : Lean.RecursorVal → ℕ
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- The unit of an adjunction  -/
CategoryTheory.Adjunction.CoreHomEquivUnitCounit.unit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            CategoryTheory.Adjunction.CoreHomEquivUnitCounit F G → (CategoryTheory.Functor.id C ⟶ F.comp G)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_counitIso_hom_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Mon C),
  (CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit.counitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.X
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.topObj_forget : ∀ {R : CommRingCat}, CategoryTheory.ToType (AlgebraicGeometry.Spec.topObj R) = PrimeSpectrum ↑R
-- Mathlib.Algebra.Algebra.Defs
Algebra.commute_algebraMap_left : ∀ {R : Type u} {A : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R) (x : A),
  Commute ((algebraMap R A) r) x
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.sub_mem_sub : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  [inst_4 : AddLeftMono α] (s t : NonemptyInterval α) {a b : α}, a ∈ s → b ∈ t → a - b ∈ s - t
-- Std.Internal.UV.System
Std.Internal.UV.System.RUsage.isRSS : Std.Internal.UV.System.RUsage → UInt64
-- Init.Data.SInt.Bitwise
Int64.xor_zero : ∀ {a : Int64}, a ^^^ 0 = a
-- Mathlib.RingTheory.Ideal.Maps
LinearEquiv.annihilator_eq : ∀ {R : Type u_1} {M : Type u_2} {M' : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (e : M ≃ₗ[R] M'), Module.annihilator R M = Module.annihilator R M'
-- Init.Data.SInt.Basic
instShiftLeftInt32 : ShiftLeft Int32
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.toShortNFOfCharThree_spec : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : CharP R 3],
  W.b₂ = 0 → (W.toShortNFOfCharThree • W).IsShortNF
-- Mathlib.GroupTheory.Perm.ClosureSwap
finite_compl_fixedBy_swap : ∀ {α : Type u_2} [inst : DecidableEq α] {x y : α}, (MulAction.fixedBy α (Equiv.swap x y))ᶜ.Finite
-- Mathlib.RingTheory.PowerSeries.PiTopology
/-- The product uniformity on `PowerSeries`  -/
PowerSeries.WithPiTopology.instUniformSpace : (R : Type u_1) → [UniformSpace R] → UniformSpace (PowerSeries R)
-- Mathlib.Order.SuccPred.Limit
Order.not_isSuccLimit_of_noMax : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] [NoMaxOrder α],
  ¬Order.IsSuccLimit a
-- Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
TopCat.Presheaf.IsSheaf.isSheafUniqueGluing : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.HasLimitsOfSize.{x, x, v_1, u_1} C] [(CategoryTheory.forget C).ReflectsIsomorphisms]
  [CategoryTheory.Limits.PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)] {X : TopCat}
  {F : TopCat.Presheaf C X},
  F.IsSheaf →
    ∀ {ι : Type u_4} (U : ι → TopologicalSpace.Opens ↑X)
      (sf : (i : ι) → CategoryTheory.ToType (F.obj (Opposite.op (U i)))), F.IsCompatible U sf → ∃! s, F.IsGluing U sf s
-- Mathlib.Algebra.Ring.Subring.Basic
/-- Subring closure of a set is monotone in its argument: if `s ⊆ t`,
then `closure s ≤ closure t`.  -/
Subring.closure_mono : ∀ {R : Type u} [inst : NonAssocRing R] ⦃s t : Set R⦄, s ⊆ t → Subring.closure s ≤ Subring.closure t
-- Mathlib.Analysis.Asymptotics.Theta
/-- **Alias** of the forward direction of `Asymptotics.isTheta_norm_left`. -/
Asymptotics.IsTheta.of_norm_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {f' : α → E'} {l : Filter α}, (fun x => ‖f' x‖) =Θ[l] g → f' =Θ[l] g
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Set.multiset_prod_singleton : ∀ {M : Type u_5} [inst : CommMonoid M] (s : Multiset M), (Multiset.map (fun i => {i}) s).prod = {s.prod}
-- Init.Data.List.Nat.Sublist
List.append_sublist_of_sublist_left : ∀ {α : Type u_1} {xs ys zs : List α}, zs.Sublist xs → ((xs ++ ys).Sublist zs ↔ ys = [] ∧ xs = zs)
-- Mathlib.SetTheory.ZFC.Class
/-- The union of a class is the class of all members of ZFC sets in the class. Uses `⋃₀` notation,
scoped under the `Class` namespace.  -/
Class.«term⋃₀_» : Lean.ParserDescr
-- Mathlib.Order.WithBot
WithBot.coe_inf : ∀ {α : Type u_1} [inst : SemilatticeInf α] (a b : α), ↑(a ⊓ b) = ↑a ⊓ ↑b
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- `colimitFlipIsoCompColim` is natural with respect to diagrams.  -/
CategoryTheory.Limits.colimCompFlipIsoWhiskerColim : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} J] →
        {K : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} K] →
            [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C] →
              (CategoryTheory.flipFunctor K J C).comp CategoryTheory.Limits.colim ≅
                (CategoryTheory.Functor.whiskeringRight K (CategoryTheory.Functor J C) C).obj
                  CategoryTheory.Limits.colim
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.tr.eq_2 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ)
  (k : K) (s : Turing.TM2to1.StAct K Γ σ k) (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2to1.tr M (Turing.TM2to1.Λ'.go k s q) =
    Turing.TM1.Stmt.branch (fun a x => (a.2 k).isNone)
      (Turing.TM2to1.trStAct (Turing.TM1.Stmt.goto fun x x_1 => Turing.TM2to1.Λ'.ret q) s)
      (Turing.TM1.Stmt.move Turing.Dir.right (Turing.TM1.Stmt.goto fun x x_1 => Turing.TM2to1.Λ'.go k s q))
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Expr.denoteN.eq_6 : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] (ctx : Lean.Grind.Linarith.Context α) (a b : Lean.Grind.Linarith.Expr),
  Lean.Grind.Linarith.Expr.denoteN ctx (a.add b) =
    Lean.Grind.Linarith.Expr.denoteN ctx a + Lean.Grind.Linarith.Expr.denoteN ctx b
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda'_inv_comp_π_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (F : CategoryTheory.Functor Iᵒᵖ C) [inst_2 : CategoryTheory.Limits.HasColimit F] (i : I)
  {Z : CategoryTheory.Functor C (Type u₂)} (h : CategoryTheory.coyoneda.obj (Opposite.op (F.obj (Opposite.op i))) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda' F).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.rightOp.comp CategoryTheory.coyoneda) i) h
-- Mathlib.Geometry.Manifold.Notation
/-- Given `V : Expr` representing `E : B → Type*`, try to find a model fiber for `E`
by searching in local context for either a `FiberBundle F E` or
`TopologicalSpace (TotalSpace F E)` instance.

We could try a more systematic search of `TotalSpace F E` anywhere in the local context,
but the current heuristic is faster and sufficient so far.  -/
_private.Mathlib.Geometry.Manifold.Notation.0.Manifold.Elab.findModelFiber? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.continuousAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {x : H},
  ContinuousAt (↑I) x
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLT_map_app_eTruncLTι_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {i j : EInt} (f : i ⟶ j) (X : C),
  CategoryTheory.CategoryStruct.comp ((t.eTruncLT.map f).app X) ((t.eTruncLTι j).app X) = (t.eTruncLTι i).app X
-- Mathlib.Topology.Category.TopCat.Yoneda
ContinuousMap.yonedaPresheaf'_map : ∀ (Y : Type w') [inst : TopologicalSpace Y] {X Y_1 : TopCatᵒᵖ} (f : X ⟶ Y_1),
  (ContinuousMap.yonedaPresheaf' Y).map f = TypeCat.ofHom fun g => g.comp (CategoryTheory.ConcreteCategory.hom f.unop)
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.ofHom_hom : ∀ {X Y : TopCat} (f : X ⟶ Y), TopCat.ofHom (TopCat.Hom.hom f) = f
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.comp_symmCompOfNondegenerate_apply : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : FiniteDimensional K V] (B₁ : LinearMap.BilinForm K V) {B₂ : LinearMap.BilinForm K V} (b₂ : B₂.Nondegenerate)
  (v : V), B₂ ((B₁.symmCompOfNondegenerate B₂ b₂) v) = B₁ v
-- Mathlib.Analysis.Complex.HasPrimitives
Complex.wedgeIntegral.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (z w : ℂ) (f : ℂ → E),
  z.wedgeIntegral w f =
    (∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) +
      Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)
-- Init.Notation
/-- Category for carrying raw syntax trees between macros; any content is printed as is by the pretty printer.
The only accepted parser for this category is an antiquotation.
 -/
Lean.Parser.Category.rawStx : Lean.Parser.Category
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.π_reflexiveCoequalizerIsoCoequalizer_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C)
  [inst_1 :
    CategoryTheory.Limits.HasCoequalizer (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
      (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.coequalizer.π (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
        (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right))
      (CategoryTheory.Limits.reflexiveCoequalizerIsoCoequalizer F).inv =
    CategoryTheory.Limits.colimit.ι F CategoryTheory.Limits.WalkingReflexivePair.zero
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_of_contains_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k a : α},
  (t.erase k).contains a = true → t.contains a = true
-- Mathlib.Data.List.Rotate
List.rotate_one_eq_self_iff_eq_replicate : ∀ {α : Type u} [Nonempty α] {l : List α}, l.rotate 1 = l ↔ ∃ a, l = List.replicate l.length a
-- Mathlib.Topology.Constructions.SumProd
/-- A product set is open in a product space if and only if each factor is open, or one of them is
empty  -/
isOpen_prod_iff' : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {t : Set Y},
  IsOpen (s ×ˢ t) ↔ IsOpen s ∧ IsOpen t ∨ s = ∅ ∨ t = ∅
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.findSome?_eq_findSome?_toIterM : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.IteratorLoop α Id Id] [Std.Iterators.Finite α Id]
  {it : Std.Iter β} {f : β → Option γ}, it.findSome? f = (it.toIterM.findSome? f).run
-- Mathlib.Algebra.Group.AddChar
AddChar.mul_apply : ∀ {A : Type u_2} {M : Type u_3} [inst : AddMonoid A] [inst_1 : CommMonoid M] (ψ φ : AddChar A M) (a : A),
  (ψ * φ) a = ψ a * φ a
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.instIsAddApplyReal : ∀ {E : Type u_3} [inst : AddGroup E], IsAddApply (AddGroupSeminorm E) E ℝ
-- Mathlib.Topology.Algebra.Group.Pointwise
subset_interior_sub_right : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {s t : Set G},
  s - interior t ⊆ interior (s - t)
-- Mathlib.Order.Defs.Unbundled
IsPartialOrder.toAntisymm : ∀ {α : Sort u_1} {r : α → α → Prop} [self : IsPartialOrder α r], Std.Antisymm r
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.tendsto_arg_nhdsWithin_im_nonneg_of_re_neg_of_im_zero : ∀ {z : ℂ}, z.re < 0 → z.im = 0 → Filter.Tendsto Complex.arg (nhdsWithin z {z | 0 ≤ z.im}) (nhds Real.pi)
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netMaxcard_infinite_iff : ∀ {X : Type u_1} (T : X → X) (F : Set X) (U : SetRel X X) (n : ℕ),
  Dynamics.netMaxcard T F U n = ⊤ ↔ ∀ (k : ℕ), ∃ s, Dynamics.IsDynNetIn T F U n ↑s ∧ k ≤ s.card
-- Mathlib.Topology.Algebra.Group.Pointwise
singleton_mul_mem_nhds_of_nhds_one : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Group α] [ContinuousConstSMul α α] {s : Set α} (a : α),
  s ∈ nhds 1 → {a} * s ∈ nhds a
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.instIsFibrantP : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A)
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct A A] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_4 : CategoryTheory.Limits.HasTerminal C] [(HomotopicalAlgebra.fibrations C).IsStableUnderComposition]
  [(HomotopicalAlgebra.fibrations C).IsStableUnderBaseChange] [HomotopicalAlgebra.IsFibrant A] [P.IsGood],
  HomotopicalAlgebra.IsFibrant P.P
-- Init.Data.UInt.Lemmas
USize.add_zero : ∀ (a : USize), a + 0 = a
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.curry_smul_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_4} {Z : Type u_5} [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {R : Type u_6} [inst_3 : SMul R Z] [inst_4 : ContinuousConstSMul R Z] (f : C(X × Y, Z))
  (r : R) (x : X), (r • f).curry x = r • f.curry x
-- Mathlib.RingTheory.Regular.RegularSequence
_private.Mathlib.RingTheory.Regular.RegularSequence.0.RingTheory.Sequence.IsWeaklyRegular.prototype_perm.aux : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {rs : List R},
  (∀ (a b : R) (rs' : List R),
      (a :: b :: rs').Subperm rs →
        have K := Submodule.torsionBy R (M ⧸ Ideal.ofList rs' • ⊤) b;
        K = a • K → K = ⊥) →
    ∀ {rs₁ rs₂ : List R} (rs₀ : List R),
      rs₁.Perm rs₂ →
        (rs₀ ++ rs₁).Subperm rs →
          (rs₀ ++ rs₂).Subperm rs →
            RingTheory.Sequence.IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) rs₁ →
              RingTheory.Sequence.IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) rs₂
-- Init.Data.SInt.Lemmas
Int32.ofIntTruncate_int16ToInt : ∀ (x : Int16), Int32.ofIntClamp x.toInt = x.toInt32
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.toSnowflaking.sizeOf_spec : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : SizeOf X] (x : X),
  sizeOf (Metric.Snowflaking.toSnowflaking x) = 1 + sizeOf x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {a fallback : α}, m.contains a = false → m.getKeyD a fallback = fallback
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_val : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  ⇑S.val = Subtype.val
-- Init.Core
ForIn.mk : {m : Type u₁ → Type u₂} →
  {ρ : Type u} → {α : outParam (Type v)} → ({β : Type u₁} → ρ → β → (α → β → m (ForInStep β)) → m β) → ForIn m ρ α
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.sum_restrict : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsFundamentalDomain G s μ → (MeasureTheory.Measure.sum fun g => μ.restrict (g • s)) = μ
-- Mathlib.CategoryTheory.Limits.Cones
/-- The construction `mapCocone` respects functor composition.  -/
CategoryTheory.Functor.mapCoconeMapCocone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            {E : Type u₅} →
              [inst_3 : CategoryTheory.Category.{v₅, u₅} E] →
                {F : CategoryTheory.Functor J C} →
                  {H : CategoryTheory.Functor C D} →
                    {H' : CategoryTheory.Functor D E} →
                      (c : CategoryTheory.Limits.Cocone F) → H'.mapCocone (H.mapCocone c) ≅ (H.comp H').mapCocone c
-- Mathlib.Topology.MetricSpace.Lipschitz
/-- **Alias** of the forward direction of `lipschitzOnWith_iff_dist_le_mul`. -/
LipschitzOnWith.dist_le_mul : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {s : Set α}
  {f : α → β}, LipschitzOnWith K f s → ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑K * dist x y
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
FiberBundle.trivializationAt_continuousAlternatingMap_target : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : Fintype ι] {B : Type u_3}
  [inst_2 : TopologicalSpace B] {F₁ : Type u_4} [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  {E₁ : B → Type u_5} [inst_5 : (x : B) → AddCommGroup (E₁ x)] [inst_6 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_7 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_8 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_9 : FiberBundle F₁ E₁] [inst_10 : VectorBundle 𝕜 F₁ E₁] {F₂ : Type u_6} [inst_11 : NormedAddCommGroup F₂]
  [inst_12 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_7} [inst_13 : (x : B) → AddCommGroup (E₂ x)]
  [inst_14 : (x : B) → Module 𝕜 (E₂ x)] [inst_15 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_16 : (x : B) → TopologicalSpace (E₂ x)] [inst_17 : FiberBundle F₂ E₂] [inst_18 : VectorBundle 𝕜 F₂ E₂]
  [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] [inst_20 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] (x₀ : B),
  (trivializationAt (F₁ [⋀^ι]→L[𝕜] F₂) (fun x => E₁ x [⋀^ι]→L[𝕜] E₂ x) x₀).target =
    ((trivializationAt F₁ E₁ x₀).baseSet ∩ (trivializationAt F₂ E₂ x₀).baseSet) ×ˢ Set.univ
-- Batteries.Data.Array.Scan
Array.scanrM_map : ∀ {m : Type u_1 → Type u_2} {α₁ : Type u_3} {α₂ : Type u_4} {β : Type u_1} {init : β} [inst : Monad m] [LawfulMonad m]
  {f : α₁ → α₂} {g : α₂ → β → m β} {as : Array α₁},
  Array.scanrM g init (Array.map f as) = Array.scanrM (fun a b => g (f a) b) init as
-- Lean.Expr
Lean.Expr.updateProj! : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.zpow_add : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  {A : Matrix n' n' R}, IsUnit A.det → ∀ (m n : ℤ), A ^ (m + n) = A ^ m * A ^ n
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Composing with a family of surjective linear maps is injective.  -/
MultilinearMap.compLinearMap_injective : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₁' : ι → Type v₁'} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → AddCommMonoid (M₁' i)] [inst_6 : (i : ι) → Module R (M₁' i)]
  (f : (i : ι) → M₁ i →ₗ[R] M₁' i),
  (∀ (i : ι), Function.Surjective ⇑(f i)) → Function.Injective fun g => g.compLinearMap f
-- Init.Grind.AC
Lean.Grind.AC.Seq.contains_k : Lean.Grind.AC.Seq → Lean.Grind.AC.Var → Bool
-- Mathlib.Order.CompleteLattice.Finset
Finset.set_biInter_inter : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] (s t : Finset α) (u : α → Set β),
  ⋂ x ∈ s ∪ t, u x = (⋂ x ∈ s, u x) ∩ ⋂ x ∈ t, u x
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.isClosed_iff : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace X],
  Topology.IsInducing f → ∀ {s : Set X}, IsClosed s ↔ ∃ t, IsClosed t ∧ f ⁻¹' t = s