mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.func : {L : FirstOrder.Language} → {α : Type u'} → {l : ℕ} → L.Functions l → (Fin l → L.Term α) → L.Term α
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] (h : (↑m).WF) {l : List ((a : α) × β a)} {k : α}
  (contains : (List.map Sigma.fst l).contains k = false) {h' : (↑(m.insertMany l)).contains k = true},
  (↑(m.insertMany l)).get k h' = m.get k ⋯
-- Mathlib.Algebra.Module.Submodule.IterateMapComap
/-- If `f(K) ≤ i(K)`, then `LinearMap.iterateMapComap` is not decreasing.  -/
LinearMap.iterateMapComap_le_succ : ∀ {R : Type u_1} {N : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (f i : N →ₗ[R] M) (K : Submodule R N),
  Submodule.map f K ≤ Submodule.map i K → ∀ (n : ℕ), f.iterateMapComap i n K ≤ f.iterateMapComap i (n + 1) K
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_pos : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M] {f : ι → M}
  {s : Finset ι} [AddLeftStrictMono M], (∀ i ∈ s, 0 < f i) → s.Nonempty → 0 < ∑ i ∈ s, f i
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Polynomial.cyclotomic'.eq_1 : ∀ (n : ℕ) (R : Type u_2) [inst : CommRing R] [inst_1 : IsDomain R],
  Polynomial.cyclotomic' n R = ∏ μ ∈ primitiveRoots n R, (Polynomial.X - Polynomial.C μ)
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonLeanModule : Lean.ToJson Lean.Lsp.LeanModule
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- A homological complex `K` is acyclic if it is exact at `i` for any `i`.  -/
HomologicalComplex.Acyclic : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} → {c : ComplexShape ι} → HomologicalComplex C c → Prop
-- Mathlib.Order.CompleteLattice.Basic
iInf₂_eq_top : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_6} [inst : CompleteLattice α] {f : (i : ι) → κ i → α},
  ⨅ i, ⨅ j, f i j = ⊤ ↔ ∀ (i : ι) (j : κ i), f i j = ⊤
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_fun_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} (f : 𝕜 → F),
  iteratedDerivWithin n (fun z => -f z) s x = -iteratedDerivWithin n f s x
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.add_eq_mk : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x y : K ⋊⁅ψ⁆ L),
  x + y = { left := x.left + y.left, right := x.right + y.right }
-- Mathlib.Analysis.Analytic.Inverse
HasFPowerSeriesAt.tendsto_partialSum_prod_of_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → G} {q : FormalMultilinearSeries 𝕜 F G}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E},
  HasFPowerSeriesAt f (q.comp p) x →
    0 < q.radius →
      0 < p.radius →
        ∀ᶠ (y : E) in nhds 0,
          Filter.Tendsto (fun a => q.partialSum a.1 (p.partialSum a.2 y - (p 0) fun x => 0)) Filter.atTop
            (nhds (f (x + y)))
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.id_actionHomLeft_assoc : ∀ {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} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (c : C) (d : D) {Z : D}
  (h : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (CategoryTheory.CategoryStruct.id d) c)
      h =
    h
-- Lean.Parser.Extra
Lean.Parser.termParser.parenthesizer : optParam ℕ 0 → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Topology.IsClosedEmbedding.measurable : ∀ {α : Type u_1} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [inst_3 : TopologicalSpace γ] [inst_4 : MeasurableSpace γ] [BorelSpace γ] {f : α → γ},
  Topology.IsClosedEmbedding f → Measurable f
-- Mathlib.Topology.DiscreteSubset
IsCompact.cofinite_inf_le_codiscreteWithin : ∀ {X : Type u_1} [inst : TopologicalSpace X] {K : Set X},
  IsCompact K → Filter.cofinite ⊓ Filter.principal K ≤ Filter.codiscreteWithin K
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_comp_smul : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p]
  [ContinuousMap.UniqueHom R A] {S : Type u_3} [inst_10 : SMul S R] [ContinuousConstSMul S R]
  [inst_12 : SMulZeroClass S A] [IsScalarTower S R A] [IsScalarTower S R (R → R)] (s : S) (f : R → R) (a : A),
  autoParam (ContinuousOn f ((fun x => s • x) '' spectrum R a)) cfc_comp_smul._auto_1 →
    autoParam (p a) cfc_comp_smul._auto_3 → cfc (fun x => f (s • x)) a = cfc f (s • a)
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F], F.leftDerivedZeroIsoSelf.hom = F.fromLeftDerivedZero
-- Lean.Meta.Tactic.Subst
Lean.Meta.trySubstVar : Lean.MVarId → Lean.FVarId → Lean.MetaM Lean.MVarId
-- Init.Data.BitVec.Lemmas
BitVec.ctz.eq_1 : ∀ {w : ℕ} (x : BitVec w), x.ctz = x.reverse.clz
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- At an invertible element `x` of a normed algebra `R`, the Fréchet derivative of the inversion
operation is the linear map `fun t ↦ - x⁻¹ * t * x⁻¹`.

TODO (low prio): prove a version without assumption `[HasSummableGeomSeries R]` but within the set
of units.  -/
hasFDerivAt_ringInverse : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {R : Type u_5} [inst_1 : NormedRing R] [HasSummableGeomSeries R]
  [inst_3 : NormedAlgebra 𝕜 R] (x : Rˣ),
  HasFDerivAt Ring.inverse (-((ContinuousLinearMap.mulLeftRight 𝕜 R) ↑x⁻¹) ↑x⁻¹) ↑x
-- Mathlib.Topology.Separation.Basic
instT1SpaceCofiniteTopology : ∀ {X : Type u_1}, T1Space (CofiniteTopology X)
-- Aesop.Forward.Substitution
Aesop.Substitution.instHashable : Hashable Aesop.Substitution
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.comap_inclusion_subgroupOf : ∀ {G : Type u_1} [inst : Group G] {K₁ K₂ : Subgroup G} (h : K₁ ≤ K₂) (H : Subgroup G),
  Subgroup.comap (Subgroup.inclusion h) (H.subgroupOf K₂) = H.subgroupOf K₁
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.isNilpotent_toEnd_sub_algebraMap : ∀ {R : Type u_2} {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [IsNoetherian R M] (χ : L → R) (x : L),
  IsNilpotent
    ((LieModule.toEnd R L ↥(LieModule.genWeightSpace M χ)) x -
      (algebraMap R (Module.End R ↥(LieModule.genWeightSpace M χ))) (χ x))
-- Mathlib.CategoryTheory.Monoidal.Braided.Transport
CategoryTheory.Functor.LaxMonoidal.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D}
  (ε ε_1 :
    CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
  (e_ε : ε = ε_1)
  (μ μ_1 :
    (X Y : C) →
      CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ⟶
        F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
  (e_μ : μ = μ_1)
  (μ_natural_left :
    ∀ {X Y : C} (f : X ⟶ Y) (X' : C),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X'))
          (μ Y X') =
        CategoryTheory.CategoryStruct.comp (μ X X') (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X')))
  (μ_natural_right :
    ∀ {X Y : C} (X' : C) (f : X ⟶ Y),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f))
          (μ X' Y) =
        CategoryTheory.CategoryStruct.comp (μ X' X) (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X' f)))
  (associativity :
    ∀ (X Y Z : C),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (μ X Y) (F.obj Z))
          (CategoryTheory.CategoryStruct.comp (μ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
            (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)) =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (μ Y Z))
            (μ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))))
  (left_unitality :
    ∀ (X : C),
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ε (F.obj X))
          (CategoryTheory.CategoryStruct.comp (μ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X)
            (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom)))
  (right_unitality :
    ∀ (X : C),
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).hom =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) ε)
          (CategoryTheory.CategoryStruct.comp (μ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
            (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom))),
  { ε := ε, μ := μ, μ_natural_left := μ_natural_left, μ_natural_right := μ_natural_right,
      associativity := associativity, left_unitality := left_unitality, right_unitality := right_unitality } =
    { ε := ε_1, μ := μ_1, μ_natural_left := ⋯, μ_natural_right := ⋯, associativity := ⋯, left_unitality := ⋯,
      right_unitality := ⋯ }
-- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
/-- The derivative `D_yf(y)` is `C^m` at `x₀`, where the derivative is taken as a continuous
linear map. We have to assume that `f` is `C^n` at `x₀` for some `n ≥ m + 1`.
We have to insert a coordinate change from `x₀` to `x` to make the derivative sensible.
This is a special case of `ContMDiffAt.mfderiv` where `f` does not contain any parameters and
`g = id`.
 -/
ContMDiffAt.mfderiv_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {m n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] [Is : IsManifold I 1 M]
  [I's : IsManifold I' 1 M'] {x₀ : M} {f : M → M'},
  ContMDiffAt I I' n f x₀ →
    m + 1 ≤ n →
      ContMDiffAt I (modelWithCornersSelf 𝕜 (E →L[𝕜] E')) m (inTangentCoordinates I I' id f (mfderiv% f) x₀) x₀
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.IsLocallyDirected.ι_eq_ι_iff : ∀ {J : Type w} [inst : CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)]
  [inst_2 : (F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [inst_3 : Quiver.IsThin J]
  [inst_4 : Small.{u, w} J] {i j : J} {xi : ↥(F.obj i)} {xj : ↥(F.obj j)},
  (CategoryTheory.Limits.colimit.ι F i) xi = (CategoryTheory.Limits.colimit.ι F j) xj ↔
    ∃ k fi fj x, (F.map fi) x = xi ∧ (F.map fj) x = xj
-- Mathlib.Algebra.Group.Hom.Defs
/-- The proposition that the function preserves addition  -/
AddHomClass.map_add : ∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} {inst : Add M} {inst_1 : Add N}
  {inst_2 : FunLike F M N} [self : AddHomClass F M N] (f : F) (x y : M), f (x + y) = f x + f y
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.PackedBitVec.bv : (self : Std.Tactic.BVDecide.BVExpr.PackedBitVec) → BitVec self.w
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.encode_lt_rfind' : ∀ (cf : Nat.Partrec.Code), Encodable.encode cf < Encodable.encode cf.rfind'
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.coeff_hsum_eq_sum : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  {s : HahnSeries.SummableFamily Γ R α} {g : Γ}, s.hsum.coeff g = ∑ i ∈ (s.coeff g).support, (s i).coeff g
-- Mathlib.Analysis.InnerProductSpace.SingularValues
LinearMap.sq_singularValues_fin : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F]
  [inst_6 : FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) {n : ℕ} (hn : Module.finrank 𝕜 E = n) (i : Fin n),
  T.singularValues ↑i ^ 2 = ⋯.eigenvalues hn i
-- Init.Data.Int.Order
Int.toNat_add_nat : ∀ {a : ℤ}, 0 ≤ a → ∀ (n : ℕ), (a + ↑n).toNat = a.toNat + n
-- Mathlib.Logic.Equiv.Set
/-- Given an equivalence `e₀` between sets `s : Set α` and `t : Set β`, the set of equivalences
`e : α ≃ β` such that `e ↑x = ↑(e₀ x)` for each `x : s` is equivalent to the set of equivalences
between `sᶜ` and `tᶜ`.  -/
Equiv.Set.compl : {α : Type u} →
  {β : Type v} →
    {s : Set α} →
      {t : Set β} →
        [DecidablePred fun x => x ∈ s] →
          [DecidablePred fun x => x ∈ t] → (e₀ : ↑s ≃ ↑t) → { e // ∀ (x : ↑s), e ↑x = ↑(e₀ x) } ≃ (↑sᶜ ≃ ↑tᶜ)
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.eq_normN_cert : Lean.Grind.Linarith.Expr → Lean.Grind.Linarith.Expr → Bool
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedSubgroup.ext_iff : ∀ {G : Type u} {inst : Group G} {inst_1 : TopologicalSpace G} {x y : ClosedSubgroup G},
  x = y ↔ (↑x).carrier = (↑y).carrier
-- Mathlib.Algebra.DirectSum.Internal
/-- The difference with `DirectSum.finsetProd_apply_eq_zero` is that the indices at which
the terms of the multiset are zero is allowed to vary.  -/
finsetProd_apply_eq_zero' : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : AddCommMonoid ι] [inst_1 : LinearOrder ι] [IsOrderedAddMonoid ι]
  [inst_3 : DecidableEq ι] [CanonicallyOrderedAdd ι] [inst_5 : CommSemiring R] [inst_6 : SetLike σ R]
  [inst_7 : AddSubmonoidClass σ R] {A : ι → σ} [inst_8 : SetLike.GradedMonoid A]
  {s : Finset ((DirectSum ι fun i => ↥(A i)) × ι)},
  (∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0) → ∀ ⦃n : ι⦄, n < ∑ xn ∈ s, xn.2 → (∏ xn ∈ s, xn.1) n = 0
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.ofIsoLimit_lift : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {r t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit r)
  (i : r ≅ t) (s : CategoryTheory.Limits.Cone F),
  (P.ofIsoLimit i).lift s = CategoryTheory.CategoryStruct.comp (P.lift s) i.hom.hom
-- Mathlib.Data.Finset.Sort
/-- The bijection `orderEmbOfFin s h` sends `k-1` to the maximum of `s`.  -/
Finset.orderEmbOfFin_last : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {k : ℕ} (h : s.card = k) (hz : 0 < k),
  (s.orderEmbOfFin h) ⟨k - 1, ⋯⟩ = s.max' ⋯
-- Mathlib.Data.Finsupp.Basic
Finsupp.comapDomain_apply : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α → β) (l : β →₀ M)
  (hf : Set.InjOn f (f ⁻¹' ↑l.support)) (a : α), (Finsupp.comapDomain f l hf) a = l (f a)
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
riemannZeta₀.eq_1 : ∀ (s : ℂ), riemannZeta₀ s = if s = 1 then ↑Real.eulerMascheroniConstant else riemannZeta s - (s - 1)⁻¹
-- Init.Data.UInt.Lemmas
USize.ofFin_uint8ToFin : ∀ (n : UInt8), USize.ofFin (Fin.castLE UInt8.size_le_usizeSize n.toFin) = n.toUSize
-- Mathlib.Data.Finsupp.AList
AList.lookupFinsupp_apply : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : DecidableEq α] (l : AList fun _x => M) (a : α),
  l.lookupFinsupp a = (AList.lookup a l).getD 0
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.instString : Lean.Elab.ConfigEval.EvalExpr String
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.aleph0_power_aleph0 : Cardinal.aleph0 ^ Cardinal.aleph0 = Cardinal.continuum
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.neg_domain : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (f : E →ₛₗ.[σ] F),
  (-f).domain = f.domain
-- Batteries.Data.List.Lemmas
List.disjoint_append_right : ∀ {α : Type u_1} {l l₁ l₂ : List α}, l.Disjoint (l₁ ++ l₂) ↔ l.Disjoint l₁ ∧ l.Disjoint l₂
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.lift_inv_comp_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.GrpObj A] [inst_3 : CategoryTheory.GrpObj B] (f : A ⟶ B)
  [CategoryTheory.IsMonHom f],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv f) f)
      CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) CategoryTheory.MonObj.one
-- Std.Data.TreeMap.Lemmas
/-- Simpler variant of `getD_filterMap` when `LawfulEqCmp` is available.  -/
Std.TreeMap.getD_filterMap' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → Option γ} {k : α} {fallback : γ},
  (Std.TreeMap.filterMap f t).getD k fallback = (t[k]?.bind (f k)).getD fallback
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.baseSet_at : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (i : ι), Z.baseSet i = (Z.localTriv i).baseSet
-- Mathlib.Algebra.Group.Subsemigroup.Basic
Subsemigroup.instInfSet.eq_1 : ∀ {M : Type u_1} [inst : Mul M],
  Subsemigroup.instInfSet = { sInf := fun s => { carrier := ⋂ t ∈ s, ↑t, mul_mem' := ⋯ } }
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- The bimonoid morphism from any bimonoid to the trivial bimonoid.  -/
CategoryTheory.Bimon.toTrivial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (A : CategoryTheory.Bimon C) → A ⟶ CategoryTheory.Bimon.trivial C
-- Mathlib.Data.Set.Insert
Set.ofPred_eq_eq_singleton' : ∀ {α : Type u_1} {a : α}, {x | a = x} = {a}
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → Bool}, t.WF → (Std.TreeMap.Raw.filter f t).WF
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.dvd_of_mem_factors' : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a : α} {p : Associates α}
  {hp : Irreducible p} {hz : a ≠ 0}, ⟨p, hp⟩ ∈ Associates.factors' a → p ∣ Associates.mk a
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
AlgebraicGeometry.UniversallyOpen.instRespectsIsoScheme : CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.UniversallyOpen
-- Mathlib.CategoryTheory.Equivalence
/-- Interpret a functor that is an equivalence as an equivalence.  -/
CategoryTheory.Functor.asEquivalence : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (F : CategoryTheory.Functor C D) → [F.IsEquivalence] → C ≌ D
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddModObj.ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.AddMonObj M] {X : C} {h₁ h₂ : CategoryTheory.AddModObj M X},
  h₁ = h₂ ↔ CategoryTheory.AddModObj.vadd = CategoryTheory.AddModObj.vadd
-- Batteries.Data.List.Basic
/-- `Chain R a l` means that `R` holds between adjacent elements of `a::l`.
```
Chain R a [b, c, d] ↔ R a b ∧ R b c ∧ R c d
```  -/
List.Chain : {α : Type u_1} → (α → α → Prop) → α → List α → Prop
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Pre.instInhabited : (R : Type u_1) → (X : Type u_2) → [CommSemiring R] → Inhabited (FreeAlgebra.Pre R X)
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- If `G.IsBipartiteWith s t` and `w ∈ t`, then the neighbor finset of `w` is the set of vertices
in `s` adjacent to `w` in `G`.  -/
SimpleGraph.isBipartiteWith_neighborFinset' : ∀ {V : Type u_1} {w : V} {G : SimpleGraph V} {s t : Finset V} [inst : Fintype ↑(G.neighborSet w)]
  [inst_1 : DecidableRel G.Adj], G.IsBipartiteWith ↑s ↑t → w ∈ t → G.neighborFinset w = {v ∈ s | G.Adj v w}
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.beq.eq_1 : ∀ (a b : Float.Model.UnpackedFloat), a.beq b = (a.compare b == some Ordering.eq)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.val_inclusion : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] {S T : NonUnitalStarSubalgebra R A} (h : S ≤ T) (s : ↥S),
  ↑((NonUnitalStarSubalgebra.inclusion h) s) = ↑s
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
/-- Auxiliary construction for `lift`.  -/
CategoryTheory.ProjectiveResolution.liftFOne : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {Y Z : C} →
        (Y ⟶ Z) →
          (P : CategoryTheory.ProjectiveResolution Y) →
            (Q : CategoryTheory.ProjectiveResolution Z) → P.complex.X 1 ⟶ Q.complex.X 1
-- Mathlib.Analysis.Normed.Module.Basic
norm_algebraMap_nnreal : ∀ (𝕜' : Type u_2) [inst : SeminormedRing 𝕜'] [NormOneClass 𝕜'] [inst_2 : NormedAlgebra ℝ 𝕜'] (x : NNReal),
  ‖(algebraMap NNReal 𝕜') x‖ = ↑x
-- Lean.LibrarySuggestions.SineQuaNon
_private.Lean.LibrarySuggestions.SineQuaNon.0.Lean.LibrarySuggestions.SineQuaNon.sineQuaNonTriggersFor : Lean.Name → Lean.CoreM (List (Lean.Name × Float))
-- Mathlib.Tactic.SetNotationForOrder
/-- Whether to use set notation for the given type or not.  -/
_private.Mathlib.Tactic.SetNotationForOrder.0.Mathlib.Meta.SetNotationForOrder.useSetNotationFor : Lean.Expr → Lean.MetaM Bool
-- Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver
CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_α : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] (b : CategoryTheory.LocallyDiscrete Cᵒᵖ),
  ↑((J.pseudofunctorOver A).obj b) = CategoryTheory.Sheaf (J.over (Opposite.unop b.as)) A