mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.Measure.exists_eq_disjoint_finiteSpanningSetsIn : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν], ∃ S T, S.set = T.set ∧ Pairwise (Function.onFun Disjoint S.set)
-- Mathlib.Tactic.GRewrite.Core
/-- Given a proof of `a ~ b`, close a goal of the form `a ~' b` or `b ~' a`
for some possibly different relation `~'`.  -/
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.dischargeMain : Lean.Expr → Lean.MVarId → Lean.MetaM Bool
-- Mathlib.Topology.Order.OrderClosed
Ioo_mem_nhdsLT : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b : α},
  a < b → Set.Ioo a b ∈ nhdsWithin b (Set.Iio b)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
DifferentiableAt.smul : ∀ {𝕜 : 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] {f : E → F}
  {x : E} {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'},
  DifferentiableAt 𝕜 c x → DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 (c • f) x
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.instSubHom : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] → {c : ComplexShape ι} → {C D : HomologicalComplex V c} → Sub (C ⟶ D)
-- Lean.Meta.Tactic.Repeat
_private.Lean.Meta.Tactic.Repeat.0.Lean.Meta.repeat'Core.go.match_3.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.RingTheory.Finiteness.Basic
Submodule.fg_finset_sup : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_3}
  (s : Finset ι) (N : ι → Submodule R M), (∀ i ∈ s, (N i).FG) → (s.sup N).FG
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.linear_eq_linearIsometry : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[𝕜] P₂),
  f.linear = f.linearIsometry.toLinearMap
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.exists_bucket_of_uset : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α]
  (self : Array (Std.DHashMap.Internal.AssocList α β)) (i : USize) (hi : i.toNat < self.size)
  (d : Std.DHashMap.Internal.AssocList α β),
  ∃ l,
    (Std.DHashMap.Internal.toListModel self).Perm (self[i.toNat].toList ++ l) ∧
      (Std.DHashMap.Internal.toListModel (self.uset i d hi)).Perm (d.toList ++ l) ∧
        ∀ [LawfulHashable α],
          Std.DHashMap.Internal.IsHashSelf self →
            ∀ (k : α),
              (↑(Std.DHashMap.Internal.mkIdx self.size ⋯ (hash k))).toNat = i.toNat →
                Std.Internal.List.containsKey k l = false
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
PreQuasiregular.equiv_apply_val : ∀ {R : Type u_1} (val : R), (PreQuasiregular.equiv val).val = val
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
ProbabilityTheory.stdGaussian.eq_1 : ∀ (E : Type u_2) [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E],
  ProbabilityTheory.stdGaussian E =
    MeasureTheory.Measure.map (fun x => ∑ i, x i • (stdOrthonormalBasis ℝ E) i)
      (MeasureTheory.Measure.pi fun x => ProbabilityTheory.gaussianReal 0 1)
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- A specialized version of `UniformOnFun.uniformContinuous_ofFun_toFun` for convenience.  -/
UniformOnFun.uniformContinuous_ofFun_toFun_of_subset : ∀ {α : Type u_1} (β : Type u_2) [inst : UniformSpace β] (𝔖 𝔗 : Set (Set α)),
  𝔖 ⊆ 𝔗 → UniformContinuous (⇑(UniformOnFun.ofFun 𝔗) ∘ ⇑(UniformOnFun.toFun 𝔖))
-- Mathlib.RepresentationTheory.Rep.Basic
_private.Mathlib.RepresentationTheory.Rep.Basic.0.Rep.Hom.mk : {k : Type u} →
  {G : Type v} →
    [inst : Semiring k] → [inst_1 : Monoid G] → {A B : Rep.{w, u, v} k G} → A.ρ.IntertwiningMap B.ρ → A.Hom B
-- Mathlib.Analysis.Normed.Group.Ultra
/-- Generalised ultrametric triangle inequality for finite products in commutative groups with
an ultrametric norm.
 -/
IsUltrametricDist.norm_prod_le_of_forall_le_of_nonneg : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedCommGroup M] [IsUltrametricDist M] {s : Finset ι} {f : ι → M} {C : ℝ},
  0 ≤ C → (∀ i ∈ s, ‖f i‖ ≤ C) → ‖∏ i ∈ s, f i‖ ≤ C
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- The natural map `Mₛ →ₗ[R] Mₜ` if `s ≤ t` (in `Submonoid R`).  -/
IsLocalizedModule.liftOfLE : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {M₁ : Type u_6} →
            {M₂ : Type u_7} →
              [inst_3 : AddCommMonoid M₁] →
                [inst_4 : AddCommMonoid M₂] →
                  [inst_5 : Module R M₁] →
                    [inst_6 : Module R M₂] →
                      (S₁ S₂ : Submonoid R) →
                        S₁ ≤ S₂ →
                          (f₁ : M →ₗ[R] M₁) →
                            (f₂ : M →ₗ[R] M₂) → [IsLocalizedModule S₁ f₁] → [IsLocalizedModule S₂ f₂] → M₁ →ₗ[R] M₂
-- Mathlib.Algebra.Order.Round
round_le : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (x : α)
  (z : ℤ), |x - ↑(round x)| ≤ |x - ↑z|
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.PolarizationIn.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_5)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : FaithfulSMul S R] [inst_8 : Module S M]
  [inst_9 : IsScalarTower S R M] [inst_10 : Module S N] [inst_11 : P.IsValuedIn S] [inst_12 : Fintype ι],
  P.PolarizationIn S = ∑ i, LinearMap.toSpanSingleton S N (P.coroot i) ∘ₗ P.coroot'In S i
-- Mathlib.Data.FunLike.IsApply
FunLike.coe_vadd : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : VAdd M F]
  [inst_2 : VAdd M β] [IsVAddApply M F α β] (n : M) (f : F), ⇑(n +ᵥ f) = n +ᵥ ⇑f
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
countablyGenerated_of_standardBorel : ∀ {α : Type u_1} [inst : MeasurableSpace α] [StandardBorelSpace α], MeasurableSpace.CountablyGenerated α
-- Mathlib.Topology.Order.Rolle
/-- A continuous function on a closed interval with `f a = f b`
has a local extremum at some point of the corresponding open interval.  -/
exists_isLocalExtr_Ioo : ∀ {X : Type u_1} {Y : Type u_2} [inst : ConditionallyCompleteLinearOrder X] [DenselyOrdered X]
  [inst_2 : TopologicalSpace X] [OrderTopology X] [inst_4 : LinearOrder Y] [inst_5 : TopologicalSpace Y]
  [OrderTopology Y] {f : X → Y} {a b : X},
  a < b → ContinuousOn f (Set.Icc a b) → f a = f b → ∃ c ∈ Set.Ioo a b, IsLocalExtr f c
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.MkPreResultResult.success.injEq : ∀ (mvarsToCheckType instMVars mvarsToCheckType_1 instMVars_1 : Array Lean.MVarId),
  (Lean.Meta.Sym.MkPreResultResult.success✝ mvarsToCheckType instMVars =
      Lean.Meta.Sym.MkPreResultResult.success✝ mvarsToCheckType_1 instMVars_1) =
    (mvarsToCheckType = mvarsToCheckType_1 ∧ instMVars = instMVars_1)
-- Mathlib.Topology.Separation.Hausdorff
isOpen_iff_ultrafilter' : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] [CompactSpace X] (U : Set X),
  IsOpen U ↔ ∀ (F : Ultrafilter X), F.lim ∈ U → U ∈ ↑F
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
/-- Given `X : DerivedCategory C` and `n : ℤ`, this property means
that `X` is `≤ n` for the canonical t-structure.  -/
DerivedCategory.IsLE : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → [inst_2 : HasDerivedCategory C] → DerivedCategory C → ℤ → Prop
-- Init.Core
Not.imp : ∀ {a b : Prop}, ¬b → (a → b) → ¬a
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_const_mul_left_iff' : ∀ {α : Type u_1} {F : Type u_4} {R : Type u_13} [inst : Norm F] [inst_1 : SeminormedRing R] {g : α → F} {l : Filter α}
  {f : α → R} {c : R}, IsUnit c → ((fun x => c * f x) =o[l] g ↔ f =o[l] g)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.natEnd.eq_3 : ∀ (x : Turing.PartrecToTM2.Γ'),
  (x = Turing.PartrecToTM2.Γ'.consₗ → False) →
    (x = Turing.PartrecToTM2.Γ'.cons → False) → Turing.PartrecToTM2.natEnd x = false
-- Mathlib.CategoryTheory.Limits.Constructions.Equalizers
/-- A functor that preserves pushouts and binary coproducts also preserves coequalizers.  -/
CategoryTheory.Limits.preservesCoequalizers_of_preservesPushouts_and_binaryCoproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasPushouts C]
  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) G]
  [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan G],
  CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair G
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
/-- **Alias** of `Order.exists_cof_eq`.

---

Every well-order has a cofinal subset of cardinal `cof α`.  -/
Order.cof_eq : ∀ (α : Type u) [inst : Preorder α], ∃ s, IsCofinal s ∧ Cardinal.mk ↑s = Order.cof α
-- Mathlib.Order.SuccPred.Basic
Order.le_pred_iff : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a b : α} [NoMinOrder α], b ≤ Order.pred a ↔ b < a
-- Mathlib.CategoryTheory.Adjunction.CompositionIso
CategoryTheory.Adjunction.leftAdjointCompNatTrans.eq_1 : ∀ {C₀ : Type u_1} {C₁ : Type u_2} {C₂ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₀]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₁] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₂]
  {F₀₁ : CategoryTheory.Functor C₀ C₁} {F₁₂ : CategoryTheory.Functor C₁ C₂} {F₀₂ : CategoryTheory.Functor C₀ C₂}
  {G₁₀ : CategoryTheory.Functor C₁ C₀} {G₂₁ : CategoryTheory.Functor C₂ C₁} {G₂₀ : CategoryTheory.Functor C₂ C₀}
  (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₂ : F₁₂ ⊣ G₂₁) (adj₀₂ : F₀₂ ⊣ G₂₀) (τ₀₁₂ : G₂₀ ⟶ G₂₁.comp G₁₀),
  adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ τ₀₁₂ = (CategoryTheory.conjugateEquiv adj₀₂ (adj₀₁.comp adj₁₂)).symm τ₀₁₂
-- Mathlib.Topology.Algebra.TopologicallyNilpotent
/-- If `a` and `b` commute and `a` is topologically nilpotent,
then `a * b` is topologically nilpotent.  -/
IsTopologicallyNilpotent.mul_right_of_commute : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : Ring R] [IsLinearTopology Rᵐᵒᵖ R] {a b : R},
  IsTopologicallyNilpotent a → Commute a b → IsTopologicallyNilpotent (a * b)
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.IterM.step_intermediateZip.match_3.eq_2 : ∀ {α₁ β₁ : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α₁ m β₁]
  (motive : Option { out // ∃ it, it.IsPlausibleOutput out } → Sort u_3)
  (out₁ : { out // ∃ it, it.IsPlausibleOutput out }) (h_1 : Unit → motive none)
  (h_2 : (out₁ : { out // ∃ it, it.IsPlausibleOutput out }) → motive (some out₁)),
  (match some out₁ with
    | none => h_1 ()
    | some out₁ => h_2 out₁) =
    h_2 out₁
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.comp_toLRSHom : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z),
  AlgebraicGeometry.Scheme.Hom.toLRSHom (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toLRSHom f)
      (AlgebraicGeometry.Scheme.Hom.toLRSHom g)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableAtFilter.eq_1 : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε]
  (f : α → ε) (l : Filter α) (μ : MeasureTheory.Measure α),
  MeasureTheory.IntegrableAtFilter f l μ = ∃ s ∈ l, MeasureTheory.IntegrableOn f s μ
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.map_snd_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y Z : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct W X]
  [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.InformationTheory.KullbackLeibler.ChainRule
/-- Chain rule for the integral of the log-likelihood ratio, under absolute continuity and
integrability assumptions.  -/
InformationTheory.integral_llr_compProd_eq_add : ∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : MeasureTheory.Measure 𝓧}
  {κ η : ProbabilityTheory.Kernel 𝓧 𝓨} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν]
  [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η],
  (μ.compProd κ).AbsolutelyContinuous (ν.compProd η) →
    MeasureTheory.Integrable (MeasureTheory.llr (μ.compProd κ) (ν.compProd η)) (μ.compProd κ) →
      ∫ (p : 𝓧 × 𝓨), MeasureTheory.llr (μ.compProd κ) (ν.compProd η) p ∂μ.compProd κ =
        ∫ (a : 𝓧), MeasureTheory.llr μ ν a ∂μ +
          ∫ (p : 𝓧 × 𝓨), MeasureTheory.llr (μ.compProd κ) (μ.compProd η) p ∂μ.compProd κ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMon.go.eq_def : ∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon) (a : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.mulMon.go k m a =
    match a with
    | Lean.Grind.CommRing.Poly.num k' =>
      bif k' == 0 then Lean.Grind.CommRing.Poly.num 0
      else Lean.Grind.CommRing.Poly.add (k * k') m (Lean.Grind.CommRing.Poly.num 0)
    | Lean.Grind.CommRing.Poly.add k' m' p =>
      Lean.Grind.CommRing.Poly.add (k * k') (m.mul m') (Lean.Grind.CommRing.Poly.mulMon.go k m p)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.unbot_one : ∀ {α : Type u} [inst : One α], WithBot.unbot 1 ⋯ = 1
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
Real.posLog_zero : Real.posLog 0 = 0
-- Mathlib.Topology.Semicontinuity.Defs
/-- A real function `f` is lower semicontinuous on a set `s` if, for any `ε > 0`, for any `x ∈ s`,
for all `x'` close enough to `x` in `s`, then `f x'` is at least `f x - ε`. We formulate this in
a general preordered space, using an arbitrary `y < f x` instead of `f x - ε`.  -/
LowerSemicontinuousOn : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → [Preorder β] → (α → β) → Set α → Prop
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
add_neg_le_neg_add_iff : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] {a b c d : α} [AddRightMono α],
  a + -b ≤ -d + c ↔ d + a ≤ c + b
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.map_mono : ∀ {α : Type u_1} {β : Type u_3} (f : α → β), Monotone ⇑(MeasureTheory.OuterMeasure.map f)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Notation for `actionObj`, the action of `C` on `D`.  -/
CategoryTheory.MonoidalCategory.MonoidalRightAction.«term_⊙ᵣ_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.instZero : {E : Type u_2} →
  {F : Type u_3} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] →
          [inst_3 : NormedSpace ℝ F] →
            {n : ℕ∞} → {K : TopologicalSpace.Compacts E} → Zero (ContDiffMapSupportedIn E F n K)
-- Mathlib.Data.List.Intervals
List.Ico.filter_lt_of_le_bot : ∀ {n m l : ℕ}, l ≤ n → List.filter (fun x => decide (x < l)) (List.Ico n m) = []
-- Lean.Elab.ConfigEval.Basic
/-- Drops the first component of the `optionName`, returning the new config item.
The first component is stored at the front of `prevOptionComps`.
 -/
Lean.Elab.ConfigEval.ConfigItem.shift : Lean.Elab.ConfigEval.ConfigItem → Lean.Elab.ConfigEval.ConfigItem
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Set.Finite.summable : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {s : Set β},
  s.Finite → ∀ (f : β → α), Summable (f ∘ Subtype.val)
-- Init.Data.BitVec.Lemmas
/-- The sign extension is the same as zero extending when `msb = false`.  -/
BitVec.signExtend_eq_setWidth_of_msb_false : ∀ {w : ℕ} {x : BitVec w} {v : ℕ}, x.msb = false → BitVec.signExtend v x = BitVec.setWidth v x
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivWithinAt.union : ∀ {𝕜 : 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 t : Set E},
  HasFDerivWithinAt f f' s x → HasFDerivWithinAt f f' t x → HasFDerivWithinAt f f' (s ∪ t) x
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.eq_σ_comp_of_not_injective' : ∀ {n : ℕ} {Δ' : SimplexCategory} (θ : { len := n + 1 } ⟶ Δ') (i : Fin (n + 1)),
  (SimplexCategory.Hom.toOrderHom θ) i.castSucc = (SimplexCategory.Hom.toOrderHom θ) i.succ →
    ∃ θ', θ = CategoryTheory.CategoryStruct.comp (SimplexCategory.σ i) θ'
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {R₁ R₂ : CategoryTheory.CommRingObjCat C} {f g : R₁ ⟶ R₂},
  f.hom = g.hom → f = g
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_findGreatest' : ∀ {α : Type u_1} {mα : MeasurableSpace α} {p : α → ℕ → Prop} [inst : (x : α) → DecidablePred (p x)] {N : ℕ},
  (∀ k ≤ N, MeasurableSet {x | Nat.findGreatest (p x) N = k}) → Measurable fun x => Nat.findGreatest (p x) N
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- The underlying set of a `SubAddAction`.  -/
SubAddAction.carrier : {R : Type u} → {M : Type v} → [inst : VAdd R M] → SubAddAction R M → Set M
-- Mathlib.CategoryTheory.Sites.Point.Conservative
CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointlyReflectIsomorphisms_type : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {P : CategoryTheory.ObjectProperty J.Point},
  P.IsConservativeFamilyOfPoints → CategoryTheory.JointlyReflectIsomorphisms fun Φ => Φ.obj.sheafFiber
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.whiskeringRightCompEvaluation_hom_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor B C) (a : A)
  (X : CategoryTheory.Functor A B),
  (CategoryTheory.whiskeringRightCompEvaluation F a).hom.app X = CategoryTheory.CategoryStruct.id (F.obj (X.obj a))
-- Mathlib.Algebra.Algebra.Bilinear
Algebra.lmul_injective : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Function.Injective ⇑(Algebra.lmul R A)
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveElabStep3.mk.inj : ∀ {finalize finalize_1 : Lean.Elab.TermElabM Unit},
  { finalize := finalize } = { finalize := finalize_1 } → finalize = finalize_1
-- Mathlib.Data.Setoid.Partition
/-- membership invariance for `some`  -/
IndexedPartition.some_mem : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (self : IndexedPartition s) (i : ι), self.some i ∈ s i
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.bucket_eq : ∀ {α : Type u} {β : α → Type v} [inst : Hashable α] (self : Array (Std.DHashMap.Internal.AssocList α β))
  (h : 0 < self.size) (k : α),
  Std.DHashMap.Internal.bucket self h k = self[↑(Std.DHashMap.Internal.mkIdx self.size h (hash k))]
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
/-- Auxiliary lemma showing that for any `k : ℤ` and `(a : Fin 2 → ℤ)`
the extension of `eisSummand` is differentiable on `{z : ℂ | 0 < z.im}`.  -/
EisensteinSeries.eisSummand_extension_differentiableOn : ∀ (k : ℤ) (a : Fin 2 → ℤ),
  DifferentiableOn ℂ (EisensteinSeries.eisSummand k a ∘ ↑UpperHalfPlane.ofComplex) {z | 0 < z.im}
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.preimage_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X Y Z : C} (f : F.obj X ⟶ F.obj Y) (g : F.obj Y ⟶ F.obj Z)
  {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (hF.preimage (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (hF.preimage f) (CategoryTheory.CategoryStruct.comp (hF.preimage g) h)
-- Mathlib.Topology.Order
coinduced_id : ∀ {α : Type u_1} [t : TopologicalSpace α], TopologicalSpace.coinduced id t = t
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.top_toAddSubmonoid : ∀ {G : Type u_1} [inst : AddGroup G], ⊤.toAddSubmonoid = ⊤
-- Mathlib.RingTheory.Unramified.Basic
Algebra.FormallyUnramified.inst : ∀ {R : Type u} [inst : CommRing R], Algebra.FormallyUnramified R R
-- Init.Control.Basic
instMonadControlTOfPure : (m : Type u → Type v) → [Pure m] → MonadControlT m m
-- Mathlib.GroupTheory.GroupAction.Basic
/-- The action of an additive group on an orbit is transitive.  -/
AddAction.instIsPretransitiveElemOrbit : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (a : α),
  AddAction.IsPretransitive G ↑(AddAction.orbit G a)
-- Mathlib.MeasureTheory.Measure.Prod
/-- A measure on a product space equals the product measure of sigma-finite measures if they are
equal on rectangles.  -/
MeasureTheory.Measure.prod_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  [MeasureTheory.SigmaFinite μ] {ν : MeasureTheory.Measure β} [MeasureTheory.SigmaFinite ν]
  {μν : MeasureTheory.Measure (α × β)},
  (∀ (s : Set α) (t : Set β), MeasurableSet s → MeasurableSet t → μν (s ×ˢ t) = μ s * ν t) → μ.prod ν = μν
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Iio_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a : α} (b : ↑(Set.Iio a)), Subtype.val '' Set.Iic b = Set.Iic ↑b
-- Lean.Data.Lsp.Basic
/-- A change to a file resource.

[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#resourceChanges)  -/
Lean.Lsp.DocumentChange : Type
-- Mathlib.Data.Nat.Bitwise
Nat.exists_most_significant_bit : ∀ {n : ℕ}, n ≠ 0 → ∃ i, n.testBit i = true ∧ ∀ (j : ℕ), i < j → n.testBit j = false
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.πE_d_ιE_assoc : ∀ {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₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (n₀ n₁ n₂ n₃ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.πE_d_ιE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.πE_d_ιE._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.πE_d_ιE._auto_5) {Z : C}
  (h : X.opcycles f₂ f₃ n₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.πE f₃ f₄ f₅ n₀ n₁ n₂ hn₁ hn₂)
      (CategoryTheory.CategoryStruct.comp (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃)
        (CategoryTheory.CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃) h)) =
    CategoryTheory.CategoryStruct.comp (X.Ψ f₂ f₃ f₄ n₁ n₂ hn₂) h