mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [LawfulBEq α] {k : α}, k ∈ m.toList ↔ k ∈ m
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.strictPatternModel : ∀ {pat : String.Slice}, pat.isEmpty = false → String.Slice.Pattern.Model.StrictPatternModel pat
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.pos_add_limZero : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {f g : CauSeq α abs},
  f.Pos → g.LimZero → (f + g).Pos
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isLongestRevMatch_cast_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s t : String.Slice} (hst : s.copy = t.copy)
  {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatch pat (pos.cast hst) ↔ String.Slice.Pattern.Model.IsLongestRevMatch pat pos
-- Mathlib.Order.Interval.Finset.Defs
Finset.map_subtype_embedding_Ioo : ∀ {α : Type u_1} [inst : Preorder α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : LocallyFiniteOrder α]
  (a b : Subtype p),
  (∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x) →
    Finset.map (Function.Embedding.subtype p) (Finset.Ioo a b) = Finset.Ioo ↑a ↑b
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.H_map_twoδ₂Toδ₁_toCycles_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 j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) {Z : C} (h_1 : X.cycles f g n ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h))
      (CategoryTheory.CategoryStruct.comp (X.toCycles f g fg h n) h_1) =
    CategoryTheory.CategoryStruct.comp 0 h_1
-- Mathlib.NumberTheory.ModularForms.Cusps
/-- An arithmetic subgroup has finitely many cusp orbits.  -/
instFiniteCuspOrbitsOfIsArithmetic : ∀ (𝒢 : Subgroup (GL (Fin 2) ℝ)) [𝒢.IsArithmetic], Finite (CuspOrbits 𝒢)
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.IsCofiltered C],
  CategoryTheory.IsCofilteredOrEmpty C
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.maxEntry!.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Inhabited (α × β)],
  Std.DTreeMap.Internal.Impl.Const.maxEntry! Std.DTreeMap.Internal.Impl.leaf =
    panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.Const.maxEntry!" 839 13
      "Map is empty"
-- Mathlib.Analysis.Normed.Group.Defs
/-- A seminormed group is an additive group endowed with a norm for which `dist x y = ‖-x + y‖`
defines a pseudometric space structure.  -/
SeminormedAddGroup : Type u_8 → Type u_8
-- Mathlib.Data.List.Rotate
List.rotate'_nil : ∀ {α : Type u} (n : ℕ), [].rotate' n = []
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent.0.summable_cotTermUpperBound : ∀ (A B : ℝ) (hB : 0 < B) {k : ℕ}, 1 ≤ k → Summable fun a => cotTermUpperBound✝ k A B hB a
-- Batteries.Recycling.RBTree.Basic
/-- `O(1)` amortized, `O(log n)` worst case: Get the next element from the stream.  -/
RBTree.RBMap.Values.Stream.next? : {α : Type u} → {β : Type v} → RBTree.RBMap.Values.Stream α β → Option (β × RBTree.RBMap.Values.Stream α β)
-- Init.Data.Order.Ord
Std.instTransCmpCompareOnOfTransOrd : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Ord β] [Std.TransOrd β], Std.TransCmp (compareOn f)
-- Lean.Language.Basic
Lean.Language.SnapshotTreeTransform.mk.inj : ∀ {addTrailing addTrailing_1 : Substring.Raw},
  { addTrailing := addTrailing } = { addTrailing := addTrailing_1 } → addTrailing = addTrailing_1
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toList_filterMap : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → Option γ} (it : Std.IterM m β),
  (Std.IterM.filterMap f it).toList = (fun x => List.filterMap f x) <$> it.toList
-- Batteries.Data.List.Basic
/-- Right-biased version of `List.zip`. `zipRight' as bs` returns the list of
pairs `(aᵢ, bᵢ)` for `aᵢ ∈ as` and `bᵢ ∈ bs`. If `as` is shorter than `bs`, the
remaining `bᵢ` are paired with `none`. Also returns the remaining `as`.
```
zipRight' [1] ['a', 'b'] = ([(some 1, 'a'), (none, 'b')], [])
zipRight' [1, 2] ['a'] = ([(some 1, 'a')], [2])
zipRight' = zipWithRight' prod.mk
```
 -/
List.zipRight' : {α : Type u_1} → {β : Type u_2} → List α → List β → List (Option α × β) × List α
-- Init.Data.Option.Attach
Option.toList_pmap : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {o : Option α} {f : (a : α) → p a → β} (h : ∀ (a : α), o = some a → p a),
  (Option.pmap f o h).toList = List.map (fun x => f ↑x ⋯) o.attach.toList
-- Init.Data.UInt.Lemmas
USize.eq_sub_iff_add_eq : ∀ {a b c : USize}, a = c - b ↔ a + b = c
-- Mathlib.RingTheory.EssentialFiniteness
Algebra.EssFiniteType.aux : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T]
  (σ : Subalgebra R S),
  (∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ) →
    ∀ (τ : Set T),
      ∀ t ∈ Algebra.adjoin S τ,
        ∃ s ∈ σ, IsUnit s ∧ s • t ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ Algebra.adjoin R τ
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegralClosure.mk'_one : ∀ {R : Type u_1} (A : Type u_2) {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [inst_4 : Algebra A B] [inst_5 : IsIntegralClosure A R B] (h : optParam (IsIntegral R 1) ⋯),
  IsIntegralClosure.mk' A 1 h = 1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, (t₁ \ t₂).getKey? k = if k ∈ t₂ then none else t₁.getKey? k
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- A smooth function `f : M → N` induces a morphism of sheaves (of types) `𝒪_N ⟶ f_* 𝒪_M`
by pre-composing with `f`.  -/
ContMDiff.smoothSheafHom : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              {IM : ModelWithCorners 𝕜 EM HM} →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          {I : ModelWithCorners 𝕜 E H} →
                            {M : Type u} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace HM M] →
                                  {N : Type u} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace H N] →
                                        {EP : Type u_7} →
                                          [inst_11 : NormedAddCommGroup EP] →
                                            [inst_12 : NormedSpace 𝕜 EP] →
                                              {HP : Type u_8} →
                                                [inst_13 : TopologicalSpace HP] →
                                                  (IP : ModelWithCorners 𝕜 EP HP) →
                                                    (P : Type u) →
                                                      [inst_14 : TopologicalSpace P] →
                                                        [inst_15 : ChartedSpace HP P] →
                                                          (f : M → P) →
                                                            (hf : ContMDiff IM IP (↑⊤) f) →
                                                              smoothSheaf IP I P N ⟶
                                                                (TopCat.Sheaf.pushforward (Type u)
                                                                      (TopCat.ofHom
                                                                        { toFun := f, continuous_toFun := ⋯ })).obj
                                                                  (smoothSheaf IM I M N)
-- Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
/-- Given a tagged prepartition `π₁`, a prepartition `π₂` that covers exactly `I \ π₁.iUnion`, and
a function `r : ℝⁿ → (0, ∞)`, returns the union of `π₁` and `π₂.toSubordinate r`. This partition
`π` has the following properties:

* `π` is a partition, i.e. it covers the whole `I`;
* `π₁.boxes ⊆ π.boxes`;
* `π.tag J = π₁.tag J` whenever `J ∈ π₁`;
* `π` is Henstock outside of `π₁`: `π.tag J ∈ J.Icc` whenever `J ∈ π`, `J ∉ π₁`;
* `π` is subordinate to `r` outside of `π₁`;
* the distortion of `π` is equal to the maximum of the distortions of `π₁` and `π₂`.
 -/
BoxIntegral.TaggedPrepartition.unionComplToSubordinate : {ι : Type u_1} →
  [Fintype ι] →
    {I : BoxIntegral.Box ι} →
      (π₁ : BoxIntegral.TaggedPrepartition I) →
        (π₂ : BoxIntegral.Prepartition I) →
          π₂.iUnion = ↑I \ π₁.iUnion → ((ι → ℝ) → ↑(Set.Ioi 0)) → BoxIntegral.TaggedPrepartition I
-- Mathlib.Order.OmegaCompletePartialOrder
/-- Transfer an `OmegaCompletePartialOrder` on `β` to an `OmegaCompletePartialOrder` on `α`
using a strictly monotone function `f : β →o α`, a definition of ωSup and a proof that `f` is
continuous with regard to the provided `ωSup` and the ωCPO on `α`.  -/
OmegaCompletePartialOrder.lift : {α : Type u_2} →
  {β : Type u_3} →
    [inst : OmegaCompletePartialOrder α] →
      [inst_1 : PartialOrder β] →
        (f : β →o α) →
          (ωSup₀ : OmegaCompletePartialOrder.Chain β → β) →
            (∀ (x y : β), f x ≤ f y → x ≤ y) →
              (∀ (c : OmegaCompletePartialOrder.Chain β), f (ωSup₀ c) = OmegaCompletePartialOrder.ωSup (c.map f)) →
                OmegaCompletePartialOrder β
-- Mathlib.Logic.Encodable.Basic
/-- Constructively countable type. Made from an explicit injection `encode : α → ℕ` and a partial
inverse `decode : ℕ → Option α`. Note that finite types *are* countable. See `Denumerable` if you
wish to enforce infiniteness.  -/
Encodable : Type u_1 → Type u_1
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
QuasispectrumRestricts.cfcₙ_eq_restrict : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {p q : A → Prop} [inst : Semifield R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Field S]
  [inst_6 : StarRing S] [inst_7 : MetricSpace S] [inst_8 : IsTopologicalRing S] [inst_9 : ContinuousStar S]
  [inst_10 : NonUnitalRing A] [inst_11 : StarRing A] [inst_12 : Module S A] [inst_13 : IsScalarTower S A A]
  [inst_14 : SMulCommClass S A A] [inst_15 : Algebra R S] [inst_16 : Module R A] [IsScalarTower R S A] [StarModule R S]
  [ContinuousSMul R S] [inst_20 : TopologicalSpace A] [inst_21 : NonUnitalContinuousFunctionalCalculus S A q]
  [inst_22 : IsScalarTower R A A] [inst_23 : SMulCommClass R A A]
  [inst_24 : NonUnitalContinuousFunctionalCalculus R A p] [ContinuousMapZero.UniqueHom R A] (f : C(S, R)),
  Topology.IsClosedEmbedding ⇑(algebraMap R S) →
    ∀ {a : A},
      p a → q a → QuasispectrumRestricts a ⇑f → ∀ (g : R → R), cfcₙ g a = cfcₙ (fun x => (algebraMap R S) (g (f x))) a
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- If `i` is an isomorphism in `Comma L R`, it is also a morphism in `P.Comma L R Q W`.  -/
CategoryTheory.MorphismProperty.Comma.homFromCommaOfIsIso : {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} →
              {R : CategoryTheory.Functor B T} →
                {P : CategoryTheory.MorphismProperty T} →
                  {Q : CategoryTheory.MorphismProperty A} →
                    {W : CategoryTheory.MorphismProperty B} →
                      [inst_3 : Q.IsMultiplicative] →
                        [inst_4 : W.IsMultiplicative] →
                          [Q.RespectsIso] →
                            [W.RespectsIso] →
                              {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} →
                                (i : X.toComma ⟶ Y.toComma) → [CategoryTheory.IsIso i] → X ⟶ Y
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin_simple_le_iff : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {α : E}
  {K : IntermediateField F E}, F⟮α⟯ ≤ K ↔ α ∈ K
-- Mathlib.Analysis.Normed.Algebra.GelfandMazur
_private.Mathlib.Analysis.Normed.Algebra.GelfandMazur.0.NormedAlgebra.Real.aeval_eq_φ : ∀ {F : Type u_1} [inst : NormedRing F] [inst_1 : NormedAlgebra ℝ F] (x : F) (u : ℝ × ℝ),
  (Polynomial.aeval x) (Polynomial.X ^ 2 - Polynomial.C u.1 * Polynomial.X + Polynomial.C u.2) =
    NormedAlgebra.Real.φ✝ x u
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.equiv_iff_toList_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF → (t₁.Equiv t₂ ↔ Std.DTreeMap.Internal.Impl.Const.toList t₁ = Std.DTreeMap.Internal.Impl.Const.toList t₂)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.instInhabitedAngle : Inhabited Real.Angle
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.liftNatIso_inv : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : L.IsLocalization W] (F₁ F₂ : CategoryTheory.Functor C E) (F₁' F₂' : CategoryTheory.Functor D E)
  [h₁ : CategoryTheory.Localization.Lifting L W F₁ F₁'] [h₂ : CategoryTheory.Localization.Lifting L W F₂ F₂']
  (e : F₁ ≅ F₂),
  (CategoryTheory.Localization.liftNatIso L W F₁ F₂ F₁' F₂' e).inv =
    CategoryTheory.Localization.liftNatTrans L W F₂ F₁ F₂' F₁' e.inv
-- Init.Data.SInt.Bitwise
Int8.toUInt8_not : ∀ (a : Int8), (~~~a).toUInt8 = ~~~a.toUInt8
-- Init.Data.List.Int.Sum
List.mul_length_le_sum_of_min?_eq_some_int : ∀ {x : ℤ} {xs : List ℤ}, xs.min? = some x → x * ↑xs.length ≤ xs.sum
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.toSubalgebra_iSup_of_directed : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {ι : Type u_5}
  {t : ι → IntermediateField K L}, Directed (fun x1 x2 => x1 ≤ x2) t → (iSup t).toSubalgebra = ⨆ i, (t i).toSubalgebra
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.setMainModule.unsafe_1 : Lean.Environment → NonScalar
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.lapply_apply : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (a : α) (f : α →₀ M), (Finsupp.lapply a) f = f a
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
WithIdeal.mk : {R : Type u_2} → [inst : CommRing R] → Ideal R → WithIdeal R
-- Init.System.IO
IO.FS.instInhabitedStream.default : IO.FS.Stream
-- Mathlib.RingTheory.ClassGroup.ExtendedHom
/-- The monoid homomorphism `ClassGroup A → ClassGroup B` induced by an
injective extension of domains `A → B`.  -/
ClassGroup.extendedHom : (A : Type u_1) →
  (B : Type u_2) →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          [Module.IsTorsionFree A B] → [inst_4 : IsDomain A] → [inst_5 : IsDomain B] → ClassGroup A →* ClassGroup B
-- Mathlib.Algebra.Category.ModuleCat.Topology.Homology
TopModuleCat.instEpiCokerπ : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N),
  CategoryTheory.Epi (TopModuleCat.cokerπ φ)
-- Mathlib.SetTheory.ZFC.Basic
/-- A set function `f` is the image of `Definable.out f`.  -/
ZFSet.Definable.mk_out : ∀ {n : ℕ} {f : (Fin n → ZFSet.{u}) → ZFSet.{u}} [self : ZFSet.Definable n f] (xs : Fin n → PSet.{u}),
  ZFSet.mk (ZFSet.Definable.out f xs) = f fun x => ZFSet.mk (xs x)
-- Mathlib.NumberTheory.FLT.Three
/-- If there is a solution then there is a minimal one.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.exists_minimal : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ),
  ∃ S₁, FermatLastTheoremForThreeGen.Solution.isMinimal✝ S₁
-- Mathlib.Algebra.BigOperators.Ring.Finset
Finset.mul_sum : ∀ {ι : Type u_1} {R : Type u_4} [inst : NonUnitalNonAssocSemiring R] (s : Finset ι) (f : ι → R) (a : R),
  a * ∑ i ∈ s, f i = ∑ i ∈ s, a * f i
-- Mathlib.Analysis.Calculus.Deriv.Inv
HasDerivWithinAt.inv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_1}
  [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'} {c' : 𝕜'},
  HasDerivWithinAt c c' s x → c x ≠ 0 → HasDerivWithinAt c⁻¹ (-c' / c x ^ 2) s x
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoUniformlyOn.inv : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {f : ι → β → α} {g : β → α} {s : Set β}, TendstoUniformlyOn f g l s → TendstoUniformlyOn f⁻¹ g⁻¹ l s
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEFinStronglyMeasurable.const_smul : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
  {f : α → β} {𝕜 : Type u_5} [inst_1 : TopologicalSpace 𝕜] [inst_2 : Zero β] [inst_3 : SMulZeroClass 𝕜 β]
  [ContinuousSMul 𝕜 β],
  MeasureTheory.AEFinStronglyMeasurable f μ → ∀ (c : 𝕜), MeasureTheory.AEFinStronglyMeasurable (c • f) μ
-- Mathlib.RingTheory.Extension.Generators
/-- The canonical generators for `R` as an `R`-algebra.  -/
Algebra.Generators.id : {R : Type u} → [inst : CommRing R] → Algebra.Generators R R PEmpty.{w + 1}
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.Result'.isNegNat.sizeOf_spec : ∀ (inst lit proof : Lean.Expr),
  sizeOf (Mathlib.Meta.NormNum.Result'.isNegNat inst lit proof) = 1 + sizeOf inst + sizeOf lit + sizeOf proof
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isEmpty_alter_eq_isEmpty_erase : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} {f : Option β → Option β},
  (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.isEmpty =
    ((Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.isEmpty && (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isNone)
-- Lean.Meta.Basic
Lean.Meta.instInhabitedPostponedEntry : Inhabited Lean.Meta.PostponedEntry
-- Mathlib.MeasureTheory.Constructions.Pi
/-- We intentionally restrict this only to the nondependent function space, since type-class
inference cannot find an instance for `ι → ℝ` when this is stated for dependent function spaces.  -/
MeasureTheory.Pi.isMulLeftInvariant_volume : ∀ {ι : Type u_1} [inst : Fintype ι] {α : Type u_4} [inst_1 : Group α] [inst_2 : MeasureTheory.MeasureSpace α]
  [MeasureTheory.SigmaFinite MeasureTheory.volume] [MeasurableMul α] [MeasureTheory.volume.IsMulLeftInvariant],
  MeasureTheory.volume.IsMulLeftInvariant
-- Mathlib.Data.Part
Part.right_dom_of_div_dom : ∀ {α : Type u_1} [inst : Div α] {a b : Part α}, (a / b).Dom → b.Dom
-- Mathlib.Topology.Convenient.GeneratedBy
/-- Disjoint unions of `X`-generated spaces are `X`-generated.  -/
Sum.isGeneratedBy : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  {Z : Type v'} [inst_1 : TopologicalSpace Z] [Topology.IsGeneratedBy X Y] [Topology.IsGeneratedBy X Z],
  Topology.IsGeneratedBy X (Y ⊕ Z)
-- Mathlib.CategoryTheory.Abelian.Basic
/-- In an abelian category, any morphism that turns to zero when postcomposed with the cokernel of a
monomorphism factors through that monomorphism.  -/
CategoryTheory.Abelian.monoLift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          [CategoryTheory.Mono f] →
            {T : C} →
              (g : T ⟶ Y) → CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.cokernel.π f) = 0 → (T ⟶ X)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- If a type is infinitely upwardly enumerable, then every element has a successor.
 -/
Std.PRange.UpwardEnumerable.isSome_succ? : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.InfinitelyUpwardEnumerable α] {a : α},
  (Std.PRange.succ? a).isSome = true
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.setValue_eq_iff : ∀ {α : Sort u_1} {β : Sort u_2} (f : α ↪ β) {a a' : α} {b : β} [inst : (a' : α) → Decidable (a' = a)]
  [inst_1 : (a' : α) → Decidable (f a' = b)], (f.setValue a b) a' = b ↔ a' = a
-- Batteries.Data.List.Interleave
List.count_interleave : ∀ {α : Type u_1} [inst : BEq α] (l₁ l₂ : List α) (a : α),
  List.count a (l₁.interleave l₂) = List.count a l₁ + List.count a l₂
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The matrix associated to the adjoint of a linear map corresponding to two orthonormal bases
is the conjugate transpose of the matrix associated to the linear map.  -/
LinearMap.toMatrix_adjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F] {m : Type u_5}
  {n : Type u_6} [inst_5 : Fintype m] [inst_6 : DecidableEq m] [inst_7 : Fintype n] [inst_8 : DecidableEq n]
  [inst_9 : FiniteDimensional 𝕜 E] [inst_10 : FiniteDimensional 𝕜 F] (v₁ : OrthonormalBasis n 𝕜 E)
  (v₂ : OrthonormalBasis m 𝕜 F) (f : E →ₗ[𝕜] F),
  (LinearMap.toMatrix v₂.toBasis v₁.toBasis) (LinearMap.adjoint f) =
    ((LinearMap.toMatrix v₁.toBasis v₂.toBasis) f).conjTranspose
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
/-- Given a `ContinuousFunctionalCalculus S A q`. If we form the predicate `p` for `a : A`
characterized by: `q a` and the spectrum of `a` restricts to the scalar subring `R` via
`f : C(S, R)`, then we can get a restricted functional calculus
`ContinuousFunctionalCalculus R A p`.  -/
SpectrumRestricts.cfc : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {p q : A → Prop} [inst : Semifield R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Semifield S]
  [inst_6 : StarRing S] [inst_7 : MetricSpace S] [inst_8 : IsTopologicalSemiring S] [inst_9 : ContinuousStar S]
  [inst_10 : Ring A] [inst_11 : StarRing A] [inst_12 : Algebra S A] [inst_13 : Algebra R S] [inst_14 : Algebra R A]
  [IsScalarTower R S A] [StarModule R S] [ContinuousSMul R S] [inst_18 : TopologicalSpace A]
  [ContinuousFunctionalCalculus S A q] (f : C(S, R)),
  Topology.IsClosedEmbedding ⇑(algebraMap R S) →
    p 0 → (∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f) → ContinuousFunctionalCalculus R A p
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.evalOneₐ_surjective : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R), Function.Surjective ⇑(AdicCompletion.evalOneₐ I)
-- Mathlib.Data.Nat.Cast.Basic
Nat.coe_castRingHom : ∀ {α : Type u_1} [inst : NonAssocSemiring α], ⇑(Nat.castRingHom α) = Nat.cast
-- Mathlib.LinearAlgebra.AnnihilatingPolynomial
/-- `annIdealGenerator 𝕜 a` is indeed a generator.  -/
Polynomial.span_singleton_annIdealGenerator : ∀ (𝕜 : Type u_1) {A : Type u_2} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A),
  Ideal.span {Polynomial.annIdealGenerator 𝕜 a} = Polynomial.annIdeal 𝕜 a