mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.OpenPos
IsOpen.measure_eq_zero_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure]
  {U : Set X}, IsOpen U → (μ U = 0 ↔ U = ∅)
-- Mathlib.Algebra.Lie.Basic
LieHom.coe_mk : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁]
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L₁ → L₂) (h₁ : ∀ (x y : L₁), f (x + y) = f x + f y)
  (h₂ :
    ∀ (m : R) (x : L₁),
      { toFun := f, map_add' := h₁ }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := h₁ }.toFun x)
  (h₃ :
    ∀ {x y : L₁},
      { toFun := f, map_add' := h₁, map_smul' := h₂ }.toFun ⁅x, y⁆ =
        ⁅{ toFun := f, map_add' := h₁, map_smul' := h₂ }.toFun x,
          { toFun := f, map_add' := h₁, map_smul' := h₂ }.toFun y⁆),
  ⇑{ toFun := f, map_add' := h₁, map_smul' := h₂, map_lie' := h₃ } = f
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.MethodsRef.toMethods : Lean.Meta.Sym.Simp.MethodsRef → Lean.Meta.Sym.Simp.Methods
-- Mathlib.Tactic.NormNum.GCD
Mathlib.Meta.NormNum.nat_gcd_helper_dvd_right : ∀ (x y : ℕ), x % y = 0 → x.gcd y = y
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.Pos.skipWhile.match_1.eq_1 : ∀ {s : String.Slice} (motive : Option s.Pos → Sort u_1) (nextCurr : s.Pos)
  (h_1 : (nextCurr : s.Pos) → motive (some nextCurr)) (h_2 : Unit → motive none),
  (match some nextCurr with
    | some nextCurr => h_1 nextCurr
    | none => h_2 ()) =
    h_1 nextCurr
-- Std.Sync.Channel
/-- Receive a value from the channel, blocking until the transmission could be completed.
 -/
Std.Channel.Sync.recv : {α : Type} → [Inhabited α] → Std.Channel.Sync α → BaseIO α
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
/-- Given an integrable function `g`, the conditional expectations of `g` with respect to
a sequence of sub-σ-algebras is uniformly integrable.  -/
MeasureTheory.Integrable.uniformIntegrable_condExp : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_2} [MeasureTheory.IsFiniteMeasure μ]
  {g : α → ℝ},
  MeasureTheory.Integrable g μ →
    ∀ {ℱ : ι → MeasurableSpace α}, (∀ (i : ι), ℱ i ≤ m0) → MeasureTheory.UniformIntegrable (fun i => μ[g | ℱ i]) 1 μ
-- Mathlib.Algebra.Group.Defs
/-- A commutative additive magma is a type with an addition which commutes.  -/
AddCommMagma : Type u → Type u
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.below.comp : ∀ {motive : {n : ℕ} → (a : List.Vector ℕ n →. ℕ) → Nat.Partrec' a → Prop} {m n : ℕ} {f : List.Vector ℕ n →. ℕ}
  (g : Fin n → List.Vector ℕ m →. ℕ) (a : Nat.Partrec' f) (a_1 : ∀ (i : Fin n), Nat.Partrec' (g i)),
  Nat.Partrec'.below a →
    motive f a → (∀ (i : Fin n), Nat.Partrec'.below ⋯) → (∀ (i : Fin n), motive (g i) ⋯) → Nat.Partrec'.below ⋯
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_liftAt_one : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {n m : ℕ} {φ : L.BoundedFormula α n}
  {v : α → M} {xs : Fin (n + 1) → M},
  m ≤ n →
    ((FirstOrder.Language.BoundedFormula.liftAt 1 m φ).Realize v xs ↔
      φ.Realize v (xs ∘ fun i => if ↑i < m then i.castSucc else i.succ))
-- Mathlib.Topology.Algebra.Module.TransferInstance
Shrink.continuousLinearEquiv_symm_apply : ∀ (R : Type u_1) (α : Type u_2) [inst : Small.{v, u_2} α] [inst_1 : AddCommMonoid α] [inst_2 : TopologicalSpace α]
  [inst_3 : Semiring R] [inst_4 : Module R α] (a : α), (Shrink.continuousLinearEquiv R α).symm a = (equivShrink α) a
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α}, k ∉ m₂ → (m₁ ∩ m₂).get! k = default
-- Lean.ProjFns
/-- Given a structure `S`, Lean automatically creates an auxiliary definition (projection function)
for each field. This structure caches information about these auxiliary definitions.
 -/
Lean.ProjectionFunctionInfo : Type
-- Mathlib.CategoryTheory.Functor.Const
/-- These are actually equal, of course, but not definitionally equal
(the equality requires `F.map (𝟙 _) = 𝟙 _`). A natural isomorphism is
more convenient than an equality between functors (compare id_to_iso).  -/
CategoryTheory.Functor.constComp : (J : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C] →
        {D : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} D] →
            (X : C) →
              (F : CategoryTheory.Functor C D) →
                ((CategoryTheory.Functor.const J).obj X).comp F ≅ (CategoryTheory.Functor.const J).obj (F.obj X)
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- The inner product is *Hermitian*, taking the `conj` swaps the arguments.  -/
PreInnerProductSpace.Core.conj_inner_symm : ∀ {𝕜 : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  (self : PreInnerProductSpace.Core 𝕜 F) (x y : F), (starRingEnd 𝕜) (inner 𝕜 y x) = inner 𝕜 x y
-- Mathlib.LinearAlgebra.Pi
LinearMap.vecEmpty_apply : ∀ {R : Type u} {M : Type v} {M₃ : Type y} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₃]
  [inst_3 : Module R M] [inst_4 : Module R M₃] (m : M), LinearMap.vecEmpty m = ![]
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_inter!_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Inhabited α]
  [Std.TransOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.inter! m₂).getKey! k = default
-- Mathlib.Probability.Distributions.Uniform
PMF.toMeasure_ofMultiset_apply : ∀ {α : Type u_1} {s : Multiset α} (hs : s ≠ 0) (t : Set α) [inst : MeasurableSpace α],
  MeasurableSet t →
    (PMF.ofMultiset s hs).toMeasure t = (∑' (x : α), ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s))) / ↑s.card
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.one : {α : Type u} → [One α] → One (WithBot α)
-- Mathlib.CategoryTheory.Monoidal.Limits.Preserves
/-- When `C` is braided and `tensorLeft c` preserves a limit, then so does `tensorRight k`.  -/
CategoryTheory.MonoidalCategory.Limits.preservesLimit_of_braided_and_preservesLimit_tensor_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {J : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} J] (F : CategoryTheory.Functor J C)
  [CategoryTheory.BraidedCategory C] (c : C)
  [CategoryTheory.Limits.PreservesLimit F (CategoryTheory.MonoidalCategory.tensorLeft c)],
  CategoryTheory.Limits.PreservesLimit F (CategoryTheory.MonoidalCategory.tensorRight c)
-- Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
/-- Auxiliary definition for `OneHypercoverFamily.isSheaf_iff`.  -/
CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.isLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          {H : J.OneHypercoverFamily} →
            {P : CategoryTheory.Functor Cᵒᵖ A} →
              (∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))) →
                {X : C} →
                  {S : CategoryTheory.Sieve X} →
                    {E : J.OneHypercover X} →
                      H E →
                        (le : E.sieve₀ ≤ S) →
                          [H.IsGenerating] →
                            CategoryTheory.Limits.IsLimit (CategoryTheory.GrothendieckTopology.Cover.multifork ⟨S, ⋯⟩ P)
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.prev : ∀ (α : Type u_2) [inst : AddRightCancelSemigroup α] [inst_1 : One α] (i : α), (ComplexShape.down α).prev i = i + 1
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.coe_homeoOfIso : ∀ {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y), ⇑(AlgebraicGeometry.Scheme.homeoOfIso e) = ⇑e.hom
-- Mathlib.CategoryTheory.Sites.Sieves
/-- **Alias** of `CategoryTheory.Presieve.HasPullbacks.hasPullback`. -/
CategoryTheory.Presieve.hasPullback : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X : C} {R : CategoryTheory.Presieve X} {Y : C} (f : Y ⟶ X)
  [self : R.HasPullbacks f] {Z : C} {h : Z ⟶ X}, R h → CategoryTheory.Limits.HasPullback h f
-- Lean.Parser.Types
Lean.Parser.TokenCacheEntry.startPos : Lean.Parser.TokenCacheEntry → String.Pos.Raw
-- Mathlib.Algebra.Group.Pi.Basic
Pi.rightCancelMonoid.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → RightCancelMonoid (f i)],
  Pi.rightCancelMonoid =
    { toSemigroup := Pi.rightCancelSemigroup.toSemigroup, toOne := Pi.monoid.toOne, one_mul := ⋯, mul_one := ⋯,
      toNPow := Pi.monoid.toNPow, npow_zero := ⋯, npow_succ := ⋯, toIsRightCancelMul := ⋯ }
-- Mathlib.Combinatorics.Matroid.Closure
/-- **Alias** of `Matroid.mem_closure_sdiff_singleton_iff_closure`. -/
Matroid.mem_closure_diff_singleton_iff_closure : ∀ {α : Type u_2} {M : Matroid α} {X : Set α} {e : α},
  e ∈ X →
    autoParam (e ∈ M.E) Matroid.mem_closure_sdiff_singleton_iff_closure._auto_1 →
      (e ∈ M.closure (X \ {e}) ↔ M.closure (X \ {e}) = M.closure X)
-- Mathlib.CategoryTheory.Shift.Pullback
CategoryTheory.PullbackShift.functor.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] [inst_3 : CategoryTheory.HasShift C B] (φ : A →+ B) {D : Type u_4}
  [inst_4 : CategoryTheory.Category.{v_2, u_4} D] [inst_5 : CategoryTheory.HasShift D B]
  (F : CategoryTheory.Functor C D), CategoryTheory.PullbackShift.functor φ F = F
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DeclarationParams.mk.inj : ∀ {toTextDocumentPositionParams toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams},
  { toTextDocumentPositionParams := toTextDocumentPositionParams } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1 } →
    toTextDocumentPositionParams = toTextDocumentPositionParams_1
-- Mathlib.Algebra.Ring.Defs
/-- The canonical map `ℕ → R` is a homomorphism.  -/
NonAssocSemiring.natCast_succ : ∀ {α : Type u} [self : NonAssocSemiring α] (n : ℕ), ↑(n + 1) = ↑n + 1
-- Mathlib.ModelTheory.LanguageMap
/-- The mapping of relations  -/
FirstOrder.Language.LHom.onRelation : {L : FirstOrder.Language} → {L' : FirstOrder.Language} → (L →ᴸ L') → ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
-- Init.Data.Vector.Range
Vector.not_mem_range_self : ∀ {n : ℕ}, n ∉ Vector.range n
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.postcompPostcompIso_inv_hom_app : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} {E' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} E'] {A : Type u_5} [inst_4 : AddMonoid A]
  [inst_5 : CategoryTheory.HasShift D A] [inst_6 : CategoryTheory.HasShift E A] [inst_7 : CategoryTheory.HasShift E' A]
  (F : CategoryTheory.SingleFunctors C D A) (G : CategoryTheory.Functor D E) (G' : CategoryTheory.Functor E E')
  [inst_8 : G.CommShift A] [inst_9 : G'.CommShift A] (a : A) (x : C),
  ((F.postcompPostcompIso G G').inv.hom a).app x =
    CategoryTheory.CategoryStruct.id (G'.obj (G.obj ((F.functor a).obj x)))
-- Mathlib.Topology.ContinuousOn
/-- **Alias** of the reverse direction of `continuousWithinAt_insert_self`. -/
ContinuousWithinAt.insert : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α}
  {x : α}, ContinuousWithinAt f s x → ContinuousWithinAt f (insert x s) x
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_add_eq_left : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {x y : K},
  0 < ArchimedeanClass.mk y → ArchimedeanClass.stdPart (x + y) = ArchimedeanClass.stdPart x
-- Mathlib.GroupTheory.Congruence.Defs
/-- Given types with multiplications `M, N` and a congruence relation `c` on `N`, a
multiplication-preserving map `f : M → N` induces a congruence relation on `f`'s domain
defined by '`x ≈ y` iff `f(x)` is related to `f(y)` by `c`.'  -/
Con.comap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : Mul M] → [inst_1 : Mul N] → (f : M → N) → (∀ (x y : M), f (x * y) = f x * f y) → Con N → Con M
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The fork `biprod.sndKernelFork` is indeed a limit.  -/
CategoryTheory.Limits.biprod.isKernelSndKernelFork : {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.IsLimit (CategoryTheory.Limits.biprod.sndKernelFork X Y)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minKeyD.match_1.congr_eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → α → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α β) (x_1 : α)
  (h_1 : (fallback : α) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            (x : α) → motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α β) →
                        (fallback : α) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)
                            fallback)
  (fallback : α),
  x = Std.DTreeMap.Internal.Impl.leaf →
    x_1 = fallback →
      (match x, x_1 with
        | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
        | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_2 size k v r x
        | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
          fallback => h_3 size k v l size_1 k_1 v_1 l_1 r h r_1 fallback) ≍
        h_1 fallback
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.OplaxTrans.Hom.of.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} (as as_1 : CategoryTheory.Lax.OplaxTrans.Modification η θ),
  ({ as := as } = { as := as_1 }) = (as = as_1)
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.mul_add_right_right : ∀ {R : Type u} [inst : CommRing R] {x y : R}, IsCoprime x y → ∀ (z : R), IsCoprime x (z * x + y)
-- Std.Time.Format.Basic
Std.Time.Awareness.only.sizeOf_spec : ∀ (a : Std.Time.TimeZone), sizeOf (Std.Time.Awareness.only a) = 1 + sizeOf a
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.instUnique.eq_1 : ∀ {M : Type u_16} {N : Type u_17} [inst : Unique M] [inst_1 : Unique N] [inst_2 : Add M] [inst_3 : Add N],
  AddEquiv.instUnique = { default := AddEquiv.ofUnique, uniq := ⋯ }
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
/-- Implementation detail.  -/
AddMonoidAlgebra.rTensorEquivAlgEquiv.invFun : {R : Type u_1} →
  {M : Type u_2} →
    {S : Type u_4} →
      {A : Type u_5} →
        {B : Type u_6} →
          [inst : CommSemiring R] →
            [inst_1 : CommSemiring S] →
              [inst_2 : CommSemiring A] →
                [inst_3 : CommSemiring B] →
                  [inst_4 : Algebra R S] →
                    [inst_5 : Algebra R A] →
                      [inst_6 : Algebra R B] →
                        [inst_7 : Algebra S A] →
                          [inst_8 : IsScalarTower R S A] →
                            [inst_9 : AddCommMonoid M] →
                              AddMonoidAlgebra (TensorProduct R A B) M →ₐ[S] TensorProduct R A (AddMonoidAlgebra B M)
-- Init.Data.String.Extra
_private.Init.Data.String.Extra.0.String.removeNumLeadingSpaces : ℕ → String → String
-- Std.Time.Format.DateFormat
/-- Narrow day-period strings for the `b` pattern (AM, PM, noon, midnight).
Used by `bbbbb`.
 -/
Std.Time.DateFormatSymbols.dayPeriodNarrow : Std.Time.DateFormatSymbols → Std.Time.DayPeriodSymbols
-- Mathlib.Logic.Equiv.Set
Equiv.image_symm_apply_coe : ∀ {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set α) (y : ↑(⇑e '' s)), ↑((e.image s).symm y) = e.symm ↑y
-- Mathlib.Analysis.Complex.Trigonometric
Complex.tanh_ofReal_im : ∀ (x : ℝ), (Complex.tanh ↑x).im = 0
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {h : (t.get? k).isSome = true}, (t.get? k).get h = t.get k ⋯
-- Mathlib.Algebra.Field.Subfield.Basic
Field.FG.mk : ∀ {L : Type v} [inst : DivisionRing L], (∃ S, Subfield.closure ↑S = ⊤) → Field.FG L
-- Mathlib.Tactic.Abel
/-- `abel` solves equations in the language of *additive*, commutative monoids and groups.

`abel` and its variants work as both tactics and conv tactics.

* `abel1` fails if the target is not an equality that is provable by the axioms of
  commutative monoids/groups.
* `abel_nf` rewrites all group expressions into a normal form.
  * `abel_nf at h` rewrites in a hypothesis.
  * `abel_nf (config := cfg)` allows for additional configuration:
    * `red`: the reducibility setting (overridden by `!`).
    * `zetaDelta`: if true, local `let` variables can be unfolded (overridden by `!`).
    * `recursive`: if true, `abel_nf` also recurses into atoms.
* `abel!`, `abel1!`, `abel_nf!` use a more aggressive reducibility setting to identify atoms.

Examples:
```
example [AddCommMonoid α] (a b : α) : a + (b + a) = a + a + b := by abel
example [AddCommGroup α] (a : α) : (3 : ℤ) • a = a + (2 : ℤ) • a := by abel
```
 -/
Mathlib.Tactic.Abel.abelConv : Lean.ParserDescr
-- Std.Time.DateTime.WallTime
Std.Time.WallTime.instHSubDuration_1 : HSub Std.Time.WallTime Std.Time.WallTime Std.Time.Duration
-- Init.Data.Cast
instCoeTailNatOfNatCast : {R : Type u_1} → [NatCast R] → CoeTail ℕ R
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A functor `F : C ⥤ D` sends binary bicones for `P` and `Q`
to binary bicones for `G.obj P` and `G.obj Q` functorially.  -/
CategoryTheory.Limits.BinaryBicones.functoriality : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {D : Type uD} →
        [inst_2 : CategoryTheory.Category.{uD', uD} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (P Q : C) →
              (F : CategoryTheory.Functor C D) →
                [F.PreservesZeroMorphisms] →
                  CategoryTheory.Functor (CategoryTheory.Limits.BinaryBicone P Q)
                    (CategoryTheory.Limits.BinaryBicone (F.obj P) (F.obj Q))
-- Mathlib.Data.Set.NAry
Set.image_prod : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} (f : α → β → γ) {s : Set α} {t : Set β},
  (fun x => f x.1 x.2) '' s ×ˢ t = Set.image2 f s t
-- Mathlib.Geometry.Euclidean.Inversion.Basic
/-- The inversion of a point tends to infinity  as it approaches the center of an inversion.  -/
EuclideanGeometry.tendsto_inversion_nhdsNE_center_cobounded : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c : P} {R : ℝ},
  R ≠ 0 → Filter.Tendsto (EuclideanGeometry.inversion c R) (nhdsWithin c {c}ᶜ) (Bornology.cobounded P)
-- Aesop.Tree.Data
Aesop.RappData.metaState : {Goal MVarCluster : Type} → Aesop.RappData Goal MVarCluster → Lean.Meta.SavedState
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.comap_id : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀]
  (v : AddValuation R Γ₀), AddValuation.comap (RingHom.id R) v = v
-- Mathlib.Algebra.Ring.Associated
Associated.neg_neg : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : HasDistribNeg M] {a b : M}, Associated a b → Associated (-a) (-b)
-- Mathlib.LinearAlgebra.BilinearForm.Hom
/-- Auxiliary definition to define `toLinHom`; see below.  -/
LinearMap.BilinForm.toLinHomAux₁ : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → LinearMap.BilinForm R M → M → M →ₗ[R] R
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.sum_measure : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  [Countable ι] {μ : ι → MeasureTheory.Measure α},
  (∀ (i : ι), AEMeasurable f (μ i)) → AEMeasurable f (MeasureTheory.Measure.sum μ)
-- Mathlib.Algebra.Notation.Pi.Basic
/-- The function supported at `i`, with value `x` there, and `0` elsewhere.  -/
Pi.single : {ι : Type u_1} → {M : ι → Type u_6} → [(i : ι) → Zero (M i)] → [DecidableEq ι] → (i : ι) → M i → (j : ι) → M j
-- Mathlib.Algebra.Order.Group.Abs
mabs_le : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b : G}, |a|ₘ ≤ b ↔ b⁻¹ ≤ a ∧ a ≤ b
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.Sheafify.map_smul_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} (φ : M₀.presheaf ⟶ A.obj)
  [inst_3 : CategoryTheory.Presheaf.IsLocallyInjective J φ] [inst_4 : CategoryTheory.Presheaf.IsLocallySurjective J φ]
  {X : Cᵒᵖ} (r : ↑(R.obj.obj X)) (m : ↑(A.obj.obj X)) {Y : Cᵒᵖ} (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
  (CategoryTheory.ConcreteCategory.hom (α.app Y)) r₀ = (CategoryTheory.ConcreteCategory.hom (R.obj.map f)) r →
    ∀ (m₀ : ↑(M₀.obj Y)),
      (CategoryTheory.ConcreteCategory.hom (φ.app Y)) m₀ = (CategoryTheory.ConcreteCategory.hom (A.obj.map f)) m →
        (CategoryTheory.ConcreteCategory.hom (A.obj.map f)) (PresheafOfModules.Sheafify.smul α φ r m) =
          (CategoryTheory.ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
-- Mathlib.Algebra.Ring.Subring.Basic
/-- The subring of elements `x : R` such that `f x = g x`, i.e.,
the equalizer of f and g as a subring of R  -/
RingHom.eqLocus : {R : Type u} → [inst : NonAssocRing R] → {S : Type v} → [inst_1 : Semiring S] → (R →+* S) → (R →+* S) → Subring R
-- Mathlib.Logic.Equiv.Basic
Equiv.piCongrFiberwise_apply : ∀ {α : Type u_9} {β : Type u_10} {γ₁ : α → Type u_11} {γ₂ : β → Type u_12} {f : α → β}
  (e : (b : β) → ((σ : { a // f a = b }) → γ₁ ↑σ) ≃ γ₂ b) (g : (a : α) → γ₁ a) (b : β),
  (Equiv.piCongrFiberwise e) g b = (e b) fun σ => g ↑σ
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.K'.main.sizeOf_spec : sizeOf Turing.PartrecToTM2.K'.main = 1
-- Mathlib.Topology.Constructions.SumProd
/-- A version of `continuous_inf_dom_left` for binary functions  -/
continuous_inf_dom_left₂ : ∀ {X : Type u_5} {Y : Type u_6} {Z : Type u_7} {f : X → Y → Z} {ta1 ta2 : TopologicalSpace X}
  {tb1 tb2 : TopologicalSpace Y} {tc1 : TopologicalSpace Z},
  (Continuous fun p => f p.1 p.2) → Continuous fun p => f p.1 p.2
-- Mathlib.Topology.Connected.TotallyDisconnected
connectedComponents_lift_unique' : ∀ {α : Type u} [inst : TopologicalSpace α] {β : Sort u_3} {g₁ g₂ : ConnectedComponents α → β},
  g₁ ∘ ConnectedComponents.mk = g₂ ∘ ConnectedComponents.mk → g₁ = g₂
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.a₁_of_isCharNeTwoNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharNeTwoNF], W.a₁ = 0