mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.map_id_comp_H0Iso_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B),
  CategoryTheory.CategoryStruct.comp (groupCohomology.map (MonoidHom.id G) f 0) (groupCohomology.H0Iso B).hom =
    CategoryTheory.CategoryStruct.comp (groupCohomology.H0Iso A).hom ((Rep.invariantsFunctor k G).map f)
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.coe_eq_algebraMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜], ↑𝕜 = ⇑(algebraMap 𝕜 (DoubleCentralizer 𝕜 𝕜))
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.mergeWith : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ t₄ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF →
    t₂.WF →
      t₃.WF →
        t₄.WF →
          ∀ (f : (a : α) → β a → β a → β a),
            t₁.Equiv t₂ → t₃.Equiv t₄ → (Std.DTreeMap.Raw.mergeWith f t₁ t₃).Equiv (Std.DTreeMap.Raw.mergeWith f t₂ t₄)
-- Init.Grind.Norm
Lean.Grind.smul_nat_eq_mul : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (n : ℕ) (a : α), n • a = ↑n * a
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.basisDivisor_eq_zero_iff : ∀ {F : Type u_1} [inst : Field F] {x y : F}, Lagrange.basisDivisor x y = 0 ↔ x = y
-- Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory
CategoryTheory.ObjectProperty.instIsStableUnderShiftUnopIntOfOpposite : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (P : CategoryTheory.ObjectProperty Cᵒᵖ) [P.IsStableUnderShift ℤ], P.unop.IsStableUnderShift ℤ
-- Mathlib.Order.Max
IsMax.not_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, IsMax a → ¬a < b
-- Mathlib.NumberTheory.KummerDedekind
/-- The first half of the **Kummer-Dedekind Theorem**, stating that the prime
factors of `I*S` are in bijection with those of the minimal polynomial of the generator of `S`
over `R`, taken `mod I`.  -/
KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {x : S} →
            {I : Ideal R} →
              [IsDomain R] →
                [IsIntegrallyClosed R] →
                  [inst_5 : IsDedekindDomain S] →
                    [Module.IsTorsionFree R S] →
                      (hI : I.IsMaximal) →
                        I ≠ ⊥ →
                          Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤ →
                            IsIntegral R x →
                              ↑{J | J ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap R S) I)} ≃
                                ↑{d |
                                    d ∈
                                      UniqueFactorizationMonoid.normalizedFactors
                                        (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))}
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCoconeMapCocone.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {E : Type u₅}
  [inst_3 : CategoryTheory.Category.{v₅, u₅} E] {F : CategoryTheory.Functor J C} {H : CategoryTheory.Functor C D}
  {H' : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cocone F),
  CategoryTheory.Functor.mapCoconeMapCocone c =
    CategoryTheory.Limits.Cocone.extInv (CategoryTheory.Iso.refl (H'.mapCocone (H.mapCocone c)).pt) ⋯
-- Batteries.Data.List.Lemmas
List.idxOfNth_cons_of_beq : ∀ {α : Type u_1} {x : α} {xs : List α} {n : ℕ} {a : α} [inst : BEq α],
  (a == x) = true → List.idxOfNth x (a :: xs) n = if n = 0 then 0 else List.idxOfNth x xs (n - 1) + 1
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
/-- If each component of the counit is a split monomorphism, then the right adjoint is full.  -/
CategoryTheory.Adjunction.full_R_of_isSplitMono_counit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R)
  [∀ (X : D), CategoryTheory.IsSplitMono (h.counit.app X)], R.Full
-- Mathlib.MeasureTheory.VectorMeasure.WithDensityVec
MeasureTheory.VectorMeasure.withDensity_apply_univ : ∀ {X : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E} {B : E →L[ℝ] F →L[ℝ] G},
  (μ.withDensity f B) Set.univ = ∫ᵛ (x : X), f x ∂[B; μ]
-- Lean.Parser.Term
Lean.Parser.semicolonOrLinebreak.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.Sum.Basic
Sum.swap_inl : ∀ {α : Type u_1} {β : Type u_2} {x : α}, (Sum.inl x).swap = Sum.inr x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_of_mem_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, k ∈ t.toList → k ∈ t
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- Eigenvectors corresponding to distinct eigenvalues of a linear operator are linearly
independent. (Lemma 5.11 of [axler2024])

We use the eigenvalues as indexing set to ensure that there is only one eigenvector for each
eigenvalue in the image of `xs`.
See `Module.End.eigenvectors_linearIndependent'` for an indexed variant.  -/
Module.End.eigenvectors_linearIndependent : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] (f : Module.End R M) (μs : Set R) (xs : ↑μs → M),
  (∀ (μ : ↑μs), f.HasEigenvector (↑μ) (xs μ)) → LinearIndependent (ι := ↑μs) R xs
-- Mathlib.Order.FixedPoints
OrderHom.map_le_lfp : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {a : α}, a ≤ OrderHom.lfp f → f a ≤ OrderHom.lfp f
-- Mathlib.Algebra.Order.Group.Synonym
ofColex_sub : ∀ {α : Type u_1} [inst : Sub α] (a b : Colex α), ofColex (a - b) = ofColex a - ofColex b
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mk.sizeOf_spec : ∀ {X : Type u_3} [inst : MetricSpace X] [inst_1 : SizeOf X] (carrier : Set X) (packingRadius : NNReal)
  (packingRadius_pos : 0 < packingRadius) (isSeparated_packingRadius : Metric.IsSeparated (↑packingRadius) carrier)
  (coveringRadius : NNReal) (coveringRadius_pos : 0 < coveringRadius)
  (isCover_coveringRadius : Metric.IsCover coveringRadius Set.univ carrier),
  sizeOf
      { carrier := carrier, packingRadius := packingRadius, packingRadius_pos := packingRadius_pos,
        isSeparated_packingRadius := isSeparated_packingRadius, coveringRadius := coveringRadius,
        coveringRadius_pos := coveringRadius_pos, isCover_coveringRadius := isCover_coveringRadius } =
    1 + sizeOf packingRadius + sizeOf packingRadius_pos + sizeOf coveringRadius + sizeOf coveringRadius_pos
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Given `f : β → ℝ`, if `f` sends `{i | p i}` to a set of positive numbers
accumulating to zero, then `f i`-neighborhoods of the diagonal form a basis of `𝓤 α`.

For specific bases see `uniformity_basis_dist`, `uniformity_basis_dist_inv_nat_succ`,
and `uniformity_basis_dist_inv_nat_pos`.  -/
Metric.mk_uniformity_basis : ∀ {α : Type u} [inst : PseudoMetricSpace α] {β : Type u_3} {p : β → Prop} {f : β → ℝ},
  (∀ (i : β), p i → 0 < f i) →
    (∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε) → (uniformity α).HasBasis p fun i => {p | dist p.1 p.2 < f i}
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.IterM.step_takeWhileWithPostcondition.match_3.eq_1 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it' out h
-- Mathlib.Order.Filter.Ultrafilter.Defs
Filter.exists_ultrafilter_iff : ∀ {α : Type u} {f : Filter α}, (∃ u, ↑u ≤ f) ↔ f.NeBot
-- Mathlib.RingTheory.Ideal.Quotient.Index
Ideal.finite_quotient_pow : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R}, I.FG → ∀ [Finite (R ⧸ I)] (n : ℕ), Finite (R ⧸ I ^ n)
-- Mathlib.LinearAlgebra.Dimension.Finite
exists_mem_ne_zero_of_rank_pos : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Nontrivial R]
  {s : Submodule R M}, 0 < Module.rank R ↥s → ∃ b ∈ s, b ≠ 0
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isRevMatch_sliceFrom_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos p : s.Pos}
  {h : p ≤ pos},
  String.Slice.Pattern.Model.IsRevMatch pat (p.sliceFrom pos h) ↔ String.Slice.Pattern.Model.IsRevMatch pat pos
-- Mathlib.Topology.ContinuousMap.Basic
Topology.IsQuotientMap.lift.congr_simp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f f_1 : C(X, Y)} (e_f : f = f_1) (hf : Topology.IsQuotientMap ⇑f) (g g_1 : C(X, Z))
  (e_g : g = g_1) (h : Function.FactorsThrough ⇑g ⇑f), hf.lift g h = ⋯.lift g_1 ⋯
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.isoMk_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} (app : (X : Cᵒᵖ) → M₁.obj X ≅ M₂.obj X)
  (naturality :
    autoParam
      (∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp (M₁.map f)
            ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (app Y).hom) =
          CategoryTheory.CategoryStruct.comp (app X).hom (M₂.map f))
      PresheafOfModules.isoMk._auto_1)
  (X : Cᵒᵖ), (PresheafOfModules.isoMk app naturality).inv.app X = (app X).inv
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The Hausdorff edistance to the empty set is infinite.  -/
Metric.hausdorffEDist_empty : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α}, s.Nonempty → Metric.hausdorffEDist s ∅ = ⊤
-- Init.PropLemmas
exists_or_eq_right : ∀ {α : Sort u_1} (y : α) (p : α → Prop), ∃ x, p x ∨ x = y
-- Mathlib.Algebra.Group.Action.End
MulAut.applyMulDistribMulAction.eq_1 : ∀ {M : Type u_2} [inst : Monoid M],
  MulAut.applyMulDistribMulAction = { toMulAction := MulAut.applyMulAction, smul_one := ⋯, smul_mul := ⋯ }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKeyD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k fallback : α},
  (List.map Prod.fst l).contains k = false →
    (Std.DTreeMap.Const.insertMany t l).getKeyD k fallback = t.getKeyD k fallback
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.wordProd_singleton : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B),
  cs.wordProd [i] = cs.simple i
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRight_map_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} (r : R₁ ⟶ R₂)
  (hr :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom (r.app X.right)))
  {X Y : CategoryTheory.MorphismProperty.Comma L R₁ P Q W} (f : X ⟶ Y),
  ((CategoryTheory.MorphismProperty.Comma.mapRight L r hr).map f).left =
    (CategoryTheory.MorphismProperty.Comma.Hom.hom f).left
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherian R M]
  (f : Module.End R M) (μ : R) (k : ℕ∞), (f.genEigenspace μ) k ≤ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.SignedMeasure.toMeasureOfZeroLE_apply : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) {i j : Set α}
  (hi : MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i) (hi₁ : MeasurableSet i),
  MeasurableSet j → (s.toMeasureOfZeroLE i hi₁ hi) j = ↑(NNReal.mk (s (i ∩ j)) ⋯)
-- Mathlib.Topology.EMetricSpace.Defs
Subtype.image_closedEBall : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {p : α → Prop} (a : { a // p a }) (r : ENNReal),
  Subtype.val '' Metric.closedEBall a r = Metric.closedEBall (↑a) r ∩ {a | p a}
-- Mathlib.CategoryTheory.Monoidal.CommComon_
CategoryTheory.CommComon.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {A B : CategoryTheory.CommComon C} (f g : A ⟶ B),
  f.hom.hom = g.hom.hom → f = g
-- Mathlib.Topology.MetricSpace.Cover
/-- A set `N` is an *`ε`-cover* of a set `s` if every point of `s` lies at distance at most `ε` of
some point of `N`.

This is also called an *`ε`-net* in the literature.

[R. Vershynin, *High Dimensional Probability*][vershynin2018high], 4.2.1.  -/
Metric.IsCover : {X : Type u_1} → [PseudoEMetricSpace X] → NNReal → Set X → Set X → Prop
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instHashableCallHierarchyItem.hash : Lean.Lsp.CallHierarchyItem → UInt64
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Enriched.Functor.associator_inv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (K L M N : CategoryTheory.Functor C D) {X : C}
  (x :
    (CategoryTheory.MonoidalCategoryStruct.tensorObj (K.functorHom L)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj (L.functorHom M) (M.functorHom N))).obj
      X),
  (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.MonoidalCategoryStruct.associator
            ((K.homObjFunctor L).obj (Opposite.op (CategoryTheory.coyoneda.obj (Opposite.op X))))
            ((L.homObjFunctor M).obj (Opposite.op (CategoryTheory.coyoneda.obj (Opposite.op X))))
            ((M.homObjFunctor N).obj (Opposite.op (CategoryTheory.coyoneda.obj (Opposite.op X))))).inv)
      x =
    ((x.1, x.2.1), x.2.2)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
SummableLocallyUniformlyOn.mono : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β] {t : Set β},
  SummableLocallyUniformlyOn f t → s ⊆ t → SummableLocallyUniformlyOn f s
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.instAddCommGroup : {M : Type u_2} →
  {N : Type u_3} →
    {X : Type u_4} →
      {Y : Type u_5} →
        {σ : M → N} →
          [inst : SMul M X] → [inst_1 : AddCommGroup Y] → [inst_2 : DistribSMul N Y] → AddCommGroup (X →ₑ[σ] Y)
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
/-- If `0 → M → M' → M''` is an exact sequence, then the set of associated primes of `M'` is
contained in the union of those of `M` and `M''`.  -/
associatedPrimes.subset_union_of_exact : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_3}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] {f : M →ₗ[R] M'} {M'' : Type u_4} [inst_5 : AddCommMonoid M'']
  [inst_6 : Module R M''] {g : M' →ₗ[R] M''},
  Function.Injective ⇑f → Function.Exact ⇑f ⇑g → associatedPrimes R M' ⊆ associatedPrimes R M ∪ associatedPrimes R M''
-- Mathlib.FieldTheory.IsSepClosed
/-- If `E` is normal over `F`, then the separable closure of `F` in `E` is Galois (i.e.
normal and separable) over `F`.  -/
separableClosure.isGalois : ∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Normal F E],
  IsGalois F ↥(separableClosure F E)
-- Lean.Elab.PreDefinition.PartialFixpoint.Induction
_private.Lean.Elab.PreDefinition.PartialFixpoint.Induction.0.Lean.Elab.PartialFixpoint.deriveInduction : Lean.Name → Bool → Lean.MetaM Unit
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.δ_one_mkOfSucc : ∀ {n : ℕ} (i : Fin n),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.δ 1) (SimplexCategory.mkOfSucc i) =
    { len := 0 }.const { len := n } i.castSucc
-- Init.Data.SInt.Bitwise
Int32.toBitVec_and : ∀ (a b : Int32), (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
-- Lean.Linter.AmbiguousOpen
Lean.Linter.linter.ambiguousOpen : Lean.Option Bool
-- Plausible.Functions
Plausible.TotalFunction.PiUncurry.sampleableExt : {α : Type u} → {β : Type v} → {γ : Sort w} → [Plausible.SampleableExt (α × β → γ)] → Plausible.SampleableExt (α → β → γ)
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderConjugate.instTwoTwo : ENNReal.HolderConjugate 2 2
-- Init.Data.Nat.Lemmas
_private.Init.Data.Nat.Lemmas.0.Nat.allLTTR.eq_1 : ∀ (n : ℕ) (f : (i : ℕ) → i < n → Bool), n.allLTTR f = Nat.allLTTR.loop✝ n f n ⋯
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
/-- One can cut out `ℝ≥0∞` into the sets `{0}`, `Ico (t^n) (t^(n+1))` for `n : ℤ` and `{∞}`. This
gives a way to compute the measure of a set in terms of sets on which a given function `f` does not
fluctuate by more than `t`.  -/
measure_eq_measure_preimage_add_measure_tsum_Ico_zpow : ∀ {α : Type u_5} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ENNReal},
  Measurable f →
    ∀ {s : Set α},
      MeasurableSet s →
        ∀ {t : NNReal},
          1 < t →
            μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' {⊤}) + ∑' (n : ℤ), μ (s ∩ f ⁻¹' Set.Ico (↑t ^ n) (↑t ^ (n + 1)))
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.liftMagma_apply_apply : ∀ (R : Type u_1) {A : Type u_4} {M : Type u_7} [inst : Semiring R] [inst_1 : Add M]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : Module R A] [inst_4 : IsScalarTower R A A]
  [inst_5 : SMulCommClass R A A] (f : Multiplicative M →ₙ* A) (a : AddMonoidAlgebra R M),
  ((AddMonoidAlgebra.liftMagma R) f) a =
    (↑((Finsupp.liftAddHom fun x => (smulAddHom R A).flip (f (Multiplicative.ofAdd x))).comp
            AddMonoidAlgebra.coeffAddEquiv.toAddMonoidHom)).toFun
      a
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.toAdicCompletion_coe : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : Finite σ] (p : MvPolynomial σ R),
  (MvPowerSeries.toAdicCompletion σ R) ↑p = (AdicCompletion.of (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)) p
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.inl_pushoutLeftPushoutInrIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W)
  [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 : CategoryTheory.Limits.HasPushout (CategoryTheory.Limits.pushout.inr f g) g'],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f (CategoryTheory.CategoryStruct.comp g g'))
      (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g)
      (CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushout.inr f g) g')
-- Mathlib.CategoryTheory.Limits.Preorder
Preorder.limitConeOfIsGLB_cone : ∀ {C : Type u} [inst : Preorder C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} J]
  (F : CategoryTheory.Functor J C) {pt : C} (h : IsGLB (Set.range F.obj) pt),
  (Preorder.limitConeOfIsGLB F h).cone = Preorder.coneOfLowerBound F ⋯
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.IsLocallyDirected.instIsLocallyDirectedWidePushoutShapeCompForgetOfIsOpenImmersionMap : ∀ {J : Type w} (F : CategoryTheory.Functor (CategoryTheory.Limits.WidePushoutShape J) AlgebraicGeometry.Scheme)
  [∀ {i j : CategoryTheory.Limits.WidePushoutShape J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)],
  (F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ}, (Std.TreeMap.map f t).size = t.size
-- Mathlib.Analysis.Seminorm
/-- The image of a closed ball under addition with a singleton is another closed ball.  -/
Seminorm.vadd_closedBall : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] {x y : E}
  {r : ℝ} (p : Seminorm 𝕜 E), x +ᵥ p.closedBall y r = p.closedBall (x +ᵥ y) r
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Quiv.homEquivOfIso_apply : ∀ {V W : CategoryTheory.Quiv} (e : V ≅ W) {X Y : ↑V} (f : X ⟶ Y), (CategoryTheory.Quiv.homEquivOfIso e) f = e.hom.map f
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiffInv₀.of_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Inv G] [inst_7 : Zero G] {m n : WithTop ℕ∞},
  m ≤ n → ∀ [h : ContMDiffInv₀ I n G], ContMDiffInv₀ I m G
-- Mathlib.Algebra.BigOperators.Ring.Finset
/-- The product of `f a + g a` over all of `s` is the sum over the powerset of `s` of the product of
`f` over a subset `t` times the product of `g` over the complement of `t`  -/
Finset.prod_add : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] [inst_1 : DecidableEq ι] (f g : ι → R) (s : Finset ι),
  ∏ i ∈ s, (f i + g i) = ∑ t ∈ s.powerset, (∏ i ∈ t, f i) * ∏ i ∈ s \ t, g i
-- Mathlib.Data.NNReal.Basic
NNReal.iSup_mul_le : ∀ {ι : Sort u_3} {a : NNReal} {g : ι → NNReal} {h : NNReal}, (∀ (i : ι), g i * h ≤ a) → iSup g * h ≤ a
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charmatrix_ofNat : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (k : ℕ)
  [inst_3 : k.AtLeastTwo], (OfNat.ofNat k).charmatrix = Matrix.diagonal fun x => Polynomial.X - OfNat.ofNat k
-- Init.Data.SInt.Lemmas
ISize.ofIntLE_eq_ofIntClamp : ∀ {x : ℤ} {h₁ : ISize.minValue.toInt ≤ x} {h₂ : x ≤ ISize.maxValue.toInt}, ISize.ofIntLE x h₁ h₂ = ISize.ofIntClamp x
-- Mathlib.Topology.MetricSpace.ShrinkingLemma
/-- Let `R : α → ℝ` be a (possibly discontinuous) function on a proper metric space.
Let `s` be a closed set in `α` such that `R` is positive on `s`. Then there exists a collection of
pairs of balls `Metric.ball (c i) (r i)`, `Metric.ball (c i) (r' i)` such that

* all centers belong to `s`;
* for all `i` we have `0 < r i < r' i < R (c i)`;
* the family of balls `Metric.ball (c i) (r' i)` is locally finite;
* the balls `Metric.ball (c i) (r i)` cover `s`.

This is a simple corollary of `refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set`
and `exists_subset_iUnion_ball_radius_pos_lt`.  -/
exists_locallyFinite_subset_iUnion_ball_radius_lt : ∀ {α : Type u} [inst : MetricSpace α] [ProperSpace α] {s : Set α},
  IsClosed s →
    ∀ {R : α → ℝ},
      (∀ x ∈ s, 0 < R x) →
        ∃ ι c r r',
          (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
            (LocallyFinite fun i => Metric.ball (c i) (r' i)) ∧ s ⊆ ⋃ i, Metric.ball (c i) (r i)
-- Mathlib.Computability.Language
Language.reverse_pow : ∀ {α : Type u_1} (l : Language α) (n : ℕ), (l ^ n).reverse = l.reverse ^ n
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instLawfulEqOrdOffset : Std.LawfulEqOrd Std.Time.Nanosecond.Offset