mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Units.chartAt_apply : ∀ {R : Type u_1} [inst : NormedRing R] [inst_1 : CompleteSpace R] {a b : Rˣ}, ↑(chartAt R a) b = ↑b
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- `AlgHom` version of `Ideal.Quotient.factor`.  -/
Ideal.Quotient.factorₐ : (R₁ : Type u_1) →
  {A : Type u_3} →
    [inst : CommSemiring R₁] →
      [inst_1 : Ring A] →
        [inst_2 : Algebra R₁ A] →
          {I J : Ideal A} → [inst_3 : I.IsTwoSided] → [inst_4 : J.IsTwoSided] → I ≤ J → A ⧸ I →ₐ[R₁] A ⧸ J
-- Mathlib.RingTheory.UniqueFactorizationDomain.Nat
Nat.instWfDvdMonoid : WfDvdMonoid ℕ
-- Mathlib.Data.Sum.Basic
Sum.sum_rec_congr : ∀ {α : Type u} {β : Type v} (P : α ⊕ β → Sort u_3) (f : (i : α) → P (Sum.inl i)) (g : (i : β) → P (Sum.inr i))
  {x y : α ⊕ β} (h : x = y), Sum.rec f g x = cast ⋯ (Sum.rec f g y)
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientAddGroup.isOpenMap_coe : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] {N : AddSubgroup G},
  IsOpenMap QuotientAddGroup.mk
-- Mathlib.Topology.Algebra.Group.Defs
ContinuousWithinAt.fun_neg : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Neg G]
  [ContinuousNeg G] {f : X → G} {s : Set X} {x : X}, ContinuousWithinAt f s x → ContinuousWithinAt (fun i => -f i) s x
-- Mathlib.Order.Filter.Pointwise
Filter.neg_le_self : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {f : Filter α}, -f ≤ f ↔ -f = f
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_erase_le : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, (m.erase k).size ≤ m.size
-- Init.Data.SInt.Bitwise
Int16.and_zero : ∀ {a : Int16}, a &&& 0 = 0
-- Mathlib.Algebra.Ring.Defs
CommSemiring.toCommMonoidWithZero : {α : Type u} → [CommSemiring α] → CommMonoidWithZero α
-- Mathlib.RingTheory.Polynomial.Bernstein
/-- `bernsteinPolynomial R n ν` is `(choose n ν) * X^ν * (1 - X)^(n - ν)`.

Although the coefficients are integers, it is convenient to work over an arbitrary commutative ring.
 -/
bernsteinPolynomial : (R : Type u_1) → [inst : CommRing R] → ℕ → ℕ → Polynomial R
-- Mathlib.Topology.FiberBundle.Basic
FiberPrebundle.mk.sizeOf_spec : ∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : (x : B) → TopologicalSpace (E x)] [inst_3 : SizeOf B] [inst_4 : SizeOf F] [inst_5 : (a : B) → SizeOf (E a)]
  (pretrivializationAtlas : Set (Bundle.Pretrivialization F Bundle.TotalSpace.proj))
  (pretrivializationAt : B → Bundle.Pretrivialization F Bundle.TotalSpace.proj)
  (mem_base_pretrivializationAt : ∀ (x : B), x ∈ (pretrivializationAt x).baseSet)
  (pretrivialization_mem_atlas : ∀ (x : B), pretrivializationAt x ∈ pretrivializationAtlas)
  (continuous_trivChange :
    ∀ e ∈ pretrivializationAtlas,
      ∀ e' ∈ pretrivializationAtlas, ContinuousOn (↑e ∘ ↑e'.symm) (e'.target ∩ ↑e'.symm ⁻¹' e.source))
  (totalSpaceMk_isInducing : ∀ (b : B), Topology.IsInducing (↑(pretrivializationAt b) ∘ Bundle.TotalSpace.mk b)),
  sizeOf
      { pretrivializationAtlas := pretrivializationAtlas, pretrivializationAt := pretrivializationAt,
        mem_base_pretrivializationAt := mem_base_pretrivializationAt,
        pretrivialization_mem_atlas := pretrivialization_mem_atlas, continuous_trivChange := continuous_trivChange,
        totalSpaceMk_isInducing := totalSpaceMk_isInducing } =
    1
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
SSet.N.monoOfLE_refl : ∀ {X : SSet} [inst : X.Nonsingular] (x : X.N), SSet.N.monoOfLE ⋯ = CategoryTheory.CategoryStruct.id { len := x.dim }
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.coeff_expand_mul : ∀ {R : Type u} [inst : CommSemiring R] {p : ℕ},
  0 < p → ∀ (f : Polynomial R) (n : ℕ), ((Polynomial.expand R p) f).coeff (n * p) = f.coeff n
-- Mathlib.CategoryTheory.LiftingProperties.Adjunction
/-- A (left) adjoint square has a lifting if and only if the original square has a lifting.  -/
CategoryTheory.CommSq.left_adjoint_hasLift_iff : ∀ {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] {G : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C}
  {A B : C} {X Y : D} {i : B ⟶ A} {p : Y ⟶ X} {u : X ⟶ G.obj A} {v : Y ⟶ G.obj B}
  (sq : CategoryTheory.CommSq v p (G.map i) u) (adj : F ⊣ G), ⋯.HasLift ↔ sq.HasLift
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.involutiveInv : {α : Type u} → [InvolutiveNeg α] → InvolutiveInv (Multiplicative α)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.IsLeftAdjoint.nonempty : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {a b : B} {left : a ⟶ b}
  [self : CategoryTheory.Bicategory.IsLeftAdjoint left], Nonempty (CategoryTheory.Bicategory.RightAdjoint left)
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.inv_hom_apply : ∀ {X Y : Semigrp} (e : X ≅ Y) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Init.WF
/-- Helper gadget that prevents reduction of `Nat.eager n` unless `n` evaluates to a ground term.  -/
WellFounded.Nat.eager : ℕ → ℕ
-- Mathlib.Computability.EpsilonNFA
εNFA.mk.sizeOf_spec : ∀ {α : Type u} {σ : Type v} [inst : SizeOf α] [inst_1 : SizeOf σ] (step : σ → Option α → Set σ) (start accept : Set σ),
  sizeOf { step := step, start := start, accept := accept } = 1
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.center_eq_bot_of_subsingleton : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] [Subsingleton n],
  Subgroup.center (Matrix.SpecialLinearGroup n R) = ⊥
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_alter_le_size : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)}, (t.alter k f).size ≤ t.size + 1
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAtOfComplement.equiv.congr_simp : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G]
  {I I_1 : ModelWithCorners 𝕜 E H} (e_I : I = I_1) {J J_1 : ModelWithCorners 𝕜 E'' G} (e_J : J = J_1) {M : Type u_11}
  {N : Type u_13} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N]
  [inst_12 : ChartedSpace G N] {n n_1 : WithTop ℕ∞} (e_n : n = n_1) {f f_1 : M → N} (e_f : f = f_1) {x x_1 : M}
  (e_x : x = x_1) (h : Manifold.IsSubmersionAtOfComplement F I J n f x), h.equiv = ⋯.equiv
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.ne_startPos_of_lt : ∀ {s : String.Slice} {p q : s.Pos}, p < q → q ≠ s.startPos
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnriched.id_hComp_heq : ∀ {C : Type u_1} [inst : CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {a b : CategoryTheory.CatEnriched C}
  {f f' : a ⟶ b} (η : f ⟶ f'),
  CategoryTheory.CatEnriched.hComp (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id a)) η ≍ η
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
/-- Process a specified range of pending entries.
returns the computed values and pending nodes.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.processPending : {α : Type} →
  Array (Lean.Meta.RefinedDiscrTree.LazyEntry × α) →
    ℕ → ℕ → Lean.MetaM (Array α × Array (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry × α))
-- Std.Sync.Channel
/-- This type represents all flavors of channels that we have available.
 -/
Std.CloseableChannel.Flavors : Type → Type
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.insert_eq_insert : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] {p : (a : α) × β a},
  insert p m = m.insert p.fst p.snd
-- Mathlib.Topology.MetricSpace.PiNat
/-- If `X` is compact, and there exists a sequence of continuous functions `f i : X → Y i` to
metric spaces `Y i` that separate points on `X`, then `X` is metrizable.  -/
Metric.PiNatEmbed.TopologicalSpace.MetrizableSpace.of_countable_separating : ∀ {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} [Encodable ι] [inst : (i : ι) → MetricSpace (Y i)]
  [inst_1 : TopologicalSpace X] [CompactSpace X] (f : (i : ι) → X → Y i),
  (∀ (i : ι), Continuous (f i)) → (Pairwise fun x y => ∃ i, f i x ≠ f i y) → TopologicalSpace.MetrizableSpace X
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
DifferentiableWithinAt.log : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E},
  DifferentiableWithinAt ℝ f s x → f x ≠ 0 → DifferentiableWithinAt ℝ (fun x => Real.log (f x)) s x
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Entry.ref.injEq : ∀ {α : Type u} {β : Type v} {σ : Type w} (node node_1 : σ),
  (Lean.PersistentHashMap.Entry.ref node = Lean.PersistentHashMap.Entry.ref node_1) = (node = node_1)
-- Mathlib.Algebra.Order.Monoid.Lex
/-- Given ordered additive monoids M, N, the natural inclusion
ordered homomorphism from M to the lexicographic M ×ₗ N.  -/
OrderAddMonoidHom.inlₗ : (α : Type u_1) →
  (β : Type u_2) →
    [inst : AddMonoid α] →
      [inst_1 : PartialOrder α] → [inst_2 : AddMonoid β] → [inst_3 : Preorder β] → α →+o Lex (α × β)
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianReal_map_linearMap : ∀ {μ : ℝ} {v : NNReal} (L : ℝ →ₗ[ℝ] ℝ),
  MeasureTheory.Measure.map (⇑L) (ProbabilityTheory.gaussianReal μ v) =
    ProbabilityTheory.gaussianReal (L μ) ((L 1 ^ 2).toNNReal * v)
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.trace_conjTranspose_mul_self_eq_zero_iff : ∀ {m : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : Fintype m] {R : Type u_5} [inst_2 : PartialOrder R]
  [inst_3 : NonUnitalRing R] [inst_4 : StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {A : Matrix m n R},
  (A.conjTranspose * A).trace = 0 ↔ A = 0
-- Init.Data.Nat.Lemmas
Nat.sub_sub_eq_min : ∀ (a b : ℕ), a - (a - b) = min a b
-- Mathlib.Algebra.Symmetrized
SymAlg.invOf_sym : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : AddMonoidWithOne α] [inst_2 : Invertible 2] (a : α) [inst_3 : Invertible a],
  ⅟(SymAlg.sym a) = SymAlg.sym ⅟a
-- Mathlib.Data.List.Sublists
List.sublists'_sublist_sublists'_iff : ∀ {α : Type u} {l₁ l₂ : List α}, l₁.sublists'.Sublist l₂.sublists' ↔ l₁.Sublist l₂
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.instIsTopologicalAddGroup : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞}, IsTopologicalAddGroup (TestFunction Ω F n)
-- Mathlib.Tactic.Positivity.Basic
Mathlib.Meta.Positivity.min_ne : ∀ {R : Type u_2} [inst : LinearOrder R] {a b c : R}, a ≠ c → b ≠ c → min a b ≠ c
-- Mathlib.Order.Filter.CountableSeparatingOn
HasCountableSeparatingOn.mk : ∀ {α : Type u_1} {p : Set α → Prop} {t : Set α},
  (∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y) →
    HasCountableSeparatingOn α p t
-- Mathlib.InformationTheory.Coding.UniquelyDecodable
/-- If a code is uniquely decodable, it does not contain the empty string.

The empty string can be "decoded" as either zero or two copies of itself,
violating unique decodability.  -/
InformationTheory.UniquelyDecodable.epsilon_not_mem : ∀ {α : Type u_1} {S : Set (List α)}, InformationTheory.UniquelyDecodable S → [] ∉ S
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.map_isAddRegular : ∀ {M : Type u_1} {N : Type u_2} [inst : AddCommMonoid M] {S : AddSubmonoid M} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) {m : M}, IsAddRegular m → IsAddRegular (f m)
-- Mathlib.CategoryTheory.Adjunction.Lifting.Left
/-- To show that `ε_X` is a coequalizer for `(FUε_X, ε_FUX)`, it suffices to assume it's always a
coequalizer of something (i.e. a regular epi).
 -/
CategoryTheory.LiftLeftAdjoint.counitCoequalises : {B : Type u₂} →
  {C : Type u₃} →
    [inst : CategoryTheory.Category.{v₂, u₂} B] →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {U : CategoryTheory.Functor B C} →
          {F : CategoryTheory.Functor C B} →
            (adj₁ : F ⊣ U) →
              ((X : B) → CategoryTheory.RegularEpi (adj₁.counit.app X)) →
                (X : B) → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ (adj₁.counit.app X) ⋯)
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- The main loop of `isMVarSwap`. Returning `none` corresponds to a failure.  -/
_private.Mathlib.Tactic.ClickSuggestions.FindPremises.0.Mathlib.Tactic.ClickSuggestions.isMVarSwap.go : Lean.Expr → Lean.Expr → List (Lean.MVarId × Lean.MVarId) → Option (List (Lean.MVarId × Lean.MVarId))
-- Init.Data.SInt.Lemmas
Int16.toISize_toInt64 : ∀ (n : Int16), n.toInt64.toISize = n.toISize
-- Mathlib.Order.SetAccumulate
Set.accumulate_bot : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] (s : α → Set β), Set.accumulate s ⊥ = s ⊥
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.toAddSubmonoid_inj : ∀ {G : Type u_1} [inst : AddGroup G] {p q : AddSubgroup G}, p.toAddSubmonoid = q.toAddSubmonoid ↔ p = q
-- Mathlib.Order.Filter.Basic
Filter.principal_univ : ∀ {α : Type u}, Filter.principal Set.univ = ⊤
-- Mathlib.FieldTheory.KummerExtension
rootOfSplitsXPowSubC.congr_simp : ∀ {K : Type u} [inst : Field K] {n n_1 : ℕ} (e_n : n = n_1) (hn : 0 < n) (a a_1 : K) (e_a : a = a_1) (L : Type u_2)
  [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)],
  rootOfSplitsXPowSubC hn a L = rootOfSplitsXPowSubC ⋯ a_1 L
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `true` is `e` is the root of its congruence class.  -/
Lean.Meta.Grind.isCongrRoot : Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.Analysis.MeanInequalities
/-- **Hölder inequality**: the scalar product of two functions is bounded by the product of their
`L^p` and `L^q` norms when `p` and `q` are conjugate exponents. A version for `NNReal`-valued
functions. For an alternative version, convenient if the infinite sums are already expressed as
`p`-th powers, see `inner_le_Lp_mul_Lq_hasSum`.  -/
NNReal.summable_and_inner_le_Lp_mul_Lq_tsum : ∀ {ι : Type u} {f g : ι → NNReal} {p q : ℝ},
  p.HolderConjugate q →
    (Summable fun i => f i ^ p) →
      (Summable fun i => g i ^ q) →
        (Summable fun i => f i * g i) ∧
          ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
-- Init.Data.List.Nat.TakeDrop
List.lt_length_drop : ∀ {α : Type u_1} {xs : List α} {i j : ℕ}, i + j < xs.length → j < (List.drop i xs).length
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.containsThenInsert_snd : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.containsThenInsert k v).2 = t.insert k v
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.germ_restrictStalkNatIso_inv_app : ∀ {X Y : AlgebraicGeometry.Scheme} {U : X.Opens} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (x : ↥X)
  (M : Y.Modules) (hxU : x ∈ U),
  CategoryTheory.CategoryStruct.comp
      (M.presheaf.germ ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj (Opposite.unop (Opposite.op U))) (f x) ⋯)
      ((AlgebraicGeometry.Scheme.Modules.restrictStalkNatIso f x).inv.app M) =
    ((AlgebraicGeometry.Scheme.Modules.restrictFunctor f).obj M).presheaf.germ U x hxU
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.All.lowerBound?_lb : ∀ {α : Type u_1} {p : α → Prop} {lb : Option α} {cut : α → Ordering} {x : α} {t : RBTree.RBNode α},
  RBTree.RBNode.All p t → (∀ {x : α}, lb = some x → p x) → RBTree.RBNode.lowerBound? cut t lb = some x → p x
-- Mathlib.Tactic.FunProp.Mor
/-- Weak normal head form of an expression involving morphism applications.

For example calling this on `coe (f a) b` will put `f` in weak normal head form instead of `coe`.
 -/
Mathlib.Meta.FunProp.Mor.whnf : Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.Nat.Coprime
Nat.instDecidableCoprime : (m n : ℕ) → Decidable (m.Coprime n)
-- Mathlib.Algebra.Order.Field.Basic
one_div_le_neg_one : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a : α},
  a < 0 → -1 ≤ a → 1 / a ≤ -1
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Set.multiset_sum_singleton : ∀ {M : Type u_5} [inst : AddCommMonoid M] (s : Multiset M), (Multiset.map (fun i => {i}) s).sum = {s.sum}
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- The semantics for `BVUnOp`.
 -/
Std.Tactic.BVDecide.BVUnOp.eval : {w : ℕ} → Std.Tactic.BVDecide.BVUnOp → BitVec w → BitVec w
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- An analytic set is a set which is the continuous image of some Polish space. There are several
equivalent characterizations of this definition. For the definition, we pick one that avoids
universe issues: a set is analytic if and only if it is a continuous image of `ℕ → ℕ` (or if it
is empty). The above more usual characterization is given
in `analyticSet_iff_exists_polishSpace_range`.

Warning: these are analytic sets in the context of descriptive set theory (which is why they are
registered in the namespace `MeasureTheory`). They have nothing to do with analytic sets in the
context of complex analysis.  -/
MeasureTheory.AnalyticSet : {α : Type u_3} → [TopologicalSpace α] → Set α → Prop
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- If `μ : Measure α` and `f : α → β` is `AEStronglyMeasurable` where `β` is a pseudometrizable
space and a Borel space, then the identity is a.e.-strongly measurable w.r.t. `μ.map f`.  -/
MeasureTheory.AEStronglyMeasurable.aestronglyMeasurable_id_map : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {mβ : MeasurableSpace β} [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] {f : α → β},
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable id (MeasureTheory.Measure.map f μ)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.find?_toArray_eq_none_iff_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  Array.find? (fun x => cmp x.fst k == Ordering.eq) t.toArray = none ↔ t.contains k = false
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roo_ne_nil_iff : ∀ {m n : ℤ}, (m<...n).toList ≠ [] ↔ m + 1 < n
-- Mathlib.Data.Part
Part.get.congr_simp : ∀ {α : Type u} (self self_1 : Part α) (e_self : self = self_1) (a : self.Dom), self.get a = self_1.get ⋯
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasProd_empty : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {L : SummationFilter β}
  [IsEmpty β], HasProd f 1 L
-- Mathlib.Algebra.Order.Ring.WithTop
MonoidWithZeroHom.withTopMap_apply : ∀ {R : Type u_2} {S : Type u_3} [inst : MulZeroOneClass R] [inst_1 : DecidableEq R] [inst_2 : Nontrivial R]
  [inst_3 : MulZeroOneClass S] [inst_4 : DecidableEq S] [inst_5 : Nontrivial S] (f : R →*₀ S)
  (hf : Function.Injective ⇑f), ⇑(f.withTopMap hf) = WithTop.map ⇑f
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.lTensor_pow : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f : N ≃ₗ[R] N) (n : ℕ),
  LinearEquiv.lTensor M f ^ n = LinearEquiv.lTensor M (f ^ n)
-- Mathlib.Analysis.Normed.Operator.NormedSpace
/-- Precomposition with a linear isometry preserves the operator norm.  -/
ContinuousLinearMap.opNorm_comp_linearIsometryEquiv : ∀ {𝕜₁ : Type u_2} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_8}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜₁] [inst_4 : NormedSpace 𝕜₁ E] [inst_5 : NontriviallyNormedField 𝕜₂]
  [inst_6 : NormedSpace 𝕜₂ F] [inst_7 : NontriviallyNormedField 𝕜₃] [inst_8 : NormedSpace 𝕜₃ G] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
  {σ₂₁ : 𝕜₂ →+* 𝕜₁} [inst_9 : RingHomInvPair σ₁₂ σ₂₁] [inst_10 : RingHomInvPair σ₂₁ σ₁₂] {σ₂₃ : 𝕜₂ →+* 𝕜₃}
  {σ₁₃ : 𝕜₁ →+* 𝕜₃} [RingHomIsometric σ₁₃] [inst_12 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomIsometric σ₂₃]
  (f : F →SL[σ₂₃] G) (e : E ≃ₛₗᵢ[σ₁₂] F), ‖f ∘SL ↑↑e‖ = ‖f‖
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_add_le : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a b : R),
  ⌈a + b⌉ ≤ ⌈a⌉ + ⌈b⌉
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
/-- `P` is a sheaf for `S`, iff the fork given by `w` is an equalizer.  -/
CategoryTheory.Equalizer.Sieve.equalizer_sheaf_condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C}
  (S : CategoryTheory.Sieve X),
  CategoryTheory.Presieve.IsSheafFor P S.arrows ↔
    Nonempty
      (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Equalizer.forkMap P S.arrows) ⋯))
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.instMin : {α : Type u} → [inst : AddGroup α] → Min (AddGroupTopology α)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.comp_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [inst_6 : F.LaxMonoidal] [inst_7 : G.LaxMonoidal]
  (X Y : C),
  CategoryTheory.Functor.LaxMonoidal.μ (F.comp G) X Y =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ G (F.obj X) (F.obj Y))
      (G.map (CategoryTheory.Functor.LaxMonoidal.μ F X Y))
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.add_apply : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → Add (R i)] [inst_2 : ∀ (i : ι), AddMemClass (S i) (R i)]
  (x y : RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕) (i : ι), (x + y) i = x i + y i
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
_private.Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass.0.CategoryTheory.ShortComplex.ShortExact.termW : Lean.ParserDescr
-- Init.Data.BitVec.Lemmas
BitVec.msb_not : ∀ {w : ℕ} {x : BitVec w}, (~~~x).msb = (decide (0 < w) && !x.msb)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.mk_surjective : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} {x : Submonoid A},
  Function.Surjective HomogeneousLocalization.mk
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.mul_self_eq : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] {a b : A},
  CFC.sqrt a = b → autoParam (0 ≤ a) CFC.mul_self_eq._auto_1 → b * b = a
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithLowerSet.toLowerSet_inj : ∀ {α : Type u_1} {a b : α}, Topology.WithLowerSet.toLowerSet a = Topology.WithLowerSet.toLowerSet b ↔ a = b