mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Combinators.Monadic.Attach
Std.Iterators.Types.Attach.instFinitenessRelation : {α β : Type w} →
  {m : Type w → Type w'} →
    [inst : Monad m] →
      [inst_1 : Std.Iterator α m β] →
        [Std.Iterators.Finite α m] →
          {P : β → Prop} → Std.Iterators.FinitenessRelation (Std.Iterators.Types.Attach α m P) m
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The first part of the third simplicial identity  -/
SimplexCategory.δ_comp_σ_self : ∀ {n : ℕ} {i : Fin (n + 1)},
  CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i.castSucc) (SimplexCategory.σ i) =
    CategoryTheory.CategoryStruct.id { len := n }
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_zero : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α], (Matrix.diagonal fun x => 0) = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.eqToIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f f' : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasImage f] [inst_2 : CategoryTheory.Limits.HasImage f'] (h : f = f'),
  CategoryTheory.Limits.image.eqToIso h = CategoryTheory.asIso (CategoryTheory.Limits.image.eqToHom h)
-- Mathlib.Algebra.Ring.Defs
/-- A `NonAssocRing` which `IsMulCommutative` is a `NonAssocCommRing`.

This is primarily used to deduce the bundled version from the unbundled one for commutative
subobjects in a noncommutative ambient type. As such this is only available inside the
`IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
commutativity.

See note [commutative subobjects].  -/
IsMulCommutative.instNonAssocCommRing : {R : Type v} → [inst : NonAssocRing R] → [IsMulCommutative R] → NonAssocCommRing R
-- Mathlib.CategoryTheory.Groupoid
/-- `f` composed with `inv f` is the identity  -/
CategoryTheory.Groupoid.comp_inv : ∀ {obj : Type u} [self : CategoryTheory.Groupoid obj] {X Y : obj} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.Groupoid.inv f) = CategoryTheory.CategoryStruct.id X
-- Init.Data.String.Lemmas.Order
String.Pos.ofSliceFrom_next : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {h : p ≠ (s.sliceFrom p₀).endPos},
  String.Pos.ofSliceFrom (p.next h) = (String.Pos.ofSliceFrom p).next ⋯
-- Mathlib.NumberTheory.EulerProduct.Basic
/-- Given a (completely) multiplicative function `f : ℕ → F`, where `F` is a normed field,
such that `‖f p‖ < 1` for all primes `p`, we can express the sum of `f n` over all `N`-smooth
positive integers `n` as a product of `(1 - f p)⁻¹` over the primes `p < N`. At the same time,
we show that the sum involved converges absolutely.  -/
EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_geometric : ∀ {F : Type u_1} [inst : NormedField F] [CompleteSpace F] {f : ℕ →* F},
  (∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1) →
    ∀ (N : ℕ), (Summable fun m => ‖f ↑m‖) ∧ HasSum (fun m => f ↑m) (∏ p ∈ N.primesBelow, (1 - f p)⁻¹)
-- Mathlib.Data.Vector3
Vector3.cons_fs : ∀ {α : Type u_1} {n : ℕ} (a : α) (v : Vector3 α n) (i : Fin2 n), Vector3.cons a v i.fs = v i
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
ZMod.χ₈'_nat_eq_if_mod_eight : ∀ (n : ℕ), ZMod.χ₈' ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1
-- Mathlib.Order.Hom.Bounded
/-- Composition of `BoundedOrderHom`s as a `BoundedOrderHom`.  -/
BoundedOrderHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : Preorder α] →
        [inst_1 : Preorder β] →
          [inst_2 : Preorder γ] →
            [inst_3 : BoundedOrder α] →
              [inst_4 : BoundedOrder β] →
                [inst_5 : BoundedOrder γ] → BoundedOrderHom β γ → BoundedOrderHom α β → BoundedOrderHom α γ
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- Any inner horn contains the spine of the unique non-degenerate `n`-simplex
in `Δ[n]`.  -/
SSet.horn.spineId : {n : ℕ} → (i : Fin (n + 3)) → 0 < i → i < Fin.last (n + 2) → (SSet.horn (n + 2) i).toSSet.Path (n + 2)
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.skipPrefixWhile_string_eq_skipPrefixWhile_toSlice : ∀ {pat : String} {s : String.Slice}, s.skipPrefixWhile pat = s.skipPrefixWhile pat.toSlice
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- When the first map `S.f` is zero, this is the homology data on `S` given
by any limit kernel fork of `S.g`  -/
CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        S.f = 0 → (c : CategoryTheory.Limits.KernelFork S.g) → CategoryTheory.Limits.IsLimit c → S.HomologyData
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.le_sum_nonempty_of_subadditive : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] [inst_2 : Preorder β]
  [IsOrderedAddMonoid β] (f : α → β),
  (∀ (a b : α), f (a + b) ≤ f a + f b) → ∀ (s : Multiset α), s ≠ ∅ → f s.sum ≤ (Multiset.map f s).sum
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Any localization of a cancellative commutative monoid is cancellative.  -/
Submonoid.LocalizationMap.cancelCommMonoid : {M : Type u_3} →
  {N : Type u_4} →
    [inst : CancelCommMonoid M] → {S : Submonoid M} → [inst_1 : CommMonoid N] → S.LocalizationMap N → CancelCommMonoid N
-- Mathlib.Algebra.Group.Hom.Defs
map_comp_add : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : Add M] [inst_1 : Add N] [inst_2 : FunLike F M N]
  [AddHomClass F M N] (f : F) (g h : ι → M), ⇑f ∘ (g + h) = ⇑f ∘ g + ⇑f ∘ h
-- Mathlib.Order.WellFoundedSet
Set.partiallyWellOrderedOn_empty : ∀ {α : Type u_2} (r : α → α → Prop), ∅.PartiallyWellOrderedOn r
-- Mathlib.Analysis.Asymptotics.Defs
/-- See also `Filter.Eventually.isBigO`, which is the same lemma
stated using `Filter.Eventually` instead of `Filter.EventuallyLE`.  -/
Asymptotics.IsBigO.of_norm_eventuallyLE : ∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {f : α → E} {l : Filter α} {g : α → ℝ},
  (fun x => ‖f x‖) ≤ᶠ[l] g → f =O[l] g
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.meas_biInter : ∀ {Ω : Type u_1} {ι : Type u_2} {κ : ι → Type u_5} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {S : Finset ι}
  {s : ι → Set Ω} {m : (i : ι) → MeasurableSpace (κ i)} {f : (x : ι) → Ω → κ x},
  ProbabilityTheory.iIndepFun f μ → (∀ i ∈ S, MeasurableSet (s i)) → μ (⋂ i ∈ S, s i) = ∏ i ∈ S, μ (s i)
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The tensor unity in the monoidal structure `𝟙_ C`  -/
CategoryTheory.MonoidalCategoryStruct.tensorUnit : (C : Type u) → {𝒞 : CategoryTheory.Category.{v, u} C} → [self : CategoryTheory.MonoidalCategoryStruct C] → C
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimApp.instInhabitedAlt : Inhabited Lean.Elab.Tactic.ElimApp.Alt
-- Aesop.RuleTac.Basic
Aesop.Subgoal.mvarId : Aesop.Subgoal → Lean.MVarId
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.mem_support_of_mem_edges : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {e : Sym2 V} {p : G.Walk u v}, e ∈ p.edges → w ∈ e → w ∈ p.support
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.boxProdComm_apply : ∀ {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) (H : SimpleGraph β) (a : α × β), (G.boxProdComm H) a = a.swap
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.WalkingCospan.instSubsingletonHom : ∀ (X Y : CategoryTheory.Limits.WalkingCospan), Subsingleton (X ⟶ Y)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.ext'_iff : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] {e e' : Bundle.Trivialization F proj},
  e = e' ↔ e.toOpenPartialHomeomorph = e'.toOpenPartialHomeomorph ∧ e.baseSet = e'.baseSet
-- Mathlib.Dynamics.BirkhoffSum.Average
birkhoffAverage_one : ∀ (R : Type u_1) {α : Type u_2} {M : Type u_3} [inst : DivisionSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (f : α → α) (g : α → M) (x : α), birkhoffAverage R f g 1 x = g x
-- Std.Data.DTreeMap.Internal.Operations
/-- The tree has size `size`.  -/
Std.DTreeMap.Internal.Impl.Tree.size_impl : ∀ {α : Type u} {β : α → Type v} {size : ℕ} (self : Std.DTreeMap.Internal.Impl.Tree α β size), self.impl.size = size
-- Mathlib.Data.Int.Init
Int.gcd_negSucc_ofNat : ∀ (m n : ℕ), (Int.negSucc m).gcd ↑n = (m + 1).gcd n
-- Mathlib.Topology.Algebra.StarSubalgebra
/-- If a star subalgebra of a topological star algebra is commutative, then so is its topological
closure. See note [reducible non-instances].  -/
StarSubalgebra.commSemiringTopologicalClosure : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : TopologicalSpace A] →
          [inst_3 : Semiring A] →
            [inst_4 : Algebra R A] →
              [inst_5 : StarRing A] →
                [inst_6 : StarModule R A] →
                  [inst_7 : IsSemitopologicalSemiring A] →
                    [inst_8 : ContinuousStar A] →
                      [T2Space A] →
                        (s : StarSubalgebra R A) → (∀ (x y : ↥s), x * y = y * x) → CommSemiring ↥s.topologicalClosure
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
UniqueDiffWithinAt.smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {x : E},
  UniqueDiffWithinAt 𝕜 s x →
    ∀ {G : Type u_4} [inst_3 : GroupWithZero G] [inst_4 : DistribMulAction G E] [ContinuousConstSMul G E]
      [SMulCommClass G 𝕜 E] {c : G}, c ≠ 0 → UniqueDiffWithinAt 𝕜 (c • s) (c • x)
-- Mathlib.Data.Finset.Filter
Finset.disjoint_filter_and_not_filter : ∀ {α : Type u_1} (p q : α → Prop) [inst : DecidablePred p] [inst_1 : DecidablePred q] {s : Finset α},
  Disjoint ({x ∈ s | p x ∧ ¬q x}) ({x ∈ s | q x ∧ ¬p x})
-- Lean.Meta.Basic
/-- Removes `fvarId` from the local context, and replaces occurrences of it with `e`.
It is the responsibility of the caller to ensure that `e` is well-typed in the context
of any occurrence of `fvarId`.
 -/
Lean.Meta.withReplaceFVarId : {α : Type} → Lean.FVarId → Lean.Expr → Lean.MetaM α → Lean.MetaM α
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.comp_mul_right : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {a b : ℝ}
  [TopologicalSpace.PseudoMetrizableSpace ε],
  IntervalIntegrable f MeasureTheory.volume a b →
    ∀ {c : ℝ},
      autoParam (‖f (min a b)‖ₑ ≠ ⊤) IntervalIntegrable.comp_mul_right._auto_1 →
        autoParam (‖f (c * min (a / c) (b / c))‖ₑ ≠ ⊤) IntervalIntegrable.comp_mul_right._auto_3 →
          IntervalIntegrable (fun x => f (x * c)) MeasureTheory.volume (a / c) (b / c)
-- Init.Data.Nat.Gcd
Nat.gcd_one_left : ∀ (n : ℕ), Nat.gcd 1 n = 1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k k' : α},
      (k == k') = true →
        ∀ {v fallback : β},
          List.Pairwise (fun a b => (a.1 == b.1) = false) l → (k, v) ∈ l → (m.insertMany l).getD k' fallback = v
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.instInhabited : {p : ℕ} → [hp : Fact (Nat.Prime p)] → Inhabited ℤ_[p]
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Bundle.ContMDiffRiemannianMetric.mk.injEq : ∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3}
  [inst_3 : TopologicalSpace B] [inst_4 : ChartedSpace HB B] {F : Type u_4} [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℝ F] {E : B → Type u_5} [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_8 : (b : B) → TopologicalSpace (E b)] [inst_9 : (b : B) → AddCommGroup (E b)]
  [inst_10 : (b : B) → Module ℝ (E b)] [inst_11 : FiberBundle F E] [inst_12 : VectorBundle ℝ F E]
  (inner : (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ) (symm : ∀ (b : B) (v w : E b), ((inner b) v) w = ((inner b) w) v)
  (pos : ∀ (b : B) (v : E b), v ≠ 0 → 0 < ((inner b) v) v)
  (isVonNBounded : ∀ (b : B), Bornology.IsVonNBounded ℝ {v | ((inner b) v) v < 1})
  (contMDiff : ContMDiff IB (IB.prod (modelWithCornersSelf ℝ (F →L[ℝ] F →L[ℝ] ℝ))) n fun b => ⟨b, inner b⟩)
  (inner_1 : (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ) (symm_1 : ∀ (b : B) (v w : E b), ((inner_1 b) v) w = ((inner_1 b) w) v)
  (pos_1 : ∀ (b : B) (v : E b), v ≠ 0 → 0 < ((inner_1 b) v) v)
  (isVonNBounded_1 : ∀ (b : B), Bornology.IsVonNBounded ℝ {v | ((inner_1 b) v) v < 1})
  (contMDiff_1 : ContMDiff IB (IB.prod (modelWithCornersSelf ℝ (F →L[ℝ] F →L[ℝ] ℝ))) n fun b => ⟨b, inner_1 b⟩),
  ({ inner := inner, symm := symm, pos := pos, isVonNBounded := isVonNBounded, contMDiff := contMDiff } =
      { inner := inner_1, symm := symm_1, pos := pos_1, isVonNBounded := isVonNBounded_1, contMDiff := contMDiff_1 }) =
    (inner = inner_1)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- A family of submodules indexed by `FiniteArchimedeanClass M` that
are complements between `FiniteArchimedeanClass.ball` and `FiniteArchimedeanClass.closedBall`.  -/
HahnEmbedding.ArchimedeanStrata : (K : Type u_1) →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [IsOrderedRing K] →
        [Archimedean K] →
          (M : Type u_2) →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [IsOrderedAddMonoid M] → [inst_7 : Module K M] → [IsOrderedModule K M] → Type u_2
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- Left identity of the `L^p` product as a linear isometric equivalence.  -/
LinearIsometryEquiv.withLpUniqueProd : (p : ENNReal) →
  (𝕜 : Type u_1) →
    (α : Type u_2) →
      (β : Type u_3) →
        [hp : Fact (1 ≤ p)] →
          [inst : Semiring 𝕜] →
            [inst_1 : SeminormedAddCommGroup α] →
              [inst_2 : Module 𝕜 α] →
                [inst_3 : SeminormedAddCommGroup β] → [inst_4 : Module 𝕜 β] → [Unique α] → WithLp p (α × β) ≃ₗᵢ[𝕜] β
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiff_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type uF} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}, ContDiff 𝕜 n fun p => p.1 + p.2
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_eq_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s ∪ t = t ↔ s ⊆ t
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingAfter_apply_anti : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] (u : ι → Ω → β) (n : ι)
  (ω : Ω), Antitone fun x => MeasureTheory.hittingAfter u x n ω
-- Lean.DocString.Types
Lean.Doc.instOrdListItem : {α : Type u_1} → [Ord α] → Ord (Lean.Doc.ListItem α)
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.IsThreeCycle.orderOf : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {g : Equiv.Perm α}, g.IsThreeCycle → orderOf g = 3
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.epi_homMk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A B : CategoryTheory.CostructuredArrow S T} (f : A.left ⟶ B.left)
  (w : CategoryTheory.CategoryStruct.comp (S.map f) B.hom = A.hom) [h : CategoryTheory.Epi f],
  CategoryTheory.Epi (CategoryTheory.CostructuredArrow.homMk f w)
-- Mathlib.Topology.Order.LawsonTopology
Topology.IsLawson.lawsonBasis.eq_1 : ∀ (α : Type u_1) [inst : Preorder α],
  Topology.IsLawson.lawsonBasis α = {s | ∃ t, t.Finite ∧ ∃ u, IsOpen u ∧ u \ ↑(upperClosure t) = s}
-- Mathlib.ModelTheory.Syntax
/-- Maps bounded formulas along a map of terms and a map of relations.  -/
FirstOrder.Language.BoundedFormula.mapTermRel : {L : FirstOrder.Language} →
  {L' : FirstOrder.Language} →
    {α : Type u'} →
      {β : Type v'} →
        {g : ℕ → ℕ} →
          ((n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin (g n))) →
            ((n : ℕ) → L.Relations n → L'.Relations n) →
              ((n : ℕ) → L'.BoundedFormula β (g (n + 1)) → L'.BoundedFormula β (g n + 1)) →
                {n : ℕ} → L.BoundedFormula α n → L'.BoundedFormula β (g n)
-- Mathlib.Geometry.Convex.Star
Convexity.IsStarConvexSet.singleton : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {x : X}, Convexity.IsStarConvexSet R x {x}
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_union! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → (m₁.union! m₂).isEmpty = (m₁.isEmpty && m₂.isEmpty)
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.IsStackFor.isPrestackFor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {S : C}
  {R : CategoryTheory.Presieve S}, F.IsStackFor R → F.IsPrestackFor R
-- Mathlib.Data.Stream.Init
Stream'.drop_append_of_le_length : ∀ {α : Type u} (n : ℕ) (x : List α) (a : Stream' α), n ≤ x.length → Stream'.drop n (x ++ₛ a) = List.drop n x ++ₛ a
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insertIfNew k v).minKey? = some (t.minKey?.elim k fun k' => if cmp k k' = Ordering.lt then k else k')
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
CategoryTheory.isCardinalFiltered_iff_aux₁ : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {κ : Cardinal.{w}},
  (∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ k, ∀ (i : ι), Nonempty (j i ⟶ k)) →
    (∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
        HasCardinalLT ι κ → ∃ l a b, ∀ (i : ι), CategoryTheory.CategoryStruct.comp (f i) a = b) →
      ∀ {ι : Type w} {j : J} {k : ι → J} (f : (i : ι) → j ⟶ k i),
        HasCardinalLT ι κ → ∃ m a b, ∀ (i : ι), CategoryTheory.CategoryStruct.comp (f i) (a i) = b
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.map_mono : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] {S₁ S₂ : NonUnitalSubalgebra R A} {f : F},
  S₁ ≤ S₂ → NonUnitalSubalgebra.map f S₁ ≤ NonUnitalSubalgebra.map f S₂
-- Mathlib.Data.List.Permutation
List.getElem_permutations'Aux : ∀ {α : Type u_1} (s : List α) (x : α) (n : ℕ) (hn : n < (List.permutations'Aux x s).length),
  (List.permutations'Aux x s)[n] = s.insertIdx n x
-- Mathlib.Geometry.Manifold.Riemannian.PathELength
/-- The Riemannian edistance is bounded above by the length of any `C^1` path from `x` to `y`.
Here, we express this using a path defined on the whole real line, considered on
some interval `[a, b]`.  -/
Manifold.riemannianEDist_le_pathELength : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : (x : M) → ENorm (TangentSpace I x)] [∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)] {x y : M} {a b : ℝ}
  {γ : ℝ → M},
  ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ (Set.Icc a b) →
    γ a = x → γ b = y → a ≤ b → Manifold.riemannianEDist I x y ≤ Manifold.pathELength I γ a b
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.Decomposition.decompose' : {ι : Type u_1} →
  {M : Type u_3} →
    {σ : Type u_4} →
      {inst : DecidableEq ι} →
        {inst_1 : AddCommMonoid M} →
          {inst_2 : SetLike σ M} →
            {inst_3 : AddSubmonoidClass σ M} →
              {ℳ : ι → σ} → [self : DirectSum.Decomposition ℳ] → M → DirectSum ι fun i => ↥(ℳ i)
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- If `b` is odd, then `J(-1 | b)` is given by `χ₄ b`.  -/
jacobiSym.at_neg_one : ∀ {b : ℕ}, Odd b → jacobiSym (-1) b = ZMod.χ₄ ↑b
-- Mathlib.RingTheory.WittVector.WittPolynomial
/-- The `xInTermsOfW p R n` is the polynomial on the basis of Witt polynomials
that corresponds to the ordinary `X n`.  -/
xInTermsOfW : (p : ℕ) → (R : Type u_1) → [inst : CommRing R] → [Invertible ↑p] → ℕ → MvPolynomial ℕ R
-- Mathlib.Topology.UrysohnsLemma
/-- A variation of **Urysohn's lemma**. In a Hausdorff locally compact space, for a compact set `K`
contained in an open set `V`, there exists a compactly supported continuous function `f` such that
`0 ≤ f ≤ 1`, `f = 1` on K and the support of `f` is contained in `V`.  -/
exists_continuousMap_one_of_isCompact_subset_isOpen : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] [LocallyCompactSpace X] {K V : Set X},
  IsCompact K →
    IsOpen V → K ⊆ V → ∃ f, Set.EqOn (⇑f) 1 K ∧ IsCompact (tsupport ⇑f) ∧ tsupport ⇑f ⊆ V ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
-- Mathlib.Order.Interval.Finset.Defs
Finset.mem_Icc : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b x : α}, x ∈ Finset.Icc a b ↔ a ≤ x ∧ x ≤ b
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.Iso.mk_inv : ∀ {α β : FinBoolAlg} (e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg),
  (FinBoolAlg.Iso.mk e).inv =
    CategoryTheory.InducedCategory.homMk
      (BoolAlg.ofHom
        (have __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }))
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
AlgebraicGeometry.Scheme.Hom.preimage_smoothLocus_eq : ∀ {X Y U : AlgebraicGeometry.Scheme} (f : U ⟶ X) (g : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f]
  [inst_1 : AlgebraicGeometry.LocallyOfFinitePresentation g],
  (TopologicalSpace.Opens.map f.base).obj (AlgebraicGeometry.Scheme.Hom.smoothLocus g) =
    AlgebraicGeometry.Scheme.Hom.smoothLocus (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Data.Finsupp.Basic
Finsupp.subtypeDomain_add : ∀ {α : Type u_1} {M : Type u_5} [inst : AddZeroClass M] {p : α → Prop} {v v' : α →₀ M},
  Finsupp.subtypeDomain p (v + v') = Finsupp.subtypeDomain p v + Finsupp.subtypeDomain p v'
-- Mathlib.LinearAlgebra.Matrix.ToLin
AlgEquiv.ofLinearEquiv.congr_simp : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (l l_1 : A₁ ≃ₗ[R] A₂) (e_l : l = l_1) (map_one : l 1 = 1)
  (map_mul : ∀ (x y : A₁), l (x * y) = l x * l y),
  AlgEquiv.ofLinearEquiv l map_one map_mul = AlgEquiv.ofLinearEquiv l_1 ⋯ ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.mapArrowLeft_id : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {f₁ : CategoryTheory.Arrow C₁}
  {f₃ : CategoryTheory.Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom),
  sq₁₃.mapArrowLeft sq₁₃ (CategoryTheory.CategoryStruct.id f₁) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk sq₁₃.π)
-- Init.Grind.ToInt
/-- The interval `[0, 2^n)`.  -/
Lean.Grind.IntInterval.uint : ℕ → Lean.Grind.IntInterval
-- Mathlib.RingTheory.FreeCommRing
/-- The natural map `FreeRing α → FreeCommRing α`, as a `RingHom`.  -/
FreeRing.coeRingHom : (α : Type u) → FreeRing α →+* FreeCommRing α
-- Init.Data.Order.Ord
Std.TransOrd.compareOfLessAndEq_of_antisymm_of_trans_of_total_of_not_le : ∀ {α : Type u} [inst : LT α] [inst_1 : LE α] [inst_2 : DecidableLT α] [DecidableLE α] [inst_4 : DecidableEq α],
  (∀ {x y : α}, x ≤ y → y ≤ x → x = y) →
    (∀ {x y z : α}, x ≤ y → y ≤ z → x ≤ z) →
      (∀ (x y : α), x ≤ y ∨ y ≤ x) → (∀ {x y : α}, ¬x ≤ y ↔ y < x) → Std.TransCmp fun x y => compareOfLessAndEq x y
-- Lean.Expr
/-- Natural number literal  -/
Lean.Literal.natVal : ℕ → Lean.Literal
-- Mathlib.NumberTheory.LSeries.Basic
/-- If the `LSeries` of `f` is summable at `s`, then `f = O(n^(re s))`.  -/
LSeriesSummable.isBigO_rpow : ∀ {f : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → f =O[Filter.atTop] fun n => ↑n ^ s.re