mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Linter.Basic
/-- Given a command elaborator `cmd`, returns a new command elaborator that
first peels off and evaluates `set_option ... in ...` syntax recursively, updating the options
accordingly, and then invokes `cmd` on the inner syntax.

This is expected to be used in linters, after elaboration is complete. It is not appropriate for
ordinary elaboration of outer `set_option`s, since it
* does not update the infotrees with info for the `set_option` commands
* silently ignores failures in setting the given options (e.g. we do not error if the option is
  unknown or the wrong type of value is provided), as these should have been reported during
  original elaboration.
 -/
Lean.withSetOptionIn : Lean.Elab.Command.CommandElab → Lean.Elab.Command.CommandElab
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : Option β → Option β},
  Std.ExtDHashMap.Const.get? (Std.ExtDHashMap.Const.alter m k f) k' =
    if (k == k') = true then f (Std.ExtDHashMap.Const.get? m k) else Std.ExtDHashMap.Const.get? m k'
-- Mathlib.FieldTheory.RatFunc.Defs
/-- `RatFunc K` is `K(X)`, the field of rational functions over `K`.

The inclusion of polynomials into `RatFunc` is `algebraMap K[X] K⟮X⟯`,
the maps between `K⟮X⟯` and another field of fractions of `K[X]`,
especially `FractionRing K[X]`, are given by `IsLocalization.algEquiv`.
 -/
RatFunc.«term_⟮X⟯» : Lean.TrailingParserDescr
-- Batteries.Data.Fin.Coding
Fin.decodeProd.eq_1 : ∀ {m n : ℕ} (z : Fin (m * n)), Fin.decodeProd z = (z.divNat, z.modNat)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.toNNRealLinear_apply : ∀ {α : Type u_2} [inst : TopologicalSpace α] (Λ : CompactlySupportedContinuousMap α ℝ →ₚ[ℝ] ℝ)
  (f : CompactlySupportedContinuousMap α NNReal), ↑((CompactlySupportedContinuousMap.toNNRealLinear Λ) f) = Λ f.toReal
-- Mathlib.Analysis.Normed.Group.Uniform
SeparationQuotient.norm_mk : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] (p : E), ‖SeparationQuotient.mk p‖ = ‖p‖
-- Init.ShareCommon
ShareCommon.StateFactoryBuilder.mk.sizeOf_spec : ∀ (Map : (α : Type) → Type → [BEq α] → [Hashable α] → Type)
  (mkMap : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ℕ → Map α β)
  (mapFind? : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Map α β → α → Option β)
  (mapInsert : {α β : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Map α β → α → β → Map α β)
  (Set : (α : Type) → [BEq α] → [Hashable α] → Type)
  (mkSet : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → ℕ → Set α)
  (setFind? : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Set α → α → Option α)
  (setInsert : {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → Set α → α → Set α),
  sizeOf
      { Map := Map, mkMap := mkMap, mapFind? := mapFind?, mapInsert := mapInsert, Set := Set, mkSet := mkSet,
        setFind? := setFind?, setInsert := setInsert } =
    1
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.Pairing.RankFunction.mk.sizeOf_spec : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {α : Type v} [inst : PartialOrder α] [inst_1 : SizeOf α]
  (rank : ↑P.II → α) (lt : ∀ {x y : ↑P.II}, P.AncestralRel x y → rank x < rank y), sizeOf { rank := rank, lt := lt } = 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_erase! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k a : α},
      Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.erase! k t) a =
        if compare k a = Ordering.eq then none else Std.DTreeMap.Internal.Impl.Const.get? t a
-- Mathlib.Topology.Homotopy.Path
ContinuousMap.Homotopy.evalAt_apply : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f g : C(X, Y)} (H : f.Homotopy g)
  (x : X) (t : ↑unitInterval), (H.evalAt x) t = H (t, x)
-- Mathlib.Algebra.Order.PUnit
PUnit.canonicallyOrderedAdd : CanonicallyOrderedAdd PUnit.{u_1 + 1}
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.rightInvSeq_reverse : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B),
  cs.rightInvSeq ω.reverse = (cs.leftInvSeq ω).reverse
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.gc_generateFrom : ∀ (X : Type u_2), GaloisConnection DiffeologicalSpace.generateFrom DiffeologicalSpace.toPlots
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.adjunctionOfEquivLeft_unit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {G : CategoryTheory.Functor D C} {F_obj : C → D} (e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
  (he :
    ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
      (e X Y') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g))
  (X : C),
  (CategoryTheory.Adjunction.adjunctionOfEquivLeft e he).unit.app X =
    (e X (F_obj X)) (CategoryTheory.CategoryStruct.id (F_obj X))
-- Mathlib.Data.Set.Function
Function.invFunOn_apply_eq : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {a : α} [inst : Nonempty α],
  a ∈ s → f (Function.invFunOn f s (f a)) = f a
-- Mathlib.Analysis.Convex.Side
/-- The points `x` and `y` are weakly on the same side of `s`.  -/
AffineSubspace.WSameSide : {R : Type u_1} →
  {V : Type u_2} →
    {P : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : PartialOrder R] →
          [IsStrictOrderedRing R] →
            [inst_3 : AddCommGroup V] →
              [inst_4 : Module R V] → [inst_5 : AddTorsor V P] → AffineSubspace R P → P → P → Prop
-- Aesop.Forward.State
/-- Get the slot with the given premise index.  -/
Aesop.ClusterState.findSlot? : Aesop.ClusterState → Aesop.PremiseIndex → Option Aesop.Slot
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier.eq_1 : AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier =
  { hom := fun {X Y} => AddCommGrpCat.Hom.hom', ofHom := fun {X Y} => AddCommGrpCat.Hom.mk✝,
    hom_ofHom := @AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier._proof_1,
    ofHom_hom := @AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier._proof_2,
    id_apply := @AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier._proof_3,
    comp_apply := @AddCommGrpCat.instConcreteCategoryAddMonoidHomCarrier._proof_4 }
-- Mathlib.Analysis.RCLike.BoundedContinuous
/-- On a star subalgebra of bounded continuous functions, the operations "restrict scalars to ℝ"
and "forget that a bounded continuous function is a bounded" commute.  -/
RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : RCLike 𝕜] [inst_1 : PseudoEMetricSpace E]
  {A : StarSubalgebra 𝕜 (BoundedContinuousFunction E 𝕜)},
  Subalgebra.map (BoundedContinuousFunction.toContinuousMapₐ ℝ)
      (Subalgebra.comap (BoundedContinuousFunction.AlgHom.compLeftContinuousBounded ℝ RCLike.ofRealAm ⋯)
        (Subalgebra.restrictScalars ℝ A.toSubalgebra)) =
    Subalgebra.comap (AlgHom.compLeftContinuous ℝ RCLike.ofRealAm ⋯)
      (Subalgebra.restrictScalars ℝ
        (StarSubalgebra.map (BoundedContinuousFunction.toContinuousMapStarₐ 𝕜) A).toSubalgebra)
-- Mathlib.AlgebraicGeometry.Fiber
AlgebraicGeometry.Scheme.Hom.fiber_fac : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (y : ↥Y),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.fiberι f y) f =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f y)
      (Y.fromSpecResidueField y)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (e : X ≅ Y) (x : ↑X.toTopCat),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.inv ((CategoryTheory.ConcreteCategory.hom e.hom.base) x))
      (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.hom x) =
    X.presheaf.stalkSpecializes ⋯
-- Lean.Util.FindExpr
Lean.Expr.findImpl? : (Lean.Expr → Bool) → Lean.Expr → Option Lean.Expr
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.isSuccPrelimit_zero : Order.IsSuccPrelimit 0
-- Mathlib.Topology.Sion
/-- The familywise sublevel sets of `f`, the first variable serving as a parameter  -/
_private.Mathlib.Topology.Sion.0.Sion.sublevelLeft : {E : Type u_1} → {F : Type u_2} → {β : Type u_3} → [LinearOrder β] → (X : Set E) → (E → F → β) → β → F → Set ↑X
-- Lean.Data.Lsp.Basic
Lean.Lsp.MarkupKind.plaintext.sizeOf_spec : sizeOf Lean.Lsp.MarkupKind.plaintext = 1
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.embDomainRingHom_C : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  {Γ' : Type u_6} [inst_3 : AddCommMonoid Γ'] [inst_4 : PartialOrder Γ'] [inst_5 : IsOrderedCancelAddMonoid Γ']
  [inst_6 : NonAssocSemiring R] {f : Γ →+ Γ'} {hfi : Function.Injective ⇑f} {hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g'}
  {r : R}, (HahnSeries.embDomainRingHom f hfi hf) (HahnSeries.C r) = HahnSeries.C r
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
/-- The class of morphisms in `Arrow C` which on the left side are
pushouts of coproducts of morphisms in `I`, and which are
isomorphisms on the right side.  -/
CategoryTheory.SmallObject.propArrow : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty (CategoryTheory.Arrow C)
-- Mathlib.Topology.Algebra.Monoid
isClosed_setOfPred_map_one : ∀ (M₁ : Type u_6) (M₂ : Type u_7) [inst : TopologicalSpace M₂] [T2Space M₂] [inst_2 : One M₁] [inst_3 : One M₂],
  IsClosed {f | f 1 = 1}
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- An embedding of graphs gives rise to a homomorphism of graphs.  -/
SimpleGraph.Embedding.toHom : {V : Type u_1} → {W : Type u_2} → {G : SimpleGraph V} → {G' : SimpleGraph W} → G ↪g G' → G →g G'
-- Init.Data.String.Iterator
String.Legacy.Iterator.sizeOf_next_lt_of_atEnd : ∀ (i : String.Legacy.Iterator), ¬i.atEnd = true → sizeOf i.next < sizeOf i
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.curry_injective : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {P₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid P₂]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R₂ P₂], Function.Injective TensorProduct.curry
-- Mathlib.Algebra.Group.Semiconj.Defs
semiconjBy_iff_eq : ∀ {M : Type u_2} [inst : CancelCommMonoid M] {a x y : M}, SemiconjBy a x y ↔ x = y
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.isoCoprod.eq_1 : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.Limits.biprod.isoCoprod X Y =
    (CategoryTheory.Limits.BinaryBiproduct.isColimit X Y).coconePointUniqueUpToIso
      (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.pair X Y))
-- Mathlib.Probability.Distributions.Poisson.Basic
ProbabilityTheory.instIsProbabilityMeasureNatPoissonMeasure : ∀ (r : NNReal), MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.poissonMeasure r)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
/-- The morphisms of the free monoidal category satisfy 21 relations ensuring that the resulting
category is in fact a category and that it is monoidal.  -/
CategoryTheory.FreeMonoidalCategory.HomEquiv : {C : Type u} → {X Y : CategoryTheory.FreeMonoidalCategory C} → X.Hom Y → X.Hom Y → Prop
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one' : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ p), (Ideal.span {hζ.toInteger - 1}).IsPrime
-- Std.Internal.UV.System
Std.Internal.UV.System.RUsage.userTime : Std.Internal.UV.System.RUsage → UInt64
-- Mathlib.Topology.Homotopy.Contractible
/-- A contractible space is one that is homotopy equivalent to `Unit`.  -/
ContractibleSpace : (X : Type u_1) → [TopologicalSpace X] → Prop
-- Mathlib.Order.Filter.Pointwise
Filter.sub_mem_sub : ∀ {α : Type u_2} [inst : Sub α] {f g : Filter α} {s t : Set α}, s ∈ f → t ∈ g → s - t ∈ f - g
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- **Integration by parts on (-∞, ∞).**
With respect to a general bilinear form, assuming moreover that the total function is integrable.
 -/
MeasureTheory.integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable : ∀ {E : Type u_1} {F : Type u_2} {G : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {L : E →L[ℝ] F →L[ℝ] G} {u : ℝ → E} {v : ℝ → F} {u' : ℝ → E} {v' : ℝ → F},
  (∀ x ∈ tsupport v, HasDerivAt u (u' x) x) →
    (∀ x ∈ tsupport u, HasDerivAt v (v' x) x) →
      MeasureTheory.Integrable (fun x => (L (u x)) (v' x)) MeasureTheory.volume →
        MeasureTheory.Integrable (fun x => (L (u' x)) (v x)) MeasureTheory.volume →
          MeasureTheory.Integrable (fun x => (L (u x)) (v x)) MeasureTheory.volume →
            ∫ (x : ℝ), (L (u x)) (v' x) = -∫ (x : ℝ), (L (u' x)) (v x)
-- Std.Data.ExtHashMap.Basic
/-- Returns `true` if there is a mapping for the given key. There is also a `Prop`-valued version
of this: `a ∈ m` is equivalent to `m.contains a = true`.

Observe that this is different behavior than for lists: for lists, `∈` uses `=` and `contains` uses
`==` for comparisons, while for hash maps, both use `==`.
 -/
Std.ExtHashMap.contains : {α : Type u} →
  {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashMap α β → α → Bool
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- The Lusin-Souslin theorem: if `s` is Borel-measurable in a Polish space, then its image under
a continuous injective map is also Borel-measurable.  -/
MeasurableSet.image_of_continuousOn_injOn : ∀ {γ : Type u_3} {β : Type u_5} [inst : MeasurableSpace β] [tβ : TopologicalSpace β] [T2Space β] {s : Set γ} {f : γ → β}
  [OpensMeasurableSpace β] [tγ : TopologicalSpace γ] [PolishSpace γ] [inst_4 : MeasurableSpace γ] [BorelSpace γ],
  MeasurableSet s → ContinuousOn f s → Set.InjOn f s → MeasurableSet (f '' s)
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.listTake_alternatingWord : ∀ {B : Type u_1} (i j : B) (p k : ℕ),
  k < 2 * p →
    List.take k (CoxeterSystem.alternatingWord i j (2 * p)) =
      if Even k then CoxeterSystem.alternatingWord i j k else CoxeterSystem.alternatingWord j i k
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.not_mem_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₁ → k ∉ m₁ \ m₂
-- Mathlib.SetTheory.Ordinal.Notation
ONote.addAux.eq_2 : ∀ (e : ONote) (n : ℕ+) (e' : ONote) (n' : ℕ+) (a' : ONote),
  e.addAux n (e'.oadd n' a') =
    match e.cmp e' with
    | Ordering.lt => e'.oadd n' a'
    | Ordering.eq => e.oadd (n + n') a'
    | Ordering.gt => e.oadd n (e'.oadd n' a')
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.rel_symm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)},
  Std.Symm (SimpleGraph.TripartiteFromTriangles.Rel t)
-- Mathlib.Data.Multiset.ZeroCons
/-- `Rel r s t` -- lift the relation `r` between two elements to a relation between `s` and `t`,
s.t. there is a one-to-one mapping between elements in `s` and `t` following `r`.  -/
Multiset.Rel : {α : Type u_1} → {β : Type v} → (α → β → Prop) → Multiset α → Multiset β → Prop
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.measure_mul_setLAverage : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (f : α → ENNReal),
  μ s ≠ ⊤ → μ s * ⨍⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, f x ∂μ
-- Lean.Data.PersistentArray
Lean.PersistentArrayNode.brecOn.go : {α : Type u} →
  {motive_1 : Lean.PersistentArrayNode α → Sort u_1} →
    {motive_2 : Array (Lean.PersistentArrayNode α) → Sort u_1} →
      {motive_3 : List (Lean.PersistentArrayNode α) → Sort u_1} →
        (t : Lean.PersistentArrayNode α) →
          ((t : Lean.PersistentArrayNode α) → t.below → motive_1 t) →
            ((t : Array (Lean.PersistentArrayNode α)) → Lean.PersistentArrayNode.below_1 t → motive_2 t) →
              ((t : List (Lean.PersistentArrayNode α)) → Lean.PersistentArrayNode.below_2 t → motive_3 t) →
                motive_1 t ×' t.below
-- Mathlib.GroupTheory.OrderOfElement
/-- `IsOfFinAddOrder` is a predicate on an element `a` of an
additive monoid to be of finite order, i.e. there exists `n ≥ 1` such that `n • a = 0`.  -/
IsOfFinAddOrder : {G : Type u_1} → [AddMonoid G] → G → Prop
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.bot_edgeSet : ∀ (α : Type u_4), ⊥.edgeSet = ∅
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_comp : ∀ {o o' : Ordinal.{max u v}} {f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}},
  (∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj) →
    ∀ {g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}} (hg : o'.blsub g = o),
      (o'.bsup fun a ha => f (g a ha) ⋯) = o.bsup f
-- Init.Data.SInt.Lemmas
Int8.left_eq_add : ∀ {a b : Int8}, a = a + b ↔ b = 0
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instInhabitedSyntheticMVarDecl : Inhabited Lean.Elab.Term.SyntheticMVarDecl
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.natCast_lt_aleph0 : ∀ {n : ℕ}, ↑n < Cardinal.aleph0
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_balanceLErase : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hlb : l.Balanced}
  {hrb : r.Balanced} {hlr : Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size},
  (Std.DTreeMap.Internal.Impl.balanceLErase k v l r hlb hrb hlr).toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel
-- Mathlib.Algebra.Polynomial.HasseDeriv
Polynomial.hasseDeriv_one : ∀ {R : Type u_1} [inst : Semiring R], Polynomial.hasseDeriv 1 = Polynomial.derivative
-- Mathlib.MeasureTheory.Measure.Doubling
/-- A scale below which the doubling measure `μ` satisfies good rescaling properties when one
multiplies the radius of balls by at most `K`, as stated
in `IsUnifLocDoublingMeasure.measure_mul_le_scalingConstantOf_mul`.  -/
IsUnifLocDoublingMeasure.scalingScaleOf : {α : Type u_1} →
  [inst : PseudoMetricSpace α] →
    [inst_1 : MeasurableSpace α] → (μ : MeasureTheory.Measure α) → [IsUnifLocDoublingMeasure μ] → ℝ → ℝ
-- Lean.Server.Completion.CompletionCollectors
Lean.Server.Completion.tacticCompletion : Lean.Lsp.DocumentUri → Lean.Lsp.Position → ℕ → Lean.Elab.ContextInfo → IO (Array Lean.Lsp.ResolvableCompletionItem)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
ContinuousLinearMap.norm_compLpL_le : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {𝕜 : Type u_6} {𝕜' : Type u_7}
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' F] {σ : 𝕜 →+* 𝕜'} [inst_6 : RingHomIsometric σ] [inst_7 : Fact (1 ≤ p)] (L : E →SL[σ] F),
  ‖ContinuousLinearMap.compLpL p μ L‖ ≤ ‖L‖
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- The bijection `normalizedFactorsEquivSpanNormalizedFactors` between the set of prime
factors of `r` and the set of prime factors of the ideal `⟨r⟩` preserves multiplicities. See
`count_normalizedFactorsSpan_eq_count` for the version stated in terms of multisets `count`.  -/
Ideal.emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R]
  [inst_3 : NormalizationMonoid R] {r d : R} (hr : r ≠ 0) (hd : d ∈ UniqueFactorizationMonoid.normalizedFactors r),
  emultiplicity d r = emultiplicity (↑((Ideal.normalizedFactorsEquivSpanNormalizedFactors hr) ⟨d, hd⟩)) (Ideal.span {r})
-- Mathlib.RingTheory.TwoSidedIdeal.BigOperators
TwoSidedIdeal.dfinsuppProd_mem : ∀ {R : Type u_1} [inst : CommRing R] (I : TwoSidedIdeal R) {ι : Type u_2} {β : ι → Type u_3} [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → Zero (β i)] [inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {f : Π₀ (i : ι), β i}
  (g : (i : ι) → β i → R), (∃ i ∈ f.support, g i (f i) ∈ I) → f.prod g ∈ I
-- Qq.Match
/-- `Qq`s expression matching in `MetaM`, up to reducible defeq.

This syntax is valid in `match`, `let`, and `if let`, but not `fun`.

The usage is very similar to the builtin `Syntax`-matching that uses `` `(<pattern>)`` notation.
As an example, consider matching against a `n : Q(ℕ)`, which can be written

* With a `match` expression,
  ```
  match n with
  | ~q(Nat.gcd $x $y) => handleGcd x y
  | ~q($x + $y) => handleAdd x y
  | _ => throwError "no match"
  ```
* With a `let` expression (if there is a single match)
  ```
  let ~q(Nat.gcd $x $y) := n | throwError "no match"
  handleGcd x y
  ```
* With an `if let` statement
  ```
  if let ~q(Nat.gcd $x $y) := n then
    handleGcd x y
  else if let ~q($x + $y) := n then
    handleAdd x y
  else
    throwError "no match"
  ```

In addition to the obvious `x` and `y` captures,
in the example above `~q` also inserts into the context a term of type `$n =Q Nat.gcd $x $y`.
 -/
Qq.matcher : Lean.ParserDescr
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
/-- The restriction `Aut(L/K) → Aut(B/A)` in an AKLB setup.  -/
galRestrict : (A : Type u_1) →
  (K : Type u_2) →
    (L : Type u_3) →
      (B : Type u_6) →
        [inst : CommRing A] →
          [inst_1 : CommRing B] →
            [inst_2 : Algebra A B] →
              [inst_3 : Field K] →
                [inst_4 : Field L] →
                  [inst_5 : Algebra A K] →
                    [IsFractionRing A K] →
                      [inst_7 : Algebra K L] →
                        [inst_8 : Algebra A L] →
                          [IsScalarTower A K L] →
                            [inst_10 : Algebra B L] →
                              [IsScalarTower A B L] →
                                [IsIntegralClosure B A L] → [Algebra.IsAlgebraic K L] → Gal(L/K) ≃* B ≃ₐ[A] B
-- Std.Data.TreeMap.Raw.Slice
Std.TreeMap.Raw.instSliceableRoiSlice : {α : Type u} →
  {β : Type v} →
    (cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw.instSliceableRoiSlice._auto_1) →
      Std.Roi.Sliceable (Std.TreeMap.Raw α β cmp) α (Std.DTreeMap.Internal.Const.RoiSlice α β)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Embedding.apply_mem_neighborSet_iff : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ↪g G') {v w : V},
  f w ∈ G'.neighborSet (f v) ↔ w ∈ G.neighborSet v
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
AhlswedeZhang.supSum.eq_1 : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (𝒜 : Finset (Finset α)),
  AhlswedeZhang.supSum 𝒜 =
    ∑ s, ↑(𝒜.truncatedSup s).card / ((↑(Fintype.card α) - ↑s.card) * ↑((Fintype.card α).choose s.card))
-- Mathlib.Data.NNReal.Defs
NNReal.instArchimedean : Archimedean NNReal
-- Mathlib.Topology.UniformSpace.CompleteSeparated
IsUniformEmbedding.isClosedEmbedding : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] [CompleteSpace α] [T0Space β]
  {f : α → β}, IsUniformEmbedding f → Topology.IsClosedEmbedding f
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, (Set.Ioi a).OrdConnected