mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.bijective : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S),
  Function.Bijective ⇑e
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_expect_le : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : Module ℚ≥0 E] [NormedSpace ℝ E] {ι : Type u_3} {s : Finset ι} {f : ι → α → E},
  (∀ i ∈ s, MeasureTheory.MemLp (f i) p μ) →
    1 ≤ p → MeasureTheory.lpNorm (s.expect fun i => f i) p μ ≤ s.expect fun i => MeasureTheory.lpNorm (f i) p μ
-- Mathlib.Logic.Equiv.Basic
Function.Involutive.symm_eq_self_of_involutive : ∀ {α : Sort u_1} (f : Equiv.Perm α), Function.Involutive ⇑f → Equiv.symm f = f
-- Mathlib.Order.Heyting.Basic
hnot_sdiff_comm : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (b a : α), ￢b \ a = ￢a \ b
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_lt_pow_left₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a b : M₀} [PosMulStrictMono M₀]
  [MulPosMono M₀], a < b → 0 ≤ a → ∀ {n : ℕ}, n ≠ 0 → a ^ n < b ^ n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_insertMany_empty_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [Std.TransOrd α] [inst : Inhabited α] {l : List (α × β)} {k k' : α},
  compare k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l →
        (↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty l ⋯)).getKey! k' = k
-- Mathlib.Topology.Algebra.Valued.ValuedField
/-- An abbreviation for `IsLocalRing.ResidueField 𝒪[K]` of a `Valued` instance, enabling the
notation `𝓀[K]` for the residue field of a valued field `K`.  -/
Valued.ResidueField : (K : Type u_1) →
  [inst : Field K] →
    {Γ₀ : outParam (Type u_2)} → [inst_1 : LinearOrderedCommGroupWithZero Γ₀] → [vK : Valued K Γ₀] → Type u_1
-- Mathlib.CategoryTheory.Bicategory.Opposites
/-- A 2-isomorphism in `Bᵒᵖ` gives a 2-isomorphism in `B`  -/
CategoryTheory.Iso.unop2 : {B : Type u} → [inst : CategoryTheory.Bicategory B] → {a b : Bᵒᵖ} → {f g : a ⟶ b} → (f ≅ g) → (f.unop ≅ g.unop)
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) {Y : AlgebraicGeometry.Scheme} (f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y)
  (hf :
    ∀ (x y : 𝒰.I₀),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y)) (f x) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (𝒰.f x) (𝒰.f y)) (f y))
  (x : 𝒰.I₀), CategoryTheory.CategoryStruct.comp (𝒰.f x) (AlgebraicGeometry.Scheme.Cover.glueMorphisms 𝒰 f hf) = f x
-- Lean.Meta.Match.MatcherInfo
/-- Whether this alternative has an artificial `Unit` parameter  -/
Lean.Meta.Match.AltParamInfo.hasUnitThunk : Lean.Meta.Match.AltParamInfo → Bool
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.prodComm_symm : ∀ (α : Type u) (β : Type u_1) [inst : UniformSpace α] [inst_1 : UniformSpace β],
  (UniformEquiv.prodComm α β).symm = UniformEquiv.prodComm β α
-- Mathlib.Order.SupClosed
isSublattice_sInter : ∀ {α : Type u_3} [inst : Lattice α] {S : Set (Set α)}, (∀ s ∈ S, IsSublattice s) → IsSublattice (⋂₀ S)
-- Mathlib.Topology.Algebra.Algebra
coe_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) = ⇑(algebraMap R A)
-- Mathlib.Order.SuccPred.Limit
IsGLB.isPredLimit_of_notMem : ∀ {α : Type u_1} {a : α} [inst : LinearOrder α] {s : Set α}, IsGLB s a → s.Nonempty → a ∉ s → Order.IsPredLimit a
-- Lean.Elab.MutualInductive
Lean.Elab.Command.ComputedFieldView.matchAlts : Lean.Elab.Command.ComputedFieldView → Lean.TSyntax `Lean.Parser.Term.matchAlts
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
/-- The abelian group structure on morphisms in `D`, when `L : C ⥤ D` is a localization
functor, `C` is preadditive and there is a left calculus of fractions.  -/
CategoryTheory.Localization.Preadditive.addCommGroup : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [CategoryTheory.Preadditive C] →
          (L : CategoryTheory.Functor C D) →
            (W : CategoryTheory.MorphismProperty C) →
              [L.IsLocalization W] → [W.HasLeftCalculusOfFractions] → (X' Y' : D) → AddCommGroup (X' ⟶ Y')
-- Mathlib.Algebra.Homology.ComplexShapeSigns
/-- the sign of the horizontal differential in the total complex  -/
TotalComplexShape.ε₁ : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₁₂ : Type u_4} →
      (c₁ : ComplexShape I₁) →
        (c₂ : ComplexShape I₂) → (c₁₂ : ComplexShape I₁₂) → [self : TotalComplexShape c₁ c₂ c₁₂] → I₁ × I₂ → ℤˣ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula.0.tacticMap_simp : Lean.ParserDescr
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.instToMessageDataResult : {u : Lean.Level} → {α : Q(Type u)} → {x : Q(«$α»)} → Lean.ToMessageData (Mathlib.Meta.NormNum.Result x)
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Reachable.sum_sup_edge : ∀ {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} {v v' : V} {w w' : W},
  G.Reachable v v' →
    H.Reachable w w' → ((G ⊕g H) ⊔ SimpleGraph.edge (Sum.inl v) (Sum.inr w)).Reachable (Sum.inl v') (Sum.inr w')
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.toAddMonObj_injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X : C}, Function.Injective (@CategoryTheory.AddGrpObj.toAddMonObj C inst inst_1 X)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
AlgHom.ext_on_codisjoint : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {F : Type u_4} [inst_5 : FunLike F A B] [AlgHomClass F R A B] {φ ψ : F}
  {S T : Subalgebra R A}, Codisjoint S T → Set.EqOn ⇑φ ⇑ψ ↑S → Set.EqOn ⇑φ ⇑ψ ↑T → φ = ψ
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.isLeftDerivedFunctor_iff_isRightKanExtension : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_2} D] [inst_2 : CategoryTheory.Category.{v_5, u_3} H]
  (LF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : L.comp LF ⟶ F) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W],
  LF.IsLeftDerivedFunctor α W ↔ LF.IsRightKanExtension α
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.one_toFun : ∀ (A : Type u_2) (B : Type u_3) [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (x : A), 1 x = 1
-- Mathlib.Order.Lattice
Prod.inf_def : ∀ (α : Type u) (β : Type v) [inst : Min α] [inst_1 : Min β] (p q : α × β), p ⊓ q = (p.1 ⊓ q.1, p.2 ⊓ q.2)
-- Lean.Meta.Basic
/-- Similar to `forallMetaTelescopeReducing`, stops
constructing the telescope when it reaches size `maxMVars`.  -/
Lean.Meta.forallMetaBoundedTelescope : Lean.Expr →
  ℕ →
    optParam Lean.MetavarKind Lean.MetavarKind.natural →
      Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.ExactPairing.evaluation_coevaluation_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  [inst_2 : CategoryTheory.ExactPairing X Y] {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (η_ X Y) X)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y X).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (ε_ X Y)) h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv h)
-- Init.Control.Lawful.Instances
ExceptT.run_pure : ∀ {m : Type u_1 → Type u_2} {α ε : Type u_1} [inst : Monad m] (x : α), (pure x).run = pure (Except.ok x)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.parser : Std.Time.FormatString → Std.Time.FormatConfig → Std.Time.Awareness → Std.Internal.Parsec.String.Parser Std.Time.DateTime
-- Batteries.Data.List.ArrayMap
List.toArrayMap_toList : ∀ {α : Type u} {β : Type v} (l : List α) (f : α → β), (l.toArrayMap f).toList = List.map f l
-- Init.Data.BitVec.Lemmas
BitVec.toInt_rotateLeft : ∀ {w : ℕ} {x : BitVec w} {r : ℕ},
  (x.rotateLeft r).toInt = (↑((x <<< (r % w)).toNat ||| (x >>> (w - r % w)).toNat)).bmod (2 ^ w)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.row_def : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α), A.row = fun i => A i
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformity_eq_comap_inv_mul_nhds_one_swapped : ∀ (Gₗ : Type u_2) [inst : UniformSpace Gₗ] [inst_1 : Group Gₗ] [IsLeftUniformGroup Gₗ],
  uniformity Gₗ = Filter.comap (fun x => x.2⁻¹ * x.1) (nhds 1)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.mul_floor_map_zero_le_floor_iterate_zero : ∀ (f : CircleDeg1Lift) (n : ℕ), ↑n * ⌊f 0⌋ ≤ ⌊(⇑f)^[n] 0⌋
-- Mathlib.Order.Category.PartOrd
PartOrd.dualEquiv_inverse : PartOrd.dualEquiv.inverse = PartOrd.dual
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_left_le_size_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t₁.size ≤ (t₁ ∪ t₂).size
-- Mathlib.Topology.Algebra.Field
Nonneg.val_inv_unitsHomeomorphPos_symm_apply_coe : ∀ (R : Type u_2) [inst : DivisionSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : PosMulReflectLT R] [inst_4 : TopologicalSpace R] [inst_5 : ContinuousInv₀ R] (r : { r // 0 < r }),
  ↑↑((Nonneg.unitsHomeomorphPos R).symm r)⁻¹ = (↑r)⁻¹
-- Mathlib.Algebra.DirectSum.Ring
/-- The `NatCast` instance on `A 0`, given `GSemiring A`.  -/
DirectSum.instNatCastOfNat : {ι : Type u_1} →
  (A : ι → Type u_2) →
    [inst : (i : ι) → AddCommMonoid (A i)] → [inst_1 : AddMonoid ι] → [DirectSum.GSemiring A] → NatCast (A 0)
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
CategoryTheory.JointlyReflectIsomorphisms.isIso_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  CategoryTheory.JointlyReflectIsomorphisms F →
    ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.IsIso f ↔ ∀ (i : I), CategoryTheory.IsIso ((F i).map f)
-- Init.Data.Range.Polymorphic.Nat
Std.instLawfulRcoIntersectionNat_2 : Std.Roi.LawfulRcoIntersection ℕ
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.op_whiskerRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ⟶ Y) (Z : C),
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z).op =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f.op (Opposite.op Z)
-- Init.Data.List.MinMax
List.max_cons : ∀ {α : Type u_1} [inst : Max α] [Std.Associative max] {a : α} {l : List α} {h : a :: l ≠ []},
  (a :: l).max h = l.max?.elim a fun x => a ⊔ x
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
/-- If a function `f` is locally integrable on a set `s` in a second countable topological space,
then there exists a sequence of open sets `u n` covering `s` such that `f` is integrable on each
set `u n ∩ s`.  -/
MeasureTheory.LocallyIntegrableOn.exists_nat_integrableOn : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} {s : Set X} [SecondCountableTopology X],
  MeasureTheory.LocallyIntegrableOn f s μ →
    ∃ u, (∀ (n : ℕ), IsOpen (u n)) ∧ s ⊆ ⋃ n, u n ∧ ∀ (n : ℕ), MeasureTheory.IntegrableOn f (u n ∩ s) μ
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
/-- The functor which maps an object `A` in `C` to the projection `A ⊗ X ⟶ X` in `Over X`.
This is the computable analogue of the functor `Over.star`.  -/
CategoryTheory.toOver : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.CartesianMonoidalCategory C] → (X : C) → CategoryTheory.Functor C (CategoryTheory.Over X)
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.saturate_I₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (i j : E.I₀), E.saturate.I₁ i j = E.Relation i j
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.of.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  AdicCompletion.of I M = { toFun := fun x => ⟨fun n => (I ^ n • ⊤).mkQ x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.resLE_eq_morphismRestrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens},
  AlgebraicGeometry.Scheme.Hom.resLE f U ((TopologicalSpace.Opens.map f.base).obj U) ⋯ = f ∣_ U
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.maxKey?_modifyKey_beq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {k : α} {f : β → β} {km kmm : α} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ (hkm : Std.Internal.List.maxKey? l = some km),
      (Std.Internal.List.maxKey? (Std.Internal.List.Const.modifyKey k f l)).get ⋯ = kmm → (kmm == km) = true
-- Mathlib.Data.NNRat.Defs
NNRat.mk_natCast : ∀ (n : ℕ), ⟨↑n, ⋯⟩ = ↑n
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
FreeAbelianGroup.toFinsupp_of : ∀ {X : Type u_1} (x : X), FreeAbelianGroup.toFinsupp (FreeAbelianGroup.of x) = fun₀ | x => 1
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.opSpan_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  (X_1 : CategoryTheory.Limits.WalkingSpanᵒᵖ),
  (CategoryTheory.Limits.opSpan f g).inv.app X_1 =
    (match Opposite.unop X_1 with
      | none => CategoryTheory.Iso.refl (Opposite.op X)
      | some CategoryTheory.Limits.WalkingPair.left => CategoryTheory.Iso.refl (Opposite.op Y)
      | some CategoryTheory.Limits.WalkingPair.right => CategoryTheory.Iso.refl (Opposite.op Z)).hom
-- Lean.Declaration
/-- Base structure for `AxiomVal`, `DefinitionVal`, `TheoremVal`, `InductiveVal`, `ConstructorVal`, `RecursorVal` and `QuotVal`.  -/
Lean.ConstantVal : Type
-- Mathlib.RingTheory.WittVector.DiscreteValuationRing
WittVector.exists_eq_pow_p_mul : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [CharP k p] [PerfectRing k p]
  (a : WittVector p k), a ≠ 0 → ∃ m b, b.coeff 0 ≠ 0 ∧ a = ↑p ^ m * b
-- Mathlib.Logic.Relation
Relation.SymmGen.instSymm : ∀ {α : Type u_1} {r : α → α → Prop}, Std.Symm (Relation.SymmGen r)
-- Mathlib.FieldTheory.Finite.Basic
Int.prime_dvd_pow_self_sub : ∀ {p : ℕ}, Nat.Prime p → ∀ (n : ℤ), ↑p ∣ n ^ p - n
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
transcendental_liouvilleNumber : ∀ {m : ℕ}, 2 ≤ m → Transcendental ℤ (liouvilleNumber ↑m)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.mem_of_insertRupUnits : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  ∀ c ∈ (f.insertRupUnits units).1.toList,
    c ∈ List.map Std.Tactic.BVDecide.LRAT.Internal.Clause.unit units ∨ c ∈ f.toList
-- Mathlib.Analysis.Normed.Group.Uniform
locallyLipschitzOn_neg_iff : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {f : α → E}
  {s : Set α}, LocallyLipschitzOn s (-f) ↔ LocallyLipschitzOn s f
-- Mathlib.NumberTheory.LSeries.RiemannZeta
/-- Riemann zeta functional equation, formulated for `ζ`: if `1 - s ∉ ℕ`, then we have
`ζ (1 - s) = 2 ^ (1 - s) * π ^ (-s) * Γ s * sin (π * (1 - s) / 2) * ζ s`.  -/
riemannZeta_one_sub : ∀ {s : ℂ},
  (∀ (n : ℕ), s ≠ -↑n) →
    s ≠ 1 →
      riemannZeta (1 - s) = 2 * (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s * Complex.cos (↑Real.pi * s / 2) * riemannZeta s
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.lt_of_revMatchAt?_eq_some : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice} {startPos endPos : s.Pos},
  String.Slice.Pattern.Model.revMatchAt? pat endPos = some startPos → startPos < endPos
-- Mathlib.Topology.Bases
TopologicalSpace.exists_countable_dense : ∀ (α : Type u) [t : TopologicalSpace α] [TopologicalSpace.SeparableSpace α], ∃ s, s.Countable ∧ Dense s
-- Mathlib.CategoryTheory.Shift.Localization
CategoryTheory.NatTrans.commShift_iso_hom_of_localization : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W] (A : Type w) [inst_4 : AddMonoid A]
  [inst_5 : CategoryTheory.HasShift C A] (F : CategoryTheory.Functor C E) (F' : CategoryTheory.Functor D E)
  [inst_6 : CategoryTheory.Localization.Lifting L W F F'] [inst_7 : CategoryTheory.HasShift D A]
  [inst_8 : CategoryTheory.HasShift E A] [inst_9 : L.CommShift A] [inst_10 : F.CommShift A],
  CategoryTheory.NatTrans.CommShift (CategoryTheory.Localization.Lifting.iso L W F F').hom A
-- Mathlib.RingTheory.Localization.AtPrime.Extension
IsDedekindDomain.primesOverEquivPrimesOver_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (Rₚ : Type u_3) [inst_4 : CommRing Rₚ] [inst_5 : Algebra R Rₚ]
  [inst_6 : IsLocalization.AtPrime Rₚ p] [inst_7 : IsLocalRing Rₚ] (Sₚ : Type u_4) [inst_8 : CommRing Sₚ]
  [inst_9 : Algebra S Sₚ] [inst_10 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]
  [inst_11 : Algebra Rₚ Sₚ] [inst_12 : IsDomain R] [inst_13 : IsDedekindDomain S] [inst_14 : Module.IsTorsionFree R S]
  [inst_15 : Algebra R Sₚ] [inst_16 : IsScalarTower R S Sₚ] [inst_17 : IsScalarTower R Rₚ Sₚ] (hp : p ≠ ⊥)
  (P : ↑(p.primesOver S)), ↑((IsDedekindDomain.primesOverEquivPrimesOver p Rₚ Sₚ hp) P) = Ideal.map (algebraMap S Sₚ) ↑P
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.ProEt.instLocallyCoverDenseOverForgetOverProetaleTopology : ∀ (S : AlgebraicGeometry.Scheme),
  (AlgebraicGeometry.Scheme.ProEt.forget S).LocallyCoverDense (AlgebraicGeometry.Scheme.proetaleTopology.over S)
-- Mathlib.Algebra.Module.FinitePresentation
Module.finitePresentation_of_ker : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.FinitePresentation R N] (l : M →ₗ[R] N),
  Function.Surjective ⇑l → ∀ [Module.FinitePresentation R ↥l.ker], Module.FinitePresentation R M
-- Lean.Meta.LazyDiscrTree
/-- Extract and drop entries at a specific key, returning the dropped entries.  -/
Lean.Meta.LazyDiscrTree.extractKey : {α : Type} →
  Lean.Meta.LazyDiscrTree α → List Lean.Meta.LazyDiscrTree.Key → Lean.MetaM (Array α × Lean.Meta.LazyDiscrTree α)
-- Mathlib.Analysis.Normed.Algebra.Spectrum
_private.Mathlib.Analysis.Normed.Algebra.Spectrum.0.AlgHom.«term↑ₐ» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeLeftOpOfConeEquiv_functor_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J Cᵒᵖ} (c : (CategoryTheory.Limits.Cone F)ᵒᵖ),
  CategoryTheory.Limits.coconeLeftOpOfConeEquiv.functor.obj c =
    CategoryTheory.Limits.coconeLeftOpOfCone (Opposite.unop c)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.leftUnshift_leftShift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n + a = n'),
  (γ.leftShift a n' hn').leftUnshift n hn' = γ
-- Mathlib.Order.Filter.Prod
Filter.mem_prod_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set (α × β)} {f : Filter α} {g : Filter β},
  s ∈ f ×ˢ g ↔ ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ ×ˢ t₂ ⊆ s
-- Lean.Data.Lsp.Internal
/-- End line of range.  -/
Lean.Lsp.DeclInfo.rangeEndPosLine : Lean.Lsp.DeclInfo → ℕ
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instWeakEquivalenceOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsWeakEquivalencesOfIsIso : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  {X Y : C} (f : X ⟶ Y)
  [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)]
  [(HomotopicalAlgebra.weakEquivalences C).IsStableUnderRetracts] [CategoryTheory.IsIso f],
  HomotopicalAlgebra.WeakEquivalence f
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.shortComplexH2_g : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u_1, u, u} k G),
  (groupCohomology.shortComplexH2 A).g = groupCohomology.d₂₃ A
-- Init.Data.BitVec.Lemmas
BitVec.toNat_shiftConcat_lt_of_lt : ∀ {w : ℕ} {x : BitVec w} {b : Bool} {k : ℕ}, k < w → x.toNat < 2 ^ k → (x.shiftConcat b).toNat < 2 ^ (k + 1)
-- Mathlib.Data.NNReal.Basic
NNReal.coe_single : ∀ {α : Type u_2} [inst : DecidableEq α] (a : α) (b : NNReal) (c : α), ↑(Pi.single a b c) = Pi.single a (↑b) c
-- Mathlib.Analysis.Calculus.FDeriv.Defs
/-- **Alias** of the reverse direction of `hasFDerivWithinAt_iff_isLittleOTVS`. -/
HasFDerivWithinAt.of_isLittleOTVS : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E},
  ((fun x' => f x' - f x - f' (x' - x)) =o[𝕜; nhdsWithin x s] fun x' => x' - x) → HasFDerivWithinAt f f' s x
-- Mathlib.Analysis.Fourier.AddCircleMulti
UnitAddTorus.mFourier_norm : ∀ {d : Type u_1} [inst : Fintype d] {n : d → ℤ}, ‖UnitAddTorus.mFourier n‖ = 1
-- Mathlib.Geometry.Manifold.Riemannian.Basic
/-- Register on the tangent space to a normed vector space the same `NormedSpace` structure
as in the vector space.

Should not be a global instance, as it does not coincide definitionally with the Riemannian
structure for inner product spaces, but can be activated locally.  -/
normedSpaceTangentSpaceVectorSpace : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] → (x : E) → NormedSpace ℝ (TangentSpace (modelWithCornersSelf ℝ E) x)
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
/-- `ζ 0 = 0`, otherwise `ζ x = 1`. The Dirichlet Series is the Riemann `ζ`.  -/
ArithmeticFunction.zeta : ArithmeticFunction ℕ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_filter_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k k' : α} {fallback : β},
  t.getKey? k = some k' →
    (Std.ExtTreeMap.filter f t).getD k fallback = (Option.filter (fun x => f k' x) t[k]?).getD fallback
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.not_nonempty_iff_eq_bot : ∀ {α : Type u_2} [inst : TopologicalSpace α] (U : TopologicalSpace.Opens α), ¬(↑U).Nonempty ↔ U = ⊥