mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.bot_toSubmonoid : ∀ {G : Type u_1} [inst : Group G], ⊥.toSubmonoid = ⊥
-- Mathlib.RingTheory.LocalRing.Basic
IsLocalRing.of_isUnit_or_isUnit_of_isUnit_add : ∀ {R : Type u_1} [inst : Semiring R] [Nontrivial R], (∀ (a b : R), IsUnit (a + b) → IsUnit a ∨ IsUnit b) → IsLocalRing R
-- Mathlib.Analysis.Normed.Module.Bases
/-- The coefficient satisfies `basisCoeff D n x • D.e n = (succSub D.P n) x`.  -/
SchauderBasis.RankOneDecomposition.basisCoeff_spec : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (D : SchauderBasis.RankOneDecomposition 𝕜 X) (n : ℕ) (x : X),
  D.basisCoeff n x • D.e n = (SchauderBasis.succSub D.P n) x
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If `ω ↦ exp (u * X ω)` is integrable at `u ≥ 0`, then it is integrable on `[0, u]`.  -/
ProbabilityTheory.integrable_exp_mul_of_nonneg_of_le : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t u : ℝ}
  [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.Integrable (fun ω => Real.exp (u * X ω)) μ →
    0 ≤ t → t ≤ u → MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.YonedaCollection.map₂_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F f ∘ CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F g
-- Mathlib.Order.Interval.Set.Image
StrictAnti.image_Ioc_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : PartialOrder α] [inst_1 : Preorder β] {a b : α},
  StrictAnti f → f '' Set.Ioc a b ⊆ Set.Ico (f b) (f a)
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- A choice of an index `i` such that `x` is in the range of `𝒰.f i`.  -/
AlgebraicGeometry.Scheme.Cover.idx : {K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme} →
  {X : AlgebraicGeometry.Scheme} →
    [AlgebraicGeometry.Scheme.JointlySurjective K] → (𝒰 : AlgebraicGeometry.Scheme.Cover K X) → ↥X → 𝒰.I₀
-- Mathlib.Topology.Order
/-- Topologies on `α` form a complete lattice, with `⊥` the discrete topology
and `⊤` the indiscrete topology. The infimum of a collection of topologies
is the topology generated by all their open sets, while the supremum is the
topology whose open sets are those sets open in every member of the collection.  -/
TopologicalSpace.instCompleteLattice : {α : Type u} → CompleteLattice (TopologicalSpace α)
-- Mathlib.Data.PFunctor.Univariate.M
/-- generates the approximations needed for `M.mk`  -/
PFunctor.M.Approx.sMk : {F : PFunctor.{uA, uB}} → ↑F F.M → (n : ℕ) → PFunctor.Approx.CofixA F n
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {km : α}, t.maxKey? = some km → t.getKey! km = km
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.inhabited_default : ∀ {V : Type u} {G : SimpleGraph V} [inst : Inhabited V], default = G.connectedComponentMk default
-- Mathlib.Order.RelIso.Basic
/-- **Alias** of `RelEmbedding.symm`. -/
RelEmbedding.isSymm : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [Std.Symm s], Std.Symm r
-- Mathlib.NumberTheory.ClassNumber.Finite
ClassGroup.finsetApprox.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra R S] {abv : AbsoluteValue R ℤ} {ι : Type u_5} {inst_4 : DecidableEq ι} [inst_5 : DecidableEq ι]
  [inst_6 : Fintype ι] (bS bS_1 : Module.Basis ι R S),
  bS = bS_1 →
    ∀ (adm adm_1 : abv.IsAdmissible),
      adm = adm_1 →
        ∀ [inst_7 : Infinite R] [inst_8 : DecidableEq R],
          ClassGroup.finsetApprox bS adm = ClassGroup.finsetApprox bS_1 adm_1
-- Mathlib.Order.Atoms
/-- **Alias** of the reverse direction of `isCoatom_compl`. -/
IsAtom.compl : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {a : α}, IsAtom a → IsCoatom aᶜ
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- The epimorphism `Z^{n₁}(f₁, f₂) ⟶ E^{n₁}(f₁, f₂, f₃)`.  -/
CategoryTheory.Abelian.SpectralObject.πE : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j k l : ι} →
              (f₁ : i ⟶ j) →
                (f₂ : j ⟶ k) →
                  (f₃ : k ⟶ l) →
                    (n₀ n₁ n₂ : ℤ) →
                      (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.πE._auto_1) →
                        (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.πE._auto_3) →
                          X.cycles f₁ f₂ n₁ ⟶ X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_insertMany_list_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List α}, (m.insertMany l).size ≤ m.size + l.length
-- Mathlib.Computability.Primrec.Basic
PrimrecPred.not : ∀ {α : Type u_1} [inst : Primcodable α] {p : α → Prop}, PrimrecPred p → PrimrecPred fun a => ¬p a
-- Mathlib.Algebra.Group.Submonoid.Saturation
/-- A saturated submonoid is a submonoid `s` that satisfies `x * y ∈ s → x ∈ s ∧ y ∈ s`.  -/
SaturatedSubmonoid : (M : Type u_1) → [MulOneClass M] → Type u_1
-- Lean.Elab.Term.TermElabM
/-- Snapshot just before execution of a tactic.  -/
Lean.Elab.Tactic.TacticParsedSnapshotInner : Type → Type
-- Mathlib.Logic.Function.Basic
/-- A set of functions "separates points"
if for each pair of distinct points there is a function taking different values on them.  -/
Set.SeparatesPoints : {α : Type u_3} → {β : Type u_4} → Set (α → β) → Prop
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.haarScalarFactor_eq_mul : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] (μ' μ ν : MeasureTheory.Measure G) [inst_5 : μ.IsHaarMeasure]
  [inst_6 : ν.IsHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_8 : μ'.IsMulLeftInvariant],
  μ'.haarScalarFactor ν = μ'.haarScalarFactor μ * μ.haarScalarFactor ν
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerLeft.inj : ∀ {e : Lean.Expr} {f g h : Mathlib.Tactic.BicategoryLike.Mor₁} {η : Mathlib.Tactic.BicategoryLike.Mor₂Iso}
  {e_1 : Lean.Expr} {f_1 g_1 h_1 : Mathlib.Tactic.BicategoryLike.Mor₁} {η_1 : Mathlib.Tactic.BicategoryLike.Mor₂Iso},
  Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerLeft e f g h η =
      Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerLeft e_1 f_1 g_1 h_1 η_1 →
    e = e_1 ∧ f = f_1 ∧ g = g_1 ∧ h = h_1 ∧ η = η_1
-- Mathlib.Computability.EpsilonNFA
εNFA.mem_evalFrom_iff_exists : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ) {s : σ} {S : Set σ} {x : List α},
  s ∈ M.evalFrom S x ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.ext : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α} {p' : ι' → Prop}
  {s' : ι' → Set α},
  l.HasBasis p s →
    l'.HasBasis p' s' →
      (∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i) → (∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i') → l = l'
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.AddContent.mk.inj : ∀ {α : Type u_1} {G : Type u_2} {inst : AddCommMonoid G} {C : Set (Set α)} {toFun : Set α → G} {empty' : toFun ∅ = 0}
  {sUnion' : ∀ (I : Finset (Set α)), ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → toFun (⋃₀ ↑I) = ∑ u ∈ I, toFun u}
  {toFun_1 : Set α → G} {empty'_1 : toFun_1 ∅ = 0}
  {sUnion'_1 :
    ∀ (I : Finset (Set α)), ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → toFun_1 (⋃₀ ↑I) = ∑ u ∈ I, toFun_1 u},
  { toFun := toFun, empty' := empty', sUnion' := sUnion' } =
      { toFun := toFun_1, empty' := empty'_1, sUnion' := sUnion'_1 } →
    toFun = toFun_1
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.Aesop.builder_option.quot : Lean.ParserDescr
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.lTensor_id : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) (N : Type u_8) [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N],
  LinearMap.lTensor M LinearMap.id = LinearMap.id
-- Init.Data.UInt.Lemmas
UInt64.toNat_mod_lt : ∀ {m : ℕ} (u : UInt64), 0 < m → (u % UInt64.ofNat m).toNat < m
-- Mathlib.Combinatorics.Matroid.Map
Matroid.mapEquiv_isBase_iff : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : α ≃ β} {B : Set β},
  (M.mapEquiv f).IsBase B ↔ M.IsBase (⇑f.symm '' B)
-- Std.Async.System
/-- The numeric group ID.
 -/
Std.Async.System.GroupId.toNat : Std.Async.System.GroupId → ℕ
-- Mathlib.Data.Part
Part.instZero : {α : Type u_1} → [Zero α] → Zero (Part α)
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Presentation.ofIsPresentation_toRelations : ∀ {A : Type u} [inst : Ring A] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module A M]
  {relations : Module.Relations A} {solution : relations.Solution M} (h : solution.IsPresentation),
  (Module.Presentation.ofIsPresentation h).toRelations = relations
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal
/-- If a real differentiable map `f` is conformal at a point `x`,
then it preserves the angles at that point.  -/
InnerProductGeometry.ConformalAt.preserves_angle : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : InnerProductSpace ℝ F] {f : E → F} {x : E} {f' : E →L[ℝ] F},
  HasFDerivAt f f' x →
    ConformalAt f x → ∀ (u v : E), InnerProductGeometry.angle (f' u) (f' v) = InnerProductGeometry.angle u v
-- Mathlib.Data.NNRat.Defs
NNRat.ext_num_den_iff : ∀ {p q : ℚ≥0}, p = q ↔ p.num = q.num ∧ p.den = q.den
-- Mathlib.Analysis.Calculus.MeanValue
/-- Variant of the mean value inequality on a convex set. Version with `fderivWithin`.  -/
Convex.norm_image_sub_le_of_norm_fderivWithin_le' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
  [inst_2 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → G} {C : ℝ} {s : Set E} {x y : E} {φ : E →L[𝕜] G},
  DifferentiableOn 𝕜 f s →
    (∀ x ∈ s, ‖fderivWithin 𝕜 f s x - φ‖ ≤ C) → Convex ℝ s → x ∈ s → y ∈ s → ‖f y - f x - φ (y - x)‖ ≤ C * ‖y - x‖
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.comp_of_aemeasurable : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] [inst_3 : MeasurableSpace δ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  {f : α → γ} {g : β → γ} {u : γ → δ},
  ProbabilityTheory.IdentDistrib f g μ ν →
    AEMeasurable u (MeasureTheory.Measure.map f μ) → ProbabilityTheory.IdentDistrib (u ∘ f) (u ∘ g) μ ν
-- Mathlib.Algebra.GroupWithZero.Units.Equiv
unitsEquivNeZero_symm_apply : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] (a : { a // a ≠ 0 }), unitsEquivNeZero.symm a = Units.mk0 ↑a ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.eval_polynomialX : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R),
  (MvPolynomial.eval P) W'.polynomialX = W'.a₁ * P 1 * P 2 - (3 * P 0 ^ 2 + 2 * W'.a₂ * P 0 * P 2 + W'.a₄ * P 2 ^ 2)
-- Mathlib.Order.WithBot
WithBot.ofDual_map : ∀ {α : Type u_1} {β : Type u_2} (f : αᵒᵈ → βᵒᵈ) (a : WithBot αᵒᵈ),
  WithBot.ofDual (WithBot.map f a) = WithTop.map (⇑OrderDual.ofDual ∘ f ∘ ⇑OrderDual.toDual) (WithBot.ofDual a)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
/-- A version of `pos_iff_ne_zero` for `WithZero` that only requires `LT α`,
not `PartialOrder α`.  -/
WithZero.pos_iff_ne_zero : ∀ {α : Type u_1} [inst : LT α] {x : WithZero α}, 0 < x ↔ x ≠ 0
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi'_pi : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [inst_2 : Encodable ι] [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  (s : (i : ι) → Set (α i)), (MeasureTheory.Measure.pi' μ) (Set.univ.pi s) = ∏ i, (μ i) (s i)
-- Lean.Elab.Match
Lean.Elab.Term.ElabMatchTypeAndDiscrsResult : Type
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda_app_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] (X : Cᵒᵖ) (F : CategoryTheory.Sheaf J (Type (max v v'))),
  (J.uliftYonedaOpCompCoyoneda.app X).app F = (J.uliftYonedaEquiv.trans Equiv.ulift.symm).toIso
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.hasFiniteColimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C],
  CategoryTheory.Limits.HasFiniteColimits C
-- Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart
/-- A C⋆-algebra is spanned by nonnegative elements of norm less than `r`.  -/
CStarAlgebra.span_nonneg_inter_ball : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {r : ℝ},
  0 < r → Submodule.span ℂ ({x | 0 ≤ x} ∩ Metric.ball 0 r) = ⊤
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.conjugate_embedding_injective : ∀ (K : Type u_1) [inst : Field K], Function.Injective fun v => NumberField.ComplexEmbedding.conjugate v.embedding
-- Mathlib.Algebra.Group.Basic
eq_zero_iff_eq_zero_of_add_eq_zero : ∀ {M : Type u_4} [inst : AddZeroClass M] {a b : M}, a + b = 0 → (a = 0 ↔ b = 0)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.toAddMonoidHom_injective : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N],
  Function.Injective AddSubmonoid.LocalizationMap.toAddMonoidHom
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.union_insert_right_equiv_insert_union : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  {p : (a : α) × β a} (h₁ : m₁.WF) (h₂ : m₂.WF),
  (m₁.union (Std.DTreeMap.Internal.Impl.insert p.fst p.snd m₂ ⋯).impl ⋯ ⋯).Equiv
    (Std.DTreeMap.Internal.Impl.insert p.fst p.snd (m₁.union m₂ ⋯ ⋯) ⋯).impl
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.isClosed_range_toBCF : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero β],
  IsClosed (Set.range ZeroAtInftyContinuousMap.toBCF)
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.unop_eq_top : ∀ {M : Type u_2} [inst : MulOneClass M] {S : Submonoid Mᵐᵒᵖ}, S.unop = ⊤ ↔ S = ⊤
-- Mathlib.Topology.MetricSpace.PiNat
/-- Homeomorphism between `X` and its embedding into `∀ i, Y i` induced by a separating family of
continuous functions `f i : X → Y i`.  -/
Metric.PiNatEmbed.toPiNatHomeo : {ι : Type u_2} →
  (X : Type u_3) →
    (Y : ι → Type u_4) →
      (f : (i : ι) → X → Y i) →
        [inst : Encodable ι] →
          [inst_1 : (i : ι) → MetricSpace (Y i)] →
            [inst_2 : TopologicalSpace X] →
              [CompactSpace X] →
                (∀ (i : ι), Continuous (f i)) → (Pairwise fun x y => ∃ i, f i x ≠ f i y) → X ≃ₜ Metric.PiNatEmbed X Y f
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.inv_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ⟶ Y) (Z : C) [inst_2 : CategoryTheory.IsIso f],
  CategoryTheory.inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.inv f) Z
-- Mathlib.Analysis.Convex.Quasiconvex
/-- A function is quasilinear if it is both quasiconvex and quasiconcave.
This means that, for all `r`,
the sets `{x ∈ s | f x ≤ r}` and `{x ∈ s | r ≤ f x}` are `𝕜`-convex.  -/
QuasilinearOn : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {β : Type u_3} → [Semiring 𝕜] → [PartialOrder 𝕜] → [AddCommMonoid E] → [LE β] → [SMul 𝕜 E] → Set E → (E → β) → Prop
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforward_obj_val : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) (M : SheafOfModules R),
  ((SheafOfModules.pushforward φ).obj M).val = (PresheafOfModules.pushforward φ.hom).obj M.val
-- Init.Data.SInt.Lemmas
Int16.toNatClampNeg_ofIntClamp_of_lt : ∀ {n : ℤ}, n < 2 ^ 15 → (Int16.ofIntClamp n).toNatClampNeg = n.toNat
-- Mathlib.GroupTheory.GroupAction.Transitive
AddAction.IsPretransitive.of_surjective_map : ∀ {M : Type u_3} {N : Type u_4} {α : Type u_5} {β : Type u_6} [inst : AddMonoid M] [inst_1 : AddMonoid N]
  [inst_2 : AddAction M α] [inst_3 : AddAction N β] {φ : M → N} {f : α →ₑ[φ] β},
  Function.Surjective ⇑f → AddAction.IsPretransitive M α → AddAction.IsPretransitive N β
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Morphisms of group objects preserve inverses.  -/
CategoryTheory.GrpObj.inv_hom : ∀ {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.GrpObj.inv f =
    CategoryTheory.CategoryStruct.comp f CategoryTheory.GrpObj.inv
-- Mathlib.Algebra.Category.Grp.Limits
/-- An auxiliary declaration to speed up typechecking.  -/
AddCommGrpCat.forget₂AddCommMon_preservesLimitsAux : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddCommGrpCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommGrpCat)).sections] →
        CategoryTheory.Limits.IsLimit
          ((CategoryTheory.forget₂ AddCommGrpCat AddCommMonCat).mapCone (AddCommGrpCat.limitCone F))
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.functorEnriched_assoc : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ F₃ F₄ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₂ F₃]
  [inst_7 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₃ F₄]
  [inst_8 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₃]
  [inst_9 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₂ F₄]
  [inst_10 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₄],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator
          (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂)
          (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₂ F₃)
          (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₃ F₄)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          (CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp V F₁ F₂ F₃)
          (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₃ F₄))
        (CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp V F₁ F₃ F₄)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
        (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂)
        (CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp V F₂ F₃ F₄))
      (CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp V F₁ F₂ F₄)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_zero : ∀ (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] (a : A), cfc 0 a = 0
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.Tree.macroExpansion.injEq : ∀ (macroName : Lean.Name) (stx stx' : Lean.Syntax) (nested : FBinopElab.Tree✝) (macroName_1 : Lean.Name)
  (stx_1 stx'_1 : Lean.Syntax) (nested_1 : FBinopElab.Tree✝),
  (FBinopElab.Tree.macroExpansion✝ macroName stx stx' nested =
      FBinopElab.Tree.macroExpansion✝ macroName_1 stx_1 stx'_1 nested_1) =
    (macroName = macroName_1 ∧ stx = stx_1 ∧ stx' = stx'_1 ∧ nested = nested_1)
-- Init.Data.List.Monadic
List.mapM_eq_reverse_foldlM_cons : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → m β} {l : List α},
  List.mapM f l = List.reverse <$> List.foldlM (fun acc a => (fun x => x :: acc) <$> f a) [] l
-- Mathlib.CategoryTheory.Retract
/-- The top of a retract diagram of morphisms determines a retract of objects.  -/
CategoryTheory.RetractArrow.left : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z W : C} → {f : X ⟶ Y} → {g : Z ⟶ W} → CategoryTheory.RetractArrow f g → CategoryTheory.Retract X Z
-- Lean.Server.Rpc.RequestHandling
Lean.Server.instInhabitedRpcProcedure.default : Lean.Server.RpcProcedure
-- Init.Data.Option.Lemmas
Option.not_rel_none_some : ∀ {α : Type u_1} {β : Type u_2} {a : β} {r : α → β → Prop}, ¬Option.Rel r none (some a)
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
/-- **Alias** of `ZetaAsymptotics.termTSum`.

---

Topological sum of `term`s.  -/
ZetaAsymptotics.term_tsum : ℝ → ℝ
-- Mathlib.LinearAlgebra.Projection
Submodule.prodEquivOfIsCompl_symm_apply_fst_eq_zero : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (p q : Submodule R E)
  (h : IsCompl p q) {x : E}, ((p.prodEquivOfIsCompl q h).symm x).1 = 0 ↔ x ∈ q
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.injective_πs : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] (o : Ordinal.{u}),
  Function.Injective ⇑(Profinite.NobelingProof.πs C o)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.ΓIso.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens),
  AlgebraicGeometry.IsOpenImmersion.ΓIso f U =
    (AlgebraicGeometry.Scheme.Hom.appIso f ((TopologicalSpace.Opens.map f.base).obj U)).symm ≪≫
      CategoryTheory.Functor.mapIso Y.presheaf (CategoryTheory.eqToIso ⋯).op
-- Mathlib.Analysis.Convex.Function
ConvexOn.add : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E]
  [inst_7 : DistribMulAction 𝕜 β] {s : Set E} {f g : E → β}, ConvexOn 𝕜 s f → ConvexOn 𝕜 s g → ConvexOn 𝕜 s (f + g)
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_le_subst_nonneg_cert : Int.Internal.Linear.Var → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Bool
-- Mathlib.Data.Fin.Tuple.Basic
Fin.append_cast_left : ∀ {α : Sort u_1} {n m : ℕ} (xs : Fin n → α) (ys : Fin m → α) (n' : ℕ) (h : n' = n),
  Fin.append (xs ∘ Fin.cast h) ys = Fin.append xs ys ∘ Fin.cast ⋯