mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
/-- The cocone `Pairwise.cocone U` with cocone point `iSup U` over `Pairwise.diagram U` is isomorphic
to the cocone `opensLeCoverCocone U` (with the same cocone point)
after appropriate whiskering and postcomposition.
 -/
TopCat.Presheaf.SheafCondition.pairwiseCoconeIso : {X : TopCat} →
  {ι : Type u_2} →
    (U : ι → TopologicalSpace.Opens ↑X) →
      (CategoryTheory.Pairwise.cocone U).op ≅
        (CategoryTheory.Limits.Cone.postcomposeEquivalence
                (CategoryTheory.NatIso.op (TopCat.Presheaf.SheafCondition.pairwiseDiagramIso U))).functor.obj
          (CategoryTheory.Limits.Cone.whisker (TopCat.Presheaf.SheafCondition.pairwiseToOpensLeCover U).op
            (TopCat.Presheaf.SheafCondition.opensLeCoverCocone U).op)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_insert_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {v : β}, (m.insert k v).getKey? k = some k
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.fromSingleEquiv.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q n : ℤ} (h : p + n = q),
  CochainComplex.HomComplex.Cochain.fromSingleEquiv h = CochainComplex.HomComplex.Cochain.fromSingleEquiv h
-- Mathlib.Order.Lattice
/-- Pointwise minimum of two antitone functions is an antitone function.  -/
AntitoneOn.min : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : LinearOrder β] {f g : α → β} {s : Set α},
  AntitoneOn f s → AntitoneOn g s → AntitoneOn (fun x => min (f x) (g x)) s
-- Mathlib.CategoryTheory.Limits.Over
CategoryTheory.Over.createsColimitsOfSize : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → CategoryTheory.CreatesColimitsOfSize.{w, w', v, v, max u v, u} (CategoryTheory.Over.forget X)
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_restrict_apply_univ : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α),
  (μ.restrict s).real Set.univ = μ.real s
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.eventually_asympBound_r_pos : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r),
  ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), 0 < AkraBazziRecurrence.asympBound g a b (r i n)
-- Mathlib.Topology.Constructions.SumProd
Filter.Tendsto.prodMap_nhds : ∀ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W] {x : X} {y : Y} {z : Z} {w : W} {f : X → Y} {g : Z → W},
  Filter.Tendsto f (nhds x) (nhds y) →
    Filter.Tendsto g (nhds z) (nhds w) → Filter.Tendsto (Prod.map f g) (nhds (x, z)) (nhds (y, w))
-- Mathlib.NumberTheory.Real.Irrational
irrational_div_natCast_iff : ∀ {n : ℕ} {x : ℝ}, Irrational (x / ↑n) ↔ n ≠ 0 ∧ Irrational x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
/-- Verify that the constructed limit cone is indeed a limit.  -/
CategoryTheory.Limits.pullbackConeOfLeftIsoIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          [inst_1 : CategoryTheory.IsIso f] →
            CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.pullbackConeOfLeftIso f g)
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.sInfClosed : ∀ {α : Type u_1} [inst : CompleteLattice α] {L : CompleteSublattice α} {s : Set α}, s ⊆ ↑L → sInf s ∈ L
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.Functor.congr_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D}, F = G → ∀ (X : C), F.obj X = G.obj X
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rxc.Iterator.toList_eq_match : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.Rxc.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  {it : Std.Iter α},
  it.toList =
    match it.internalState.next with
    | none => []
    | some a =>
      if a ≤ it.internalState.upperBound then
        a :: { internalState := { next := Std.PRange.succ? a, upperBound := it.internalState.upperBound } }.toList
      else []
-- Std.Data.DTreeMap.Raw.Basic
/-- Compares two tree maps using Boolean equality on keys and values.

Returns `true` if the maps contain the same key-value pairs, `false` otherwise.
 -/
Std.DTreeMap.Raw.Const.beq : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} → [BEq β] → Std.DTreeMap.Raw α (fun x => β) cmp → Std.DTreeMap.Raw α (fun x => β) cmp → Bool
-- Mathlib.Algebra.Order.Ring.Abs
/-- If `n` is even and `a` is even, then `n % a` is even.  -/
Even.mod_even : ∀ {n a : ℕ}, Even n → Even a → Even (n % a)
-- Mathlib.Algebra.Group.End
/-- If `α` is equivalent to `β`, then `Perm α` is equivalent to `Perm β`.  -/
Equiv.permCongrHom : {α : Type u_4} → {β : Type u_5} → α ≃ β → Equiv.Perm α ≃* Equiv.Perm β
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
AddOpposite.dist_unop : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] (x y : αᵃᵒᵖ), dist (AddOpposite.unop x) (AddOpposite.unop y) = dist x y
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.instMonoidalCategory : {C : Type u} → CategoryTheory.MonoidalCategory (CategoryTheory.FreeMonoidalCategory C)
-- Mathlib.Data.Rat.Cast.Defs
Rat.cast_natCast : ∀ {α : Type u_3} [inst : DivisionRing α] (n : ℕ), ↑↑n = ↑n
-- Init.Data.UInt.BasicAux
instLEUSize : LE USize
-- Mathlib.Data.List.Basic
List.surjective_tail : ∀ {α : Type u}, Function.Surjective List.tail
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.instZero : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : Monoid R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : DistribMulAction R A] →
            [inst_3 : StarAddMonoid A] →
              [inst_4 : NonUnitalNonAssocSemiring B] →
                [inst_5 : DistribMulAction R B] → [inst_6 : StarAddMonoid B] → Zero (A →⋆ₙₐ[R] B)
-- Mathlib.Analysis.InnerProductSpace.LinearMap
/-- The adjoint of a linear isometric equivalence is its inverse.  -/
LinearIsometryEquiv.inner_map_eq_flip : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {E' : Type u_7} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (x : E)
  (y : E'), inner 𝕜 (f x) y = inner 𝕜 x (f.symm y)
-- Mathlib.CategoryTheory.Idempotents.Biproducts
CategoryTheory.Idempotents.Karoubi.complement_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (P : CategoryTheory.Idempotents.Karoubi C), P.complement.X = P.X
-- Mathlib.Topology.UniformSpace.Basic
UniformContinuousOn.congr : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f g : α → β} {s : Set α},
  UniformContinuousOn f s → Set.EqOn f g s → UniformContinuousOn g s
-- Lean.Elab.Parallel
/-- Runs a list of TermElabM computations in parallel and collects results in the original order,
including the saved state after each task completes.

Unlike `parIter`, this waits for all tasks to complete and returns results
in the same order as the input list, not in completion order.

Results are wrapped in `Except Exception (α × Term.SavedState)` so that errors in individual
tasks don't stop the collection - you can observe all results including which tasks failed.

The final TermElabM state is restored to the initial state (before tasks ran).
 -/
Lean.Elab.Term.TermElabM.par : {α : Type} →
  List (Lean.Elab.TermElabM α) → Lean.Elab.TermElabM (List (Except Lean.Exception (α × Lean.Elab.Term.SavedState)))
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.norm_eq_of_L1 : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] (x : PiLp 1 β),
  ‖x‖ = ∑ i, ‖x.ofLp i‖
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.false_of_right_to_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : D} {Y : C} (f : CategoryTheory.Join.right X ⟶ CategoryTheory.Join.left Y), False
-- Mathlib.Geometry.Diffeology.Basic
/-- Every constant map needs to be a plot.  -/
DiffeologicalSpace.constant_plots : ∀ {X : Type u_1} [self : DiffeologicalSpace X] {n : ℕ} (x : X), (fun x_1 => x) ∈ DiffeologicalSpace.plots n
-- Mathlib.Analysis.SpecialFunctions.Exponential
differentiableAt_exp_smul_const : ∀ {𝕂 : Type u_1} {𝔸 : Type u_3} [inst : RCLike 𝕂] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸]
  (x : 𝔸) (r : 𝕂), DifferentiableAt 𝕂 (fun t => NormedSpace.exp (t • x)) r
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.prodMonoidal_tensorUnit : ∀ (C₁ : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C₁] [inst_1 : CategoryTheory.MonoidalCategory C₁]
  (C₂ : Type u₂) [inst_2 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_3 : CategoryTheory.MonoidalCategory C₂],
  CategoryTheory.MonoidalCategoryStruct.tensorUnit (C₁ × C₂) =
    (CategoryTheory.MonoidalCategoryStruct.tensorUnit C₁, CategoryTheory.MonoidalCategoryStruct.tensorUnit C₂)
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddGrpCat.FilteredColimits.forget_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget AddGrpCat)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.toAffine_some : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {X Y : F} (h : W.Nonsingular ![X, Y, 1]),
  WeierstrassCurve.Projective.Point.toAffine W ![X, Y, 1] = WeierstrassCurve.Affine.Point.some X Y ⋯
-- Mathlib.Algebra.Order.Group.Unbundled.Int
Int.abs_sub_lt_of_lt_lt : ∀ {m a b : ℕ}, a < m → b < m → |↑b - ↑a| < ↑m
-- Mathlib.Data.FunLike.Group
FunLike.coeMonoidHom_apply : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : MulOne F] [inst_2 : MulOneClass β]
  [inst_3 : IsOneApply F α β] [inst_4 : IsMulApply F α β] (f : F), (FunLike.coeMonoidHom F α β) f = ⇑f
-- Init.Data.Repr
/-- Returns a representation of an optional value that should be able to be parsed as an equivalent
optional value.

This function is typically accessed through the `Repr (Option α)` instance.
 -/
Option.repr : {α : Type u_1} → [Repr α] → Option α → ℕ → Std.Format
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.singleton_vadd_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {a : α} {b : β}, {a} +ᵥ {b} = {a +ᵥ b}
-- Mathlib.Analysis.Normed.Module.Bases
/-- The basis constant for unconditional bases (supremum over all finite sets) as `enorm`.  -/
UnconditionalSchauderBasis.enormProjBound : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {X : Type u_2} →
      [inst_1 : NormedAddCommGroup X] →
        [inst_2 : NormedSpace 𝕜 X] → {β : Type u_3} → UnconditionalSchauderBasis β 𝕜 X → ENNReal
-- Lean.Environment
_private.Lean.Environment.0.Lean.AsyncContext.mkRaw.injEq : ∀ (declPrefix : Lean.Name) (realizingStack : List Lean.Name) (declPrefix_1 : Lean.Name)
  (realizingStack_1 : List Lean.Name),
  ({ declPrefix := declPrefix, realizingStack := realizingStack } =
      { declPrefix := declPrefix_1, realizingStack := realizingStack_1 }) =
    (declPrefix = declPrefix_1 ∧ realizingStack = realizingStack_1)
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.String.digitChar : (n : UInt32) → n < 16 → Char
-- Mathlib.Data.Finsupp.Defs
/-- `Finsupp.mapRange` of a surjective function is surjective.  -/
Finsupp.mapRange_surjective : ∀ {α : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] (e : M → N) (he₀ : e 0 = 0),
  Function.Surjective e → Function.Surjective (Finsupp.mapRange e he₀)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.map_atom : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (W : ℤ → R) {F : Type u_3}
  [inst_2 : FunLike F R S] [RingHomClass F R S] (f : F) (a b : ℤ),
  f (IsEllipticNet.atom W a b) = IsEllipticNet.atom (⇑f ∘ W) a b
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Int.Internal.Linear.Poly.isZero : Int.Internal.Linear.Poly → Bool
-- Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
/-- Given a bounded variation function `f`, we can construct a vector measure giving
mass `f.rightLim v - f.rightLim a` to each open-closed interval `(a, b]`. This is *not* the
measure associated to `f` in general, as we may need to adjust things at the bot element if
there is one.  -/
_private.Mathlib.MeasureTheory.VectorMeasure.BoundedVariation.0.BoundedVariationOn.exists_vectorMeasure_le_measureAux : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : DenselyOrdered α] [inst_2 : TopologicalSpace α]
  [inst_3 : OrderTopology α] [inst_4 : SecondCountableTopology α] [inst_5 : CompactIccSpace α] [hα : MeasurableSpace α]
  [inst_6 : BorelSpace α] {E : Type u_2} [inst_7 : NormedAddCommGroup E] [inst_8 : CompleteSpace E] {f : α → E}
  (hf : BoundedVariationOn f Set.univ),
  ∃ m,
    (∀ (u v : α), u ≤ v → m (Set.Ioc u v) = Function.rightLim f v - Function.rightLim f u) ∧
      m botSet = 0 ∧ ∀ (s : Set α), ‖m s‖ₑ ≤ (BoundedVariationOn.measureAux✝ hf) s
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Equiv.coe_toMulEquiv : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} {E' : Type u_4} [inst_3 : Group E'] {S' : GroupExtension N E' G} (equiv : S.Equiv S'),
  ⇑↑equiv = ⇑equiv
-- Lean.AddDecl
/-- Adds given declaration to the environment, respecting `debug.skipKernelTC`.  -/
Lean.Kernel.Environment.addDecl : Lean.Kernel.Environment →
  Lean.Options →
    Lean.Declaration → optParam (Option IO.CancelToken) none → Except Lean.Kernel.Exception Lean.Kernel.Environment
-- Mathlib.Order.Copy
OrderTop.copy.congr_simp : ∀ {α : Type u} {h h' : LE α} (c c_1 : OrderTop α) (e_c : c = c_1) (top top_1 : α) (e_top : top = top_1)
  (eq_top : top = ⊤) (le_eq : ∀ (x y : α), x ≤ y ↔ x ≤ y), c.copy top eq_top le_eq = c_1.copy top_1 ⋯ le_eq
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_eq_subst'_cert : ℤ → ℤ → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Bool
-- Init.Data.List.Monadic
List.mapM_nil : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {f : α → m β}, List.mapM f [] = pure []
-- Mathlib.Order.Filter.Basic
Filter.EventuallyLE.ge_iff_eq : ∀ {α : Type u} {β : Type v} [inst : PartialOrder β] {l : Filter α} {f g : α → β}, f ≤ᶠ[l] g → (g ≤ᶠ[l] f ↔ f =ᶠ[l] g)
-- Mathlib.Topology.Category.TopPair
/-- The second space of the pair  -/
TopPair.snd : {X : TopPair} → TopCat
-- Lean.Compiler.IR.Basic
Lean.IR.JoinPointId.mk : Lean.IR.Index → Lean.IR.JoinPointId
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.inter_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → m₃.WF → m₂.Equiv m₃ → (m₁ ∩ m₂).Equiv (m₁ ∩ m₃)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- The associativity of the composition of cochains.  -/
CochainComplex.HomComplex.Cochain.comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K L : CochainComplex C ℤ} {n₁ n₂ n₃ n₁₂ n₂₃ n₁₂₃ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁)
  (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (z₃ : CochainComplex.HomComplex.Cochain K L n₃) (h₁₂ : n₁ + n₂ = n₁₂)
  (h₂₃ : n₂ + n₃ = n₂₃) (h₁₂₃ : n₁ + n₂ + n₃ = n₁₂₃), (z₁.comp z₂ h₁₂).comp z₃ ⋯ = z₁.comp (z₂.comp z₃ h₂₃) ⋯
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.Context.mk.injEq : ∀ (cat : Lean.Name) (forceParens : Bool) (cat_1 : Lean.Name) (forceParens_1 : Bool),
  ({ cat := cat, forceParens := forceParens } = { cat := cat_1, forceParens := forceParens_1 }) =
    (cat = cat_1 ∧ forceParens = forceParens_1)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
AddAction.stabilizerEquivStabilizer.congr_simp : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {g g_1 : G} (e_g : g = g_1) {a b : α}
  (hg : b = g +ᵥ a), AddAction.stabilizerEquivStabilizer hg = AddAction.stabilizerEquivStabilizer ⋯
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α}, (t₁ ∪ t₂).get? k = (t₂.get? k).or (t₁.get? k)
-- Mathlib.RingTheory.PowerSeries.Basic
Polynomial.coe_injective : ∀ (R : Type u_1) [inst : Semiring R], Function.Injective Polynomial.toPowerSeries
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- If a `G`-representation on `A` is trivial, this is the natural map `Gᵃᵇ → A → H₁(G, A)`
sending `⟦g⟧, a` to `⟦single g a⟧`.  -/
groupHomology.mkH1OfIsTrivial : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) → [A.IsTrivial] → Additive (Abelianization G) →ₗ[ℤ] ↑A →ₗ[ℤ] ↑(groupHomology.H1 A)
-- Mathlib.NumberTheory.Divisors
Nat.Prime.sum_divisors : ∀ {α : Type u_1} [inst : AddCommMonoid α] {p : ℕ} {f : ℕ → α}, Nat.Prime p → ∑ x ∈ p.divisors, f x = f p + f 1
-- Mathlib.CategoryTheory.MorphismProperty.Composition
/-- A class of morphisms `W` has the of-precomp property w.r.t. `W'` if whenever
`f` is in `W'` and `f ≫ g` is in `W`, also `g` is in `W`.  -/
CategoryTheory.MorphismProperty.HasOfPrecompProperty : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.Monoidal.μ_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X Y : C) {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y)
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst (F.obj X) (F.obj Y)) h
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.continuousEvalConst : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  (𝔖 : Set (Set E)), ⋃₀ 𝔖 = Set.univ → ContinuousEvalConst (UniformConvergenceCLM σ F 𝔖) E F
-- Init.Data.Array.Perm
Array.Perm.refl : ∀ {α : Type u_1} (xs : Array α), xs.Perm xs
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.instPartialOrder : {L : FirstOrder.Language} →
  {M : Type w} → [inst : L.Structure M] → {A : Set M} → {α : Type u₁} → PartialOrder (L.DefinableSet A α)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_alter!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k : α} [inst_1 : Inhabited (β k)] {f : Option (β k) → Option (β k)},
      (Std.DTreeMap.Internal.Impl.alter! k f t).get! k = (f (t.get? k)).get!
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.coe_comp_lattice_hom' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [inst_5 : BoundedOrder γ] (f : BoundedLatticeHom β γ)
  (g : BoundedLatticeHom α β),
  { toSupHom := { toFun := ⇑f, map_sup' := ⋯ }.comp { toFun := ⇑g, map_sup' := ⋯ }, map_inf' := ⋯ } =
    { toFun := ⇑f, map_sup' := ⋯, map_inf' := ⋯ }.comp { toFun := ⇑g, map_sup' := ⋯, map_inf' := ⋯ }
-- Init.Data.Option.Lemmas
Option.pmap.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} (f f_1 : (a : α) → p a → β),
  f = f_1 →
    ∀ (o o_1 : Option α) (e_o : o = o_1) (a : ∀ (a : α), o = some a → p a), Option.pmap f o a = Option.pmap f_1 o_1 ⋯
-- Mathlib.Algebra.FreeAlgebra.Cardinality
Algebra.lift_cardinalMk_adjoin_le : ∀ (R : Type u) [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Set A),
  Cardinal.lift.{u, v} (Cardinal.mk ↥(Algebra.adjoin R s)) ≤
    max (max (Cardinal.lift.{v, u} (Cardinal.mk R)) (Cardinal.lift.{u, v} (Cardinal.mk ↑s))) Cardinal.aleph0
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- The unique meromorphic function `ℂ → ℂ` which agrees with `∑' n : ℕ, χ n / n ^ s` wherever the
latter is convergent. This is constructed as a linear combination of Hurwitz zeta functions.

Note that this is not the same as `LSeries χ`: they agree in the convergence range, but
`LSeries χ s` is defined to be `0` if `re s ≤ 1`.
 -/
DirichletCharacter.LFunction : {N : ℕ} → [NeZero N] → DirichletCharacter ℂ N → ℂ → ℂ
-- Mathlib.CategoryTheory.Comma.Over.StrictInitial
/-- If `C` has strict terminal objects and `X` is a terminal object, the category
`P.Under Q X` is equivalent to a point.  -/
CategoryTheory.MorphismProperty.underEquivOfIsTerminal : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (P Q : CategoryTheory.MorphismProperty C) →
      [P.ContainsIdentities] →
        [inst_2 : Q.IsMultiplicative] →
          [Q.RespectsIso] →
            [CategoryTheory.Limits.HasStrictTerminalObjects C] →
              (X : C) → CategoryTheory.Limits.IsTerminal X → (P.Under Q X ≌ CategoryTheory.Discrete PUnit.{w + 1})
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.card_support_le_one : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α}, f.support.card ≤ 1 ↔ f = 1
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.mem_domain_ofFromSpecStalk : ∀ {X Y S : AlgebraicGeometry.Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) [inst : IrreducibleSpace ↥X]
  [inst_1 : AlgebraicGeometry.LocallyOfFiniteType sY] {x : ↥X} [inst_2 : X.IsGermInjectiveAt x]
  (φ : AlgebraicGeometry.Spec (X.presheaf.stalk x) ⟶ Y)
  (h : CategoryTheory.CategoryStruct.comp φ sY = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) sX),
  x ∈ (AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk sX sY φ h).domain
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.E₈_off_diag_nonpos : ∀ (i j : Fin 8), i ≠ j → CartanMatrix.E₈ i j ≤ 0
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.Equivalence.right_triangle_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} (e : CategoryTheory.Bicategory.Equivalence a b),
  CategoryTheory.Bicategory.rightZigzag e.unit.hom e.counit.hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor e.inv).hom
      (CategoryTheory.Bicategory.leftUnitor e.inv).inv
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabCheckCore : Bool → Lean.Elab.Command.CommandElab
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.inl_injective : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N},
  Function.Injective ⇑SemidirectProduct.inl
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_real_closedBall : ∀ {a r : ℝ}, 0 ≤ r → MeasureTheory.volume.real (Metric.closedBall a r) = 2 * r
-- Std.Time.Notation.Spec
_private.Std.Time.Notation.Spec.0.Std.Time.convertOffsetO : Std.Time.OffsetO → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.isSupported_op_iff : ∀ {ι : 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]
  (K : HomologicalComplex C c') (e : c.Embedding c'), K.op.IsSupported e.op ↔ K.IsSupported e