mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionSemiHomClass.toMulDistribMulActionHom.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : Monoid A]
  [inst_3 : MulDistribMulAction M A] {B : Type u_5} [inst_4 : Monoid B] [inst_5 : MulDistribMulAction N B]
  {F : Type u_10} [inst_6 : FunLike F A B] [inst_7 : MulDistribMulActionSemiHomClass F (⇑φ) A B] (f : F),
  ↑f = { toFun := (↑↑f).toFun, map_smul' := ⋯, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.str : (self : MonCat) → Monoid ↑self
-- Mathlib.Data.Finset.Lattice.Fold
/-- **Alias** of the reverse direction of `Finset.le_inf_iff`. -/
Finset.le_inf : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} {f : β → α} {a : α},
  (∀ b ∈ s, a ≤ f b) → a ≤ s.inf f
-- Mathlib.Analysis.Meromorphic.Order
/-- If `g` is analytic at `x`, `f` is meromorphic at `g x`, and `g` is not locally constant near
`x`, the order of `f ∘ g` is the product of the orders of `f` and `g · - g x`.  -/
MeromorphicAt.meromorphicOrderAt_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E} {g : 𝕜 → 𝕜},
  MeromorphicAt f (g x) →
    AnalyticAt 𝕜 g x →
      ¬Filter.EventuallyConst g (nhds x) →
        meromorphicOrderAt (f ∘ g) x =
          meromorphicOrderAt f (g x) * ENat.map Nat.cast (analyticOrderAt (fun x_1 => g x_1 - g x) x)
-- Init.Data.Int.Order
_private.Init.Data.Int.Order.0.Int.sign.match_1.splitter : (motive : ℤ → Sort u_1) →
  (x : ℤ) →
    ((n : ℕ) → motive (Int.ofNat n.succ)) →
      (Unit → motive (Int.ofNat 0)) → ((a : ℕ) → motive (Int.negSucc a)) → motive x
-- Mathlib.Data.Set.Card
Set.ncard_graphOn : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) (f : α → β), (Set.graphOn f s).ncard = s.ncard
-- Mathlib.Topology.Category.Profinite.Extend
Profinite.instEpiAppDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceπAsLimitCone : ∀ (S : Profinite) (i : DiscreteQuotient ↑S.toTop), CategoryTheory.Epi (S.asLimitCone.π.app i)
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.QInfty_f_comp_PInfty_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (n : ℕ),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.QInfty.f n) (AlgebraicTopology.DoldKan.PInfty.f n) = 0
-- Mathlib.Topology.UniformSpace.AbstractCompletion
/-- The uniform isomorphism between two completions of isomorphic uniform spaces.  -/
AbstractCompletion.mapEquiv : {α : Type uα} →
  [inst : UniformSpace α] →
    (pkg : AbstractCompletion.{vα, uα} α) →
      {β : Type uβ} →
        [inst_1 : UniformSpace β] → (pkg' : AbstractCompletion.{vβ, uβ} β) → α ≃ᵤ β → pkg.space ≃ᵤ pkg'.space
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.currySumEquiv_apply : ∀ {R : Type uR} {ι : Type uι} {ι' : Type uι'} {M₂ : Type v₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : Module R M₂] {N : ι ⊕ ι' → Type u_1} [inst_3 : (i : ι ⊕ ι') → AddCommMonoid (N i)]
  [inst_4 : (i : ι ⊕ ι') → Module R (N i)] (f : MultilinearMap R N M₂), MultilinearMap.currySumEquiv f = f.currySum
-- Mathlib.LinearAlgebra.Basis.VectorSpace
Module.Basis.range_ofVectorSpace : ∀ (K : Type u_3) (V : Type u_4) [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  Set.range ⇑(Module.Basis.ofVectorSpace K V) = Module.Basis.ofVectorSpaceIndex K V
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.toList_ensureTermination : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [inst_2 : Std.Iterators.Finite α m] {it : Std.IterM m β}, it.ensureTermination.toList = it.toList
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.isBasis_sUnion : ∀ {α : Type u_1} {M : Matroid α} {I : Set α} {Xs : Set (Set α)},
  Xs.Nonempty → (∀ X ∈ Xs, M.IsBasis I X) → M.IsBasis I (⋃₀ Xs)
-- Mathlib.Combinatorics.Configuration
Configuration.ProjectivePlane.toHasLines : {P : Type u_1} →
  {L : Type u_2} → [inst : Membership P L] → [self : Configuration.ProjectivePlane P L] → Configuration.HasLines P L
-- Aesop.Forward.State
/-- There is exactly one queue for each slot.  -/
Aesop.ClusterState.slotQueues_size : ∀ (self : Aesop.ClusterState), self.slotQueues.size = self.slots.size
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.ofHom_X' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C) {X Y : C}
  (f : X ⟶ Y) [inst_1 : W.ContainsIdentities], (CategoryTheory.MorphismProperty.RightFraction.ofHom W f).X' = X
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.structureMapLM.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] (n : ℕ∞) {K : TopologicalSpace.Compacts E} (i : ℕ),
  ContDiffMapSupportedIn.structureMapLM 𝕜 n i =
    ContDiffMapSupportedIn.toBoundedContinuousFunctionLM 𝕜 ∘ₗ ContDiffMapSupportedIn.iteratedFDerivLM 𝕜 n 0 i
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.prod_empty : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B},
  HNNExtension.NormalWord.ReducedWord.prod φ HNNExtension.NormalWord.empty.toReducedWord = 1
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerve.σ_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} (i : Fin (n + 1))
  (x : CategoryTheory.ComposableArrows C n) (j : Fin (n + 2)),
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ (CategoryTheory.nerve C) i)) x).obj j =
    x.obj (i.predAbove j)
-- Mathlib.Analysis.Convex.Cone.Closure
/-- The closure of a pointed cone inside a topological space as a pointed cone. This
construction is mainly used for defining maps between proper cones.  -/
PointedCone.closure : {𝕜 : Type u_1} →
  [inst : Semiring 𝕜] →
    [inst_1 : PartialOrder 𝕜] →
      [inst_2 : IsOrderedRing 𝕜] →
        {E : Type u_2} →
          [inst_3 : AddCommMonoid E] →
            [inst_4 : TopologicalSpace E] →
              [ContinuousAdd E] → [inst_6 : Module 𝕜 E] → [ContinuousConstSMul 𝕜 E] → PointedCone 𝕜 E → PointedCone 𝕜 E
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.indepFun_div_right : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_10}
  {m : MeasurableSpace β} [inst : Div β] [MeasurableDiv₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iIndepFun f μ →
    (∀ (i : ι), Measurable (f i)) → ∀ (i j k : ι), i ≠ j → i ≠ k → ProbabilityTheory.IndepFun (f i) (f j / f k) μ
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
BoundedContinuousFunction.range_toLpHom : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E]
  [inst_3 : SecondCountableTopologyEither α E] [inst_4 : MeasureTheory.IsFiniteMeasure μ] [inst_5 : Fact (1 ≤ p)],
  (BoundedContinuousFunction.toLpHom p μ).range = MeasureTheory.Lp.boundedContinuousFunction E p μ
-- Batteries.Data.PairingHeap
/-- Amortized `O(log n)`. Remove the minimum element of the heap.  -/
Batteries.PairingHeapImp.Heap.tail : {α : Type u_1} → (α → α → Bool) → Batteries.PairingHeapImp.Heap α → Batteries.PairingHeapImp.Heap α
-- Mathlib.Data.List.Sections
List.mem_sections_length : ∀ {α : Type u_1} {L : List (List α)} {f : List α}, f ∈ L.sections → f.length = L.length
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.MethodsRef.toMethods.unsafe_impl_2 : Lean.Meta.Grind.MethodsRef → Lean.Meta.Grind.Methods
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.hausdorffEDist_le_of_mem_edist`.

---

Bounding the Hausdorff edistance by exhibiting, for any point in each set,
another point in the other set at controlled distance  -/
EMetric.hausdorffEdist_le_of_mem_edist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α} {r : ENNReal},
  (∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r) → (∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r) → Metric.hausdorffEDist s t ≤ r
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List (α × β)} {k : α},
      (List.map Prod.fst l).contains k = false →
        Std.DHashMap.Internal.Raw₀.Const.get? (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)) k =
          Std.DHashMap.Internal.Raw₀.Const.get? m k
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.det_nonsing_inv : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α),
  A⁻¹.det = Ring.inverse A.det
-- Std.Data.DTreeMap.Internal.Operations
/-- Iterate over `l` and erase all of its elements from `t`.  -/
Std.DTreeMap.Internal.Impl.eraseMany : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      {ρ : Type w} → [ForIn Id ρ α] → (t : Std.DTreeMap.Internal.Impl α β) → ρ → t.Balanced → t.IteratedErasureFrom
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- **Uniqueness of left-invariant measures**: In a second-countable locally compact additive group,
any σ-finite left-invariant measure is a scalar multiple of the additive Haar measure.
This is slightly weaker than assuming that `μ` is an additive Haar measure (in particular we don't
require `μ ≠ 0`).
See also `isAddLeftInvariant_eq_smul_of_regular`
for a statement not assuming second-countability.  -/
MeasureTheory.Measure.addHaarMeasure_unique : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [SecondCountableTopology G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SigmaFinite μ] [μ.IsAddLeftInvariant] (K₀ : TopologicalSpace.PositiveCompacts G),
  μ = μ ↑K₀ • MeasureTheory.Measure.addHaarMeasure K₀
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.isComplex_iff : ∀ {K : Type u_1} [inst : Field K] {w : NumberField.InfinitePlace K},
  w.IsComplex ↔ ¬NumberField.ComplexEmbedding.IsReal w.embedding
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.iterate_derivative_U_eval_one : ∀ {R : Type u_1} [inst : CommRing R] (n : ℤ) (k : ℕ),
  ↑(∏ l ∈ Finset.range k, (2 * l + 3)) * Polynomial.eval 1 ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.U R n)) =
    ↑(∏ l ∈ Finset.range k, ((n + 1) ^ 2 - (↑l + 1) ^ 2)) * (↑n + 1)
-- Mathlib.CategoryTheory.Bicategory.Free
/-- Auxiliary definition for `lift`.  -/
CategoryTheory.FreeBicategory.liftHom : {B : Type u₁} →
  [inst : Quiver B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.CategoryStruct.{v₂, u₂} C] →
        (F : B ⥤q C) → {a b : CategoryTheory.FreeBicategory B} → (a ⟶ b) → (F.obj a ⟶ F.obj b)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Polynomial.Chebyshev.leadingCoeff_le_of_forall_abs_le_one : ∀ {n : ℕ} {P : Polynomial ℝ},
  P.degree ≤ ↑n → (∀ x ∈ Set.Icc (-1) 1, |Polynomial.eval x P| ≤ 1) → P.leadingCoeff ≤ 2 ^ (n - 1)
-- Lean.Server.Requests
Lean.Server.RequestContext.hLog : Lean.Server.RequestContext → IO.FS.Stream
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.flip_support : ∀ {ι : 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} (b : P.Base),
  b.flip.support = b.support
-- Mathlib.Logic.Equiv.PartialEquiv
/-- The codomain of the partial equivalence.  -/
PartialEquiv.target : {α : Type u_5} → {β : Type u_6} → PartialEquiv α β → Set β
-- Mathlib.MeasureTheory.Integral.Average
/-- Average value of a function `f` w.r.t. the standard measure on a set `s`.

It is equal to `(volume.real s)⁻¹ * ∫ x, f x`, so it takes value zero `f` is not integrable on `s`
or if `s` has infinite measure. If `s` has measure `1`, then the average of any function is equal to
its integral.  -/
MeasureTheory.«term⨍_In_,_» : Lean.ParserDescr
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- If `g` is a topological embedding, then `f` is strongly measurable iff `g ∘ f` is.  -/
Embedding.comp_stronglyMeasurable_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [inst : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : TopologicalSpace γ] [TopologicalSpace.PseudoMetrizableSpace γ]
  {g : β → γ} {f : α → β},
  Topology.IsEmbedding g → ((MeasureTheory.StronglyMeasurable fun x => g (f x)) ↔ MeasureTheory.StronglyMeasurable f)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k k' : α} [hi : Inhabited (β k')] {f : β k → β k},
      (t.modify k f).get! k' =
        if heq : cmp k k' = Ordering.eq then (Option.map (cast ⋯) (Option.map f (t.get? k))).get! else t.get! k'
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
Lean.Meta.Grind.Arith.CommRing.mkBinHomoFn : {m : Type → Type} →
  [MonadLiftT Lean.MetaM m] →
    [Lean.MonadError m] →
      [Monad m] →
        [Lean.Meta.Sym.Arith.MonadCanon m] → Lean.Expr → Lean.Level → Lean.Name → Lean.Name → Lean.Expr → m Lean.Expr
-- Aesop.Tree.Traversal
Aesop.TreeRef.mvarCluster.injEq : ∀ (cref cref_1 : Aesop.MVarClusterRef),
  (Aesop.TreeRef.mvarCluster cref = Aesop.TreeRef.mvarCluster cref_1) = (cref = cref_1)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- Given `T : F →L[𝕜] F'`, `postcompCLM T` is the continuous `𝕜`-linear-map sending
`f : 𝓓^{n}_{K}(E, F)` to `T ∘ f` as an element of `𝓓^{n}_{K}(E, F')`.  -/
ContDiffMapSupportedIn.postcompCLM : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      {F' : Type u_4} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace ℝ E] →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace ℝ F] →
                  [inst_5 : NormedSpace 𝕜 F] →
                    [inst_6 : SMulCommClass ℝ 𝕜 F] →
                      [inst_7 : NormedAddCommGroup F'] →
                        [inst_8 : NormedSpace ℝ F'] →
                          [inst_9 : NormedSpace 𝕜 F'] →
                            [inst_10 : SMulCommClass ℝ 𝕜 F'] →
                              {n : ℕ∞} →
                                {K : TopologicalSpace.Compacts E} →
                                  [LinearMap.CompatibleSMul F F' ℝ 𝕜] →
                                    (F →L[𝕜] F') → ContDiffMapSupportedIn E F n K →L[𝕜] ContDiffMapSupportedIn E F' n K
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasFDerivAt_natCast : ∀ {𝕜 : 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] [inst_7 : NatCast F] (n : ℕ) (x : E), HasFDerivAt (↑n) 0 x
-- Mathlib.Topology.Algebra.UniformMulAction
smul_uniformity₀ : ∀ {M : Type v} {X : Type x} [inst : UniformSpace X] [inst_1 : GroupWithZero M] [inst_2 : MulAction M X]
  [UniformContinuousConstSMul M X] {c : M}, c ≠ 0 → c • uniformity X = uniformity X
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGT.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α)
  (x_3 : Std.DTreeMap.Internal.Impl.leaf.Ordered)
  (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, compare a k = Ordering.gt),
  Std.DTreeMap.Internal.Impl.getEntryGT k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim
-- Mathlib.NumberTheory.Dioph
/-- Local abbreviation for `Fin2.ofNat'`  -/
Dioph.«term&_» : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.inclusion_comp_assoc : ∀ {X : AlgebraicGeometry.Scheme} {I J K : X.IdealSheafData} (h₁ : I ≤ J) (h₂ : J ≤ K) {Z : AlgebraicGeometry.Scheme}
  (h : I.subscheme ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.inclusion h₂)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.inclusion h₁) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.inclusion ⋯) h
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- Scalar multiplication on `MvPowerSeries` is continuous.  -/
MvPowerSeries.WithPiTopology.instContinuousSMul : ∀ {σ : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] {S : Type u_3} [inst_1 : Semiring S]
  [inst_2 : TopologicalSpace S] [inst_3 : CommSemiring R] [inst_4 : Algebra R S] [ContinuousSMul R S],
  ContinuousSMul R (MvPowerSeries σ S)
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.comp_equiv : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → ∀ (e : ι' ≃ ι), l.HasBasis (p ∘ ⇑e) (s ∘ ⇑e)
-- Mathlib.Order.Filter.Ultrafilter.Defs
Filter.Iic_pure : ∀ {α : Type u} (a : α), Set.Iic (pure a) = {⊥, pure a}
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey!_le_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α}, k ∈ t → (cmp t.minKey! k).isLE = true
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
_private.Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality.0.AddChar.mkZModAux_injective : ∀ {ι : Type u_2} [inst : DecidableEq ι] {n : ι → ℕ} [inst_1 : ∀ (i : ι), NeZero (n i)],
  Function.Injective (AddChar.mkZModAux✝ n)
-- Mathlib.Topology.Constructible
IsRetrocompact.finsetInf' : ∀ {X : Type u_2} [inst : TopologicalSpace X] [T2Space X] {ι : Type u_4} {s : Finset ι} {hs : s.Nonempty}
  {t : ι → Set X}, (∀ i ∈ s, IsRetrocompact (t i)) → IsRetrocompact (s.inf' hs t)
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.presheafEquivOfIso_inverse_map_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H : X ≅ Y)
  {X_1 Y_1 : CategoryTheory.Functor (TopologicalSpace.Opens ↑Y)ᵒᵖ C} (α : X_1 ⟶ Y_1)
  (X_2 : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  ((TopCat.Presheaf.presheafEquivOfIso C H).inverse.map α).app X_2 =
    α.app (Opposite.op ((TopologicalSpace.Opens.map H.inv).obj (Opposite.unop X_2)))
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
/-- The diagram of the multicoequalizer of all pair of morphisms `g₁ g₂ : Y ⟶ step W Z` with
a `f : X ⟶ Y` satisfying `W` such that `f ≫ g₁ = f ≫ g₂`.  -/
CategoryTheory.OrthogonalReflection.D₂.multispanIndex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (Z : C) →
        [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] →
          [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] →
            [inst_3 : CategoryTheory.Limits.HasPushouts C] →
              CategoryTheory.Limits.MultispanIndex (CategoryTheory.OrthogonalReflection.D₂.multispanShape W Z) C
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.map_U : ∀ {R : Type u_1} {R' : Type u_2} [inst : CommRing R] [inst_1 : CommRing R'] (f : R →+* R') (n : ℤ),
  Polynomial.map f (Polynomial.Chebyshev.U R n) = Polynomial.Chebyshev.U R' n
-- Mathlib.Data.EReal.Operations
/-- `a ≤ -b` if and only if `b ≤ -a` on `EReal`.  -/
EReal.le_neg : ∀ {a b : EReal}, a ≤ -b ↔ b ≤ -a
-- Mathlib.Data.Int.Lemmas
Int.strictMonoOn_natAbs : StrictMonoOn Int.natAbs (Set.Ici 0)
-- Mathlib.Analysis.Normed.Field.Lemmas
/-- If `s` is a set disjoint from `𝓝 0`, then `fun x ↦ x⁻¹` is uniformly continuous on `s`.  -/
uniformContinuousOn_inv₀ : ∀ {α : Type u_1} [inst : NormedDivisionRing α] {s : Set α}, sᶜ ∈ nhds 0 → UniformContinuousOn Inv.inv s
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.symm_apply_apply : ∀ {𝕜 : 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₂] (e : P ≃ᵃⁱ[𝕜] P₂) (x : P), e.symm (e x) = x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.comp_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M X Y : C} [inst_2 : CategoryTheory.AddMonObj M] (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp f 0 = 0
-- Mathlib.CategoryTheory.Localization.HomEquiv
CategoryTheory.Localization.homEquiv_symm_apply : ∀ {C : Type u_1} {D₁ : Type u_5} {D₂ : Type u_6} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_5, u_5} D₁] [inst_2 : CategoryTheory.Category.{v_6, u_6} D₂]
  (W : CategoryTheory.MorphismProperty C) (L₁ : CategoryTheory.Functor C D₁) [inst_3 : L₁.IsLocalization W]
  (L₂ : CategoryTheory.Functor C D₂) [inst_4 : L₂.IsLocalization W] {X Y : C} (g : L₂.obj X ⟶ L₂.obj Y),
  (CategoryTheory.Localization.homEquiv W L₁ L₂).symm g = (CategoryTheory.Localization.homEquiv W L₂ L₁) g
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_support : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R), f.eraseLead.support = f.support.erase f.natDegree
-- Mathlib.Analysis.BoxIntegral.Basic
/-- Integral sum of `f` over a tagged prepartition `π` such that `π.Union = π₀.Union` tends to the
sum of integrals of `f` over the boxes of `π₀`.  -/
BoxIntegral.Integrable.tendsto_integralSum_sum_integral : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤}
  [CompleteSpace F],
  BoxIntegral.Integrable I l f vol →
    ∀ (π₀ : BoxIntegral.Prepartition I),
      Filter.Tendsto (BoxIntegral.integralSum f vol) (BoxIntegral.IntegrationParams.toFilteriUnion I π₀)
        (nhds (∑ J ∈ π₀.boxes, BoxIntegral.integral J l f vol))
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getKey_eq_getKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [instBEq : BEq α] [inst_2 : Std.LawfulBEqOrd α]
  {k : α} {t : Std.DTreeMap.Internal.Impl α β} {h : Std.DTreeMap.Internal.Impl.contains k t = true} (hto : t.Ordered),
  t.getKey k h = Std.Internal.List.getKey k t.toListModel ⋯
-- Init.System.IO
/-- Sets the heartbeat counter of the current thread to the given amount. This can be used to avoid
counting heartbeats of code whose execution time is non-deterministic.
 -/
IO.setNumHeartbeats : ℕ → BaseIO Unit
-- Mathlib.Data.Option.Basic
Option.some_eq_map_iff : ∀ {α : Type u_1} {β : Type u_2} {b : β} {x : Option α} {f : α → β}, some b = Option.map f x ↔ ∃ a, x = some a ∧ f a = b
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
IsCyclotomicExtension.Rat.mem_zpowers_galEquivZMod_of_mem_stabilizer : ∀ (n : ℕ) [inst : NeZero n] (K : Type u_1) [inst_1 : Field K] [inst_2 : NumberField K]
  [hK : IsCyclotomicExtension {n} ℚ K] (p : ℕ) [hp : Fact (Nat.Prime p)] (P : Ideal (NumberField.RingOfIntegers K))
  [P.IsMaximal] [P.LiesOver (Ideal.span {↑p})] (hn : p.Coprime n) {σ : Gal(K/ℚ)},
  σ ∈ MulAction.stabilizer Gal(K/ℚ) P →
    (IsCyclotomicExtension.Rat.galEquivZMod n K) σ ∈ Subgroup.zpowers (ZMod.unitOfCoprime p hn)
-- Mathlib.CategoryTheory.Limits.Preorder
/-- If a cocone is a colimit, its point is a lub.  -/
Preorder.isLUB_of_isColimit : ∀ {C : Type u} [inst : Preorder C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} J]
  (F : CategoryTheory.Functor J C) {c : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit c),
  IsLUB (Set.range F.obj) c.pt