mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.AEMeasurableSequence
aeSeq.aeSeq_eq_fun_ae : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : ι → α → β}
  {μ : MeasureTheory.Measure α} {p : α → (ι → β) → Prop} [Countable ι] (hf : ∀ (i : ι), AEMeasurable (f i) μ),
  (∀ᵐ (x : α) ∂μ, p x fun n => f n x) → ∀ᵐ (a : α) ∂μ, ∀ (i : ι), aeSeq hf p i a = f i a
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
/-- The pullback by the identity morphism identifies to the identity functor of the
category of presheaves of modules.  -/
PresheafOfModules.pullbackId : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (S : CategoryTheory.Functor Cᵒᵖ RingCat) →
      PresheafOfModules.pullback (CategoryTheory.CategoryStruct.id S) ≅ CategoryTheory.Functor.id (PresheafOfModules S)
-- Mathlib.Topology.Separation.SeparatedNhds
SeparatedNhds.disjoint_closure_right : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, SeparatedNhds s t → Disjoint s (closure t)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
QuasispectrumRestricts.nonUnitalStarAlgHom_injective : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [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] [inst_17 : IsScalarTower R S A] [inst_18 : StarModule R S]
  [inst_19 : ContinuousSMul R S] {a : A} {φ : ContinuousMapZero (↑(quasispectrum S a)) S →⋆ₙₐ[S] A},
  Function.Injective ⇑φ →
    ∀ {f : C(S, R)} (h : QuasispectrumRestricts a ⇑f),
      Function.Injective ⇑(algebraMap R S) → Function.Injective ⇑(QuasispectrumRestricts.nonUnitalStarAlgHom φ h)
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.getKey? : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → α → Option α
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_modify_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] [Inhabited α] {k fallback : α} {f : β → β},
  m.WF → (m.modify k f).getKeyD k fallback = if k ∈ m then k else fallback
-- Init.Data.String.Basic
String.Pos.offset_slice : ∀ {s : String} {p₀ p₁ pos : s.Pos} {h₁ : p₀ ≤ pos} {h₂ : pos ≤ p₁},
  (pos.slice p₀ p₁ h₁ h₂).offset = pos.offset.unoffsetBy p₀.offset
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_eq_zero : ∀ {a b : Ordinal.{u_1}}, a ^ b = 0 ↔ a = 0 ∧ b ≠ 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- The structural natural isomorphism.  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.iso : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                {X : Type u₄} →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] →
                    (self : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) →
                      self.fst.comp F ≅ self.snd.comp G
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- Pythagorean theorem, vector angle form.  -/
InnerProductGeometry.norm_add_sq_eq_norm_sq_add_norm_sq' : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  InnerProductGeometry.angle x y = Real.pi / 2 → ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.eq_iff_frequently_trunc'_eq : ∀ {σ : Type u_1} {R : Type u_2} [inst : DecidableEq σ] [inst_1 : CommSemiring R] {f g : MvPowerSeries σ R},
  f = g ↔ ∃ᶠ (m : σ →₀ ℕ) in Filter.atTop, (MvPowerSeries.trunc' R m) f = (MvPowerSeries.trunc' R m) g
-- Batteries.Tactic.Lint.Basic
/-- Returns true if `decl` is an automatically generated declaration.

Also returns true if `decl` is an internal name or created during macro expansion (after stripping
private mangling; i.e., private names are not necessarily considered autogenerated).
 -/
Lean.Environment.isAutoDecl : Lean.Environment → Lean.Name → Bool
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.unique_irreducible : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [PreValuationRing R] ⦃p q : R⦄,
  Irreducible p → Irreducible q → Associated p q
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalAddGroup.IsSES.inducedMeasure.eq_1 : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : AddGroup A] [inst_1 : AddGroup B] [inst_2 : AddGroup C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →+ B} {ψ : B →+ C}
  (H : TopologicalAddGroup.IsSES φ ψ) [inst_6 : IsTopologicalAddGroup A] [inst_7 : IsTopologicalAddGroup B]
  [inst_8 : MeasurableSpace A] [inst_9 : BorelSpace A] (μA : MeasureTheory.Measure A) [hμA : μA.IsAddHaarMeasure]
  [inst_10 : IsTopologicalAddGroup C] [inst_11 : LocallyCompactSpace B] [inst_12 : MeasurableSpace C]
  [inst_13 : BorelSpace C] (μC : MeasureTheory.Measure C) [hμC : μC.IsAddHaarMeasure] [inst_14 : T2Space B]
  [inst_15 : MeasurableSpace B] [inst_16 : BorelSpace B],
  H.inducedMeasure μA μC = RealRMK.rieszMeasure { toLinearMap := H.integrate μA μC, monotone' := ⋯ }
-- Mathlib.Data.Analysis.Topology
/-- Replace the representation type of a `Ctop` realizer.  -/
Ctop.Realizer.ofEquiv : {α : Type u_1} → {τ : Type u_4} → [inst : TopologicalSpace α] → (F : Ctop.Realizer α) → F.σ ≃ τ → Ctop.Realizer α
-- Mathlib.Analysis.Distribution.FourierMultiplier
SchwartzMap.fourierMultiplierCLM.congr_simp : ∀ {𝕜 : Type u_2} {E : Type u_3} (F : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace ℝ E] [inst_4 : NormedSpace ℂ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℂ 𝕜 F] [inst_7 : FiniteDimensional ℝ E] [inst_8 : MeasurableSpace E] [inst_9 : BorelSpace E]
  (g g_1 : E → 𝕜), g = g_1 → SchwartzMap.fourierMultiplierCLM F g = SchwartzMap.fourierMultiplierCLM F g_1
-- Mathlib.Data.Finset.Slice
/-- The `r`-th slice of `𝒜` is a subset of `𝒜`.  -/
Finset.slice_subset : ∀ {α : Type u_1} {𝒜 : Finset (Finset α)} {r : ℕ}, 𝒜.slice r ⊆ 𝒜
-- Mathlib.CategoryTheory.Localization.Bifunctor
CategoryTheory.Localization.Lifting₂.uncurry : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        {E : Type u_5} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} E] →
                    (L₁ : CategoryTheory.Functor C₁ D₁) →
                      (L₂ : CategoryTheory.Functor C₂ D₂) →
                        (W₁ : CategoryTheory.MorphismProperty C₁) →
                          (W₂ : CategoryTheory.MorphismProperty C₂) →
                            (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)) →
                              (F' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) →
                                [CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F F'] →
                                  CategoryTheory.Localization.Lifting (L₁.prod L₂) (W₁.prod W₂)
                                    (CategoryTheory.Functor.uncurry.obj F) (CategoryTheory.Functor.uncurry.obj F')
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.equiv_iff_keysArray_unit_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => Unit) cmp},
  t₁.Equiv t₂ ↔ t₁.keysArray.Perm t₂.keysArray
-- Std.Time.Time.Unit.Hour
/-- Converts an `Ordinal` to an `Offset`, which represents the duration in hours as an integer value.
 -/
Std.Time.Hour.Ordinal.toOffset : Std.Time.Hour.Ordinal → Std.Time.Hour.Offset
-- Mathlib.Algebra.Category.ModuleCat.Free
/-- In a short exact sequence `0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0`, if `X₁` and `X₃` are free,
then `X₂` is free.  -/
ModuleCat.free_shortExact : ∀ {R : Type u_3} [inst : Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)},
  S.ShortExact → ∀ [Module.Free R ↑S.X₁] [Module.Free R ↑S.X₃], Module.Free R ↑S.X₂
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_mul_right_singleton : ∀ {α : Type u_2} [inst : Group α] {a b : α}, (fun x => x * a) ⁻¹' {b} = {b * a⁻¹}
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.ballAddSubgroup_antitone : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  Antitone ArchimedeanClass.ballAddSubgroup
-- Mathlib.Algebra.LinearRecurrence
LinearRecurrence.mk.injEq : ∀ {R : Type u_1} [inst : CommSemiring R] (order : ℕ) (coeffs : Fin order → R) (order_1 : ℕ)
  (coeffs_1 : Fin order_1 → R),
  ({ order := order, coeffs := coeffs } = { order := order_1, coeffs := coeffs_1 }) =
    (order = order_1 ∧ coeffs ≍ coeffs_1)
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.processDelayed.congr_simp : ∀ (mvars mvars_1 : Array Lean.Expr) (e_mvars : mvars = mvars_1) (i i_1 : ℕ) (e_i : i = i_1) (h : i < mvars.size)
  (a a_1 : Lean.Meta.Grind.EMatch.Choice),
  a = a_1 →
    ∀ (a_2 a_3 : Lean.Meta.Grind.EMatch.Context),
      a_2 = a_3 →
        ∀ (a_4 a_5 : ST.Ref IO.RealWorld Lean.Meta.Grind.EMatch.SearchState),
          a_4 = a_5 →
            ∀ (a_6 a_7 : ST.Ref IO.RealWorld Lean.Meta.Grind.Goal),
              a_6 = a_7 →
                ∀ (a_8 a_9 : Lean.Meta.Grind.MethodsRef),
                  a_8 = a_9 →
                    ∀ (a_10 a_11 : Lean.Meta.Grind.Context),
                      a_10 = a_11 →
                        ∀ (a_12 a_13 : ST.Ref IO.RealWorld Lean.Meta.Grind.State),
                          a_12 = a_13 →
                            ∀ (a_14 a_15 : Lean.Meta.Sym.Context),
                              a_14 = a_15 →
                                ∀ (a_16 a_17 : ST.Ref IO.RealWorld Lean.Meta.Sym.State),
                                  a_16 = a_17 →
                                    ∀ (a_18 a_19 : Lean.Meta.Context),
                                      a_18 = a_19 →
                                        ∀ (a_20 a_21 : ST.Ref IO.RealWorld Lean.Meta.State),
                                          a_20 = a_21 →
                                            ∀ (a_22 a_23 : Lean.Core.Context),
                                              a_22 = a_23 →
                                                ∀ (a_24 a_25 : ST.Ref IO.RealWorld Lean.Core.State),
                                                  a_24 = a_25 →
                                                    ∀ (a_26 a_27 : Void IO.RealWorld),
                                                      a_26 = a_27 →
                                                        Lean.Meta.Grind.EMatch.processDelayed✝ mvars i h a a_2 a_4 a_6
                                                            a_8 a_10 a_12 a_14 a_16 a_18 a_20 a_22 a_24 a_26 =
                                                          Lean.Meta.Grind.EMatch.processDelayed✝ mvars_1 i_1 ⋯ a_1 a_3
                                                            a_5 a_7 a_9 a_11 a_13 a_15 a_17 a_19 a_21 a_23 a_25 a_27
-- Init.GrindInstances.ToInt
Lean.Grind.instAddUSizeUintNumBits : Lean.Grind.ToInt.Add USize (Lean.Grind.IntInterval.uint System.Platform.numBits)
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.weightEquiv_one : ∀ {ι : 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),
  ↑(RootPairing.Equiv.weightEquiv P P 1) = LinearMap.id
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.Coalgebra.Hom.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A B : G.Coalgebra}
  (f : A.A ⟶ B.A)
  (h :
    autoParam (CategoryTheory.CategoryStruct.comp A.a (G.map f) = CategoryTheory.CategoryStruct.comp f B.a)
      CategoryTheory.Comonad.Coalgebra.Hom.h._autoParam)
  (f_1 : A.A ⟶ B.A)
  (h_1 :
    autoParam (CategoryTheory.CategoryStruct.comp A.a (G.map f_1) = CategoryTheory.CategoryStruct.comp f_1 B.a)
      CategoryTheory.Comonad.Coalgebra.Hom.h._autoParam),
  ({ f := f, h := h } = { f := f_1, h := h_1 }) = (f = f_1)
-- Mathlib.Tactic.GrindAttrs
/-- The `closedness` attribute is a custom grind-set specialized to prove that sets are closed.
It is called by the `closedness` tactic.  -/
Lean.Parser.Attr.closedness : Lean.ParserDescr
-- Init.Data.List.Sublist
List.drop_sublist : ∀ {α : Type u_1} (i : ℕ) (l : List α), (List.drop i l).Sublist l
-- Lean.Expr
/-- Return `true` if `e` is of the form `optParam _ _`  -/
Lean.Expr.isOptParam : Lean.Expr → Bool
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.mem_uIoo_of_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b x : α}, a < x → x < b → x ∈ Set.uIoo a b
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- **Alias** of `Valuation.isClosed_ball`.

---

For any valuation `v` compatible with the valuative relation on `R`, the open `r`-ball
around zero `{x | v.restrict x < r}` is closed in the valuative topology.  -/
IsValuativeTopology.isClosed_ball : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible]
  (r : (MonoidWithZeroHom.ofClass v).ValueGroup₀), IsClosed {x | v.restrict x < r}
-- Mathlib.GroupTheory.OrderOfElement
AddCommute.addOrderOf_add_dvd_mul_addOrderOf : ∀ {G : Type u_1} [inst : AddMonoid G] {x y : G}, AddCommute x y → addOrderOf (x + y) ∣ addOrderOf x * addOrderOf y
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.comapEquiv_counitIso : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {β γ : Type w} (e : β ≃ γ),
  (CategoryTheory.GradedObject.comapEquiv C e).counitIso =
    CategoryTheory.Pi.comapComp (fun x => C) ⇑e.symm ⇑e ≪≫ CategoryTheory.GradedObject.comapEq C ⋯
-- Init.Data.String.Lemmas.IsEmpty
String.Slice.startPos_ne_endPos_iff : ∀ {s : String.Slice}, s.startPos ≠ s.endPos ↔ s.isEmpty = false
-- Mathlib.Topology.UniformSpace.Basic
UniformSpace.toTopologicalSpace_inf : ∀ {α : Type ua} {u v : UniformSpace α}, (u ⊓ v).toTopologicalSpace = u.toTopologicalSpace ⊓ v.toTopologicalSpace
-- Mathlib.Data.Fin.Tuple.Basic
Fin.le_cons : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} [inst : (i : Fin (n + 1)) → Preorder (α i)] {x : α 0}
  {q : (i : Fin (n + 1)) → α i} {p : (i : Fin n) → α i.succ}, q ≤ Fin.cons x p ↔ q 0 ≤ x ∧ Fin.tail q ≤ p
-- Mathlib.Data.Fintype.EquivFin
Prod.infinite_of_left : ∀ {α : Type u_1} {β : Type u_2} [Infinite α] [Nonempty β], Infinite (α × β)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.vsub_sUnion : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] (s : Set β) (T : Set (Set β)), s -ᵥ ⋃₀ T = ⋃ t ∈ T, s -ᵥ t
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSupp_sub_le : ∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : AddGroup R] (x y : HahnSeries Γ R),
  (x - y).cardSupp ≤ x.cardSupp + y.cardSupp
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_fun_sum : ∀ {T : Type u_2} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] [inst_3 : NormedSpace ℝ E]
  [SecondCountableTopology E],
  ProbabilityTheory.IsGaussianProcess X P →
    ∀ {I : Finset T}, ProbabilityTheory.HasGaussianLaw (fun ω => ∑ i ∈ I, X i ω) P
-- Mathlib.Topology.Algebra.Group.Basic
Subgroup.topologicalClosure_mono : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G] {s t : Subgroup G},
  s ≤ t → s.topologicalClosure ≤ t.topologicalClosure
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- An additive group `G` acts properly on a topological space `X` if and only if
for all ultrafilters `𝒰` on `X`, if `𝒰` converges to `(x₁, x₂)`
along the map `(g, x) ↦ (g • x, x)`, then there exists `g : G` such that `g • x₂ = x₁`
and `𝒰.fst` converges to `g`.  -/
properVAdd_iff_continuousVAdd_ultrafilter_tendsto : ∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X],
  ProperVAdd G X ↔
    ContinuousVAdd G X ∧
      ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
        Filter.Tendsto (fun gx => (gx.1 +ᵥ gx.2, gx.2)) (↑𝒰) (nhds (x₁, x₂)) →
          ∃ g, g +ᵥ x₂ = x₁ ∧ Filter.Tendsto Prod.fst (↑𝒰) (nhds g)
-- Mathlib.Analysis.Analytic.Composition
Composition.blocksFun_sigmaCompositionAux : ∀ {n : ℕ} (a : Composition n) (b : Composition a.length) (i : Fin b.length) (j : Fin (b.blocksFun i)),
  (a.sigmaCompositionAux b ⟨↑i, ⋯⟩).blocksFun ⟨↑j, ⋯⟩ = a.blocksFun ((b.embedding i) j)
-- Init.Notation
/-- `(p)?` is shorthand for `optional(p)`. It uses parser `p` 0 or 1 times, and produces a
`nullNode` containing the array of parsed results. This parser has arity 1.

`p` is allowed to have arity n > 1 (in which case the node will have either 0 or n children),
but if it has arity 0 then the result will be ambiguous.

Because `?` is an identifier character, `ident?` will not work as intended.
You have to write either `ident ?` or `(ident)?` for it to parse as the `?` combinator
applied to the `ident` parser.
 -/
stx_? : Lean.TrailingParserDescr
-- Mathlib.Data.Setoid.Partition
/-- The equivalence classes of the equivalence relation defined by a set of sets
partitioning α are elements of the set of sets.  -/
Setoid.eqv_class_mem : ∀ {α : Type u_1} {c : Set (Set α)} (H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b) {y : α}, {x | (Setoid.mkClasses c H) x y} ∈ c
-- Mathlib.Algebra.Ring.Rat
Rat.commSemiring : CommSemiring ℚ
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.compProd_map_condDistrib : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_3 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β},
  AEMeasurable Y μ →
    (MeasureTheory.Measure.map X μ).compProd (ProbabilityTheory.condDistrib Y X μ) =
      MeasureTheory.Measure.map (fun a => (X a, Y a)) μ
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isNonloop_iff_notMem_loops : ∀ {α : Type u_1} {M : Matroid α} {e : α},
  autoParam (e ∈ M.E) Matroid.isNonloop_iff_notMem_loops._auto_1 → (M.IsNonloop e ↔ e ∉ M.loops)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.instFunLikeSubtypeForallProdVMemSubmoduleCoboundaries₂ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → {A : Rep.{u_1, u, u} k G} → FunLike (↥(groupCohomology.coboundaries₂ A)) (G × G) ↑A
-- Mathlib.Analysis.Complex.Exponential
Complex.norm_exp_sub_one_le : ∀ {x : ℂ}, ‖x‖ ≤ 1 → ‖Complex.exp x - 1‖ ≤ 2 * ‖x‖
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- Given `x : X _⦋n⦌`, this is the epimorphism from `Δ[n]`
to the subcomplex of `X` generated by `x`.  -/
SSet.Subcomplex.toOfSimplex : {X : SSet} →
  {n : ℕ} →
    (x : X.obj (Opposite.op { len := n })) → SSet.stdSimplex.obj { len := n } ⟶ (SSet.Subcomplex.ofSimplex x).toSSet
-- Mathlib.Dynamics.Newton
/-- If `x` is almost a root of `P` in the sense that `P(x)` is nilpotent (and `P'(x)` is a
unit) then we may write `x` as a sum `x = n + r` where `n` is nilpotent and `r` is a root of `P`.
Moreover, `n` and `r` are unique.

This can be used to prove the Jordan-Chevalley decomposition of linear endomorphisms.  -/
Polynomial.existsUnique_nilpotent_sub_and_aeval_eq_zero : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Polynomial R}
  {x : S},
  IsNilpotent ((Polynomial.aeval x) P) →
    IsUnit ((Polynomial.aeval x) (Polynomial.derivative P)) → ∃! r, IsNilpotent (x - r) ∧ (Polynomial.aeval r) P = 0
-- Std.Http.Data.URI.Basic
Std.Http.URI.Host.ipv6.sizeOf_spec : ∀ (ipv6 : Std.Net.IPv6Addr), sizeOf (Std.Http.URI.Host.ipv6 ipv6) = 1 + sizeOf ipv6
-- Lean.Expr
Lean.FVarIdSet.union : Lean.FVarIdSet → Lean.FVarIdSet → Lean.FVarIdSet
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
/-- In an `R`-algebra with a continuous functional calculus, every element satisfying the predicate
has nonempty `R`-spectrum.  -/
CFC.spectrum_nonempty : ∀ (R : Type u_1) {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [Nontrivial A] (a : A),
  autoParam (p a) CFC.spectrum_nonempty._auto_1 → (spectrum R a).Nonempty
-- Mathlib.Data.Setoid.Partition
/-- The obvious equivalence between the quotient associated to an indexed partition and
the indexing type.  -/
IndexedPartition.equivQuotient : {ι : Type u_1} → {α : Type u_2} → {s : ι → Set α} → (hs : IndexedPartition s) → ι ≃ hs.Quotient
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.instWeaklyEtaleF : ∀ {S : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage @AlgebraicGeometry.WeaklyEtale) S)
  (i : 𝒰.I₀), AlgebraicGeometry.WeaklyEtale (𝒰.f i)
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.not_xor : ∀ (a b : Bool), (!(a ^^ b)) = (a == b)
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.coroot_coweightMap : ∀ {ι : 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] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (self : P.Hom Q),
  ⇑self.coweightMap ∘ ⇑Q.coroot = ⇑P.coroot ∘ ⇑self.indexEquiv.symm
-- Plausible.Gen
Plausible.instMonadLiftGen : {m : Type u_1 → Type u_2} →
  [MonadLiftT m (ReaderT (ULift.{u_1, 0} ℕ) (Except Plausible.GenError))] →
    MonadLiftT (Plausible.RandGT StdGen m) Plausible.Gen
-- Mathlib.Algebra.Order.Group.PosPart
negPart_neg : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] (a : α), (-a)⁻ = a⁺
-- Mathlib.Tactic.Simproc.ExistsAndEq
/-- Used to indicate the current case should be unreachable, unless an invariant is violated.
`context` should be used to indicate which case is asserted to be unreachable.
For example, `"findEq: path for a conjunction should be nonempty"`.  -/
_private.Mathlib.Tactic.Simproc.ExistsAndEq.0.ExistsAndEq.assertUnreachable : {α : Type} → String → Lean.MetaM α
-- Mathlib.CategoryTheory.Action.Continuous
ContAction.res_obj_obj : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {FV : V → V → Type u_2} {CV : V → Type u_3}
  [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] [inst_2 : CategoryTheory.ConcreteCategory V FV]
  [inst_3 : CategoryTheory.HasForget₂ V TopCat] {G : Type u_4} [inst_4 : Monoid G] [inst_5 : TopologicalSpace G]
  {H : Type u_5} [inst_6 : Monoid H] [inst_7 : TopologicalSpace H] (f : G →ₜ* H) (X : ContAction V H),
  ((ContAction.res V f).obj X).obj = (Action.res V ↑f).obj X.obj
-- Lean.AuxRecursor
Lean.NoConfusionInfo.perCtor.injEq : ∀ (arity fields arity_1 fields_1 : ℕ),
  (Lean.NoConfusionInfo.perCtor arity fields = Lean.NoConfusionInfo.perCtor arity_1 fields_1) =
    (arity = arity_1 ∧ fields = fields_1)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min?_insert_le_self : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k kmi : α},
  (t.insert k).min?.get ⋯ = kmi → (cmp kmi k).isLE = true