mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Tactic.Exact
/-- `MetaM` version of `Lean.Elab.Tactic.evalExact`: add `mvarId := x` to the metavariable assignment.
This method wraps `Lean.MVarId.assign`, checking whether `mvarId` is already assigned, and whether
the expression has the right type.  -/
Lean.MVarId.assignIfDefEq : Lean.MVarId → Lean.Expr → Lean.MetaM Unit
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insert k v)[k] = v
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.addProjection_respects_measure : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  {ν : MeasureTheory.Measure α} (μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α)))
  [i : MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ] {t : Set α},
  MeasureTheory.IsAddFundamentalDomain G t ν →
    μ = MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict t)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Prod
CliffordAlgebra.map_mul_map_eq_neg_of_isOrtho_of_mem_evenOdd_one : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Qₙ : QuadraticForm R N} (f₁ : Q₁ →qᵢ Qₙ)
  (f₂ : Q₂ →qᵢ Qₙ),
  (∀ (x : M₁) (y : M₂), QuadraticMap.IsOrtho Qₙ (f₁ x) (f₂ y)) →
    ∀ (m₁ : CliffordAlgebra Q₁) (m₂ : CliffordAlgebra Q₂),
      m₁ ∈ CliffordAlgebra.evenOdd Q₁ 1 →
        m₂ ∈ CliffordAlgebra.evenOdd Q₂ 1 →
          (CliffordAlgebra.map f₁) m₁ * (CliffordAlgebra.map f₂) m₂ =
            -(CliffordAlgebra.map f₂) m₂ * (CliffordAlgebra.map f₁) m₁
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.isElliptic_conj_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Preorder R] {m : Matrix (Fin 2) (Fin 2) R} (g : GL (Fin 2) R),
  (↑g * m * (↑g)⁻¹).IsElliptic ↔ m.IsElliptic
-- Mathlib.RingTheory.Finiteness.Finsupp
Module.Finite.finsupp : ∀ {R : Type u_2} {V : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid V] [inst_2 : Module R V] {ι : Type u_1}
  [Finite ι] [Module.Finite R V], Module.Finite R (ι →₀ V)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_insertManyIfNewUnit_list : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} (h : t.WF) {l : List α} {k : α}
  {fallback : Unit},
  Std.DTreeMap.Internal.Impl.Const.getD (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯)) k fallback = ()
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
AlgebraicGeometry.IsIntegralHom.of_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
  [AlgebraicGeometry.IsIntegralHom (CategoryTheory.CategoryStruct.comp f g)] [AlgebraicGeometry.IsSeparated g],
  AlgebraicGeometry.IsIntegralHom f
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.refl_symm : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Add α], (OrderAddMonoidIso.refl α).symm = OrderAddMonoidIso.refl α
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.trans_symm : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ), φ.trans φ.symm = Representation.Equiv.refl ρ
-- Mathlib.Data.Multiset.Count
Multiset.count_le_count_cons : ∀ {α : Type u_1} [inst : DecidableEq α] (a b : α) (s : Multiset α), Multiset.count a s ≤ Multiset.count a (b ::ₘ s)
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.instIsFilteredI : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  (P : CategoryTheory.Limits.IndObjectPresentation A), CategoryTheory.IsFiltered P.I
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- Adding a point to a finite-dimensional subspace increases the dimension by at most one.  -/
finrank_vectorSpan_insert_le : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : AffineSubspace k P) (p : P),
  Module.finrank k ↥(vectorSpan k (insert p ↑s)) ≤ Module.finrank k ↥s.direction + 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
/-- The `Y`-coordinate of a representative of `-(P + Q)` for two distinct projective point
representatives `P` and `Q` on a Weierstrass curve.

If the representatives of `P` and `Q` are equal, then this returns the value `0`.  -/
WeierstrassCurve.Projective.negAddY : {R : Type r} → [CommRing R] → WeierstrassCurve.Projective R → (Fin 3 → R) → (Fin 3 → R) → R
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, (t.insert k v).contains k = true
-- Mathlib.Order.Interval.Set.Basic
Set.mem_Iic_Iio_of_subset_of_subset : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α} {s : Set α}, Set.Iio a ⊆ s → s ⊆ Set.Iic a → s ∈ {Set.Iic a, Set.Iio a}
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.instLaxMonoidalMonMapMon.eq_1 : ∀ {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]
  (F : CategoryTheory.Functor C D) [inst_4 : CategoryTheory.BraidedCategory C]
  [inst_5 : CategoryTheory.BraidedCategory D] [inst_6 : F.LaxBraided],
  F.instLaxMonoidalMonMapMon =
    { ε := { hom := CategoryTheory.Functor.LaxMonoidal.ε F, isMonHom_hom := ⋯ },
      μ := fun M N => { hom := CategoryTheory.Functor.LaxMonoidal.μ F M.X N.X, isMonHom_hom := ⋯ }, μ_natural_left := ⋯,
      μ_natural_right := ⋯, associativity := ⋯, left_unitality := ⋯, right_unitality := ⋯ }
-- Lean.Meta.Tactic.Induction
Lean.Meta.InductionSubgoal.subst : Lean.Meta.InductionSubgoal → Lean.Meta.FVarSubst
-- Mathlib.Algebra.FreeMonoid.Basic
_private.Mathlib.Algebra.FreeMonoid.Basic.0.FreeMonoid.prodAux.match_1.eq_1 : ∀ {M : Type u_1} (motive : List M → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (x : M) → (xs : List M) → motive (x :: xs)),
  (match [] with
    | [] => h_1 ()
    | x :: xs => h_2 x xs) =
    h_1 ()
-- Mathlib.Lean.Expr.Basic
/-- `getBinderName e` returns `some n` if `e` is an expression of the form `∀ n, ...`
and `none` otherwise.  -/
Lean.Expr.getBinderName : Lean.Expr → Lean.MetaM (Option Lean.Name)
-- Mathlib.Topology.Maps.Basic
Topology.IsClosedEmbedding.tendsto_nhds_iff : ∀ {X : Type u_1} {Y : Type u_2} {ι : Type u_4} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {g : ι → X} {l : Filter ι} {x : X},
  Topology.IsClosedEmbedding f → (Filter.Tendsto g l (nhds x) ↔ Filter.Tendsto (f ∘ g) l (nhds (f x)))
-- Mathlib.Algebra.Group.Defs
/-- An additive commutative group is an additive group with commutative `(+)`. 

[Wikidata Q181296](https://www.wikidata.org/wiki/Q181296) -/
AddCommGroup : Type u → Type u
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Split.State.mk.inj : ∀ {num : ℕ} {candidates : List Lean.Meta.Grind.SplitInfo} {added : Std.HashSet Lean.Meta.Grind.SplitInfo}
  {resolved : Lean.PHashSet Lean.Meta.Sym.ExprPtr} {trace : List Lean.Meta.Grind.CaseTrace}
  {lookaheads : List Lean.Meta.Grind.SplitInfo} {argPosMap : Std.HashMap (Lean.Expr × Lean.Expr) (List ℕ)}
  {argsAt : Lean.PHashMap (Lean.Expr × ℕ) (List Lean.Meta.Grind.SplitArg)} {num_1 : ℕ}
  {candidates_1 : List Lean.Meta.Grind.SplitInfo} {added_1 : Std.HashSet Lean.Meta.Grind.SplitInfo}
  {resolved_1 : Lean.PHashSet Lean.Meta.Sym.ExprPtr} {trace_1 : List Lean.Meta.Grind.CaseTrace}
  {lookaheads_1 : List Lean.Meta.Grind.SplitInfo} {argPosMap_1 : Std.HashMap (Lean.Expr × Lean.Expr) (List ℕ)}
  {argsAt_1 : Lean.PHashMap (Lean.Expr × ℕ) (List Lean.Meta.Grind.SplitArg)},
  { num := num, candidates := candidates, added := added, resolved := resolved, trace := trace,
        lookaheads := lookaheads, argPosMap := argPosMap, argsAt := argsAt } =
      { num := num_1, candidates := candidates_1, added := added_1, resolved := resolved_1, trace := trace_1,
        lookaheads := lookaheads_1, argPosMap := argPosMap_1, argsAt := argsAt_1 } →
    num = num_1 ∧
      candidates = candidates_1 ∧
        added = added_1 ∧
          resolved = resolved_1 ∧
            trace = trace_1 ∧ lookaheads = lookaheads_1 ∧ argPosMap = argPosMap_1 ∧ argsAt = argsAt_1
-- Lean.Compiler.InlineAttrs
Lean.Compiler.InlineAttributeKind.inlineIfReduce.sizeOf_spec : sizeOf Lean.Compiler.InlineAttributeKind.inlineIfReduce = 1
-- Mathlib.Geometry.RingedSpace.OpenImmersion
IsOpenMap.functorMap.congr_simp : ∀ {X Y : TopCat} {f : X ⟶ Y} {U V : TopologicalSpace.Opens ↑X}
  (HU : IsOpen (⇑(CategoryTheory.ConcreteCategory.hom f) '' ↑U))
  (HV : IsOpen (⇑(CategoryTheory.ConcreteCategory.hom f) '' ↑V)) (le : U ≤ V),
  IsOpenMap.functorMap HU HV le = IsOpenMap.functorMap HU HV le
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
/-- If a left Kan extension is pointwise, then evaluating it at an object is isomorphic to
taking a colimit.  -/
CategoryTheory.Functor.leftKanExtensionObjIsoColimit : {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] →
        (L : CategoryTheory.Functor C D) →
          {H : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} H] →
              (F : CategoryTheory.Functor C H) →
                [inst_3 : L.HasPointwiseLeftKanExtension F] →
                  [inst_4 : L.HasLeftKanExtension F] →
                    (X : D) →
                      (L.leftKanExtension F).obj X ≅
                        CategoryTheory.Limits.colimit ((CategoryTheory.CostructuredArrow.proj L X).comp F)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_max! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {hc : t.max! ∈ t}, t.get t.max! hc = t.max!
-- Init.Internal.Order.Basic
Lean.Order.«term⊥» : Lean.ParserDescr
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.PlausibleStep.sndYield : ∀ {m : Type w → Type w'} {β α₁ α₂ : Type w} [inst : Std.Iterator α₁ m β] [inst_1 : Std.Iterator α₂ m β]
  {it₂' : Std.IterM m β} {out : β} {it₂ : Std.IterM m β},
  it₂.IsPlausibleStep (Std.IterStep.yield it₂' out) →
    Std.Iterators.Types.Append.PlausibleStep (Std.IterM.Intermediate.appendSnd α₁ it₂)
      (Std.IterStep.yield (Std.IterM.Intermediate.appendSnd α₁ it₂') out)
-- Mathlib.Algebra.Order.Group.Lattice
sub_inf : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddLeftMono α] [AddRightMono α] (a b c : α),
  c - a ⊓ b = (c - a) ⊔ (c - b)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.MemLp.ofReal : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {K : Type u_8} [inst : RCLike K]
  {f : α → ℝ}, MeasureTheory.MemLp f p μ → MeasureTheory.MemLp (fun x => ↑(f x)) p μ
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.ext_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : TopologicalSpace.NonemptyCompacts α}, s = t ↔ ↑s = ↑t
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_union_of_subset`. -/
Set.diff_union_of_subset : ∀ {α : Type u_1} {s t : Set α}, t ⊆ s → s \ t ∪ t = s
-- Mathlib.Topology.Algebra.Monoid
/-- Construct an additive unit from limits of additive units and their negatives.  -/
Filter.Tendsto.addUnits : {ι : Type u_1} →
  {N : Type u_4} →
    [inst : TopologicalSpace N] →
      [inst_1 : AddMonoid N] →
        [ContinuousAdd N] →
          [T2Space N] →
            {f : ι → AddUnits N} →
              {r₁ r₂ : N} →
                {l : Filter ι} →
                  [l.NeBot] →
                    Filter.Tendsto (fun x => ↑(f x)) l (nhds r₁) →
                      Filter.Tendsto (fun x => ↑(-f x)) l (nhds r₂) → AddUnits N
-- Std.Async.Basic
/-- Creates a `BaseAsync` computation that immediately returns the given value.
 -/
Std.Async.BaseAsync.pure : {α : Type} → α → Std.Async.BaseAsync α
-- Mathlib.Data.Set.Image
Set.Nonempty.preimage : ∀ {α : Type u_1} {β : Type u_2} {s : Set β}, s.Nonempty → ∀ {f : α → β}, Function.Surjective f → (f ⁻¹' s).Nonempty
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.det_J : Matrix.GeneralLinearGroup.det UpperHalfPlane.J = -1
-- Mathlib.Algebra.Group.Units.Basic
IsAddUnit.sub_sub_cancel : ∀ {α : Type u} [inst : SubtractionCommMonoid α] {a b : α}, IsAddUnit a → a - (a - b) = b
-- Mathlib.Algebra.Polynomial.Eval.Defs
/-- **Alias** of `Polynomial.eval₂_finsetProd`. -/
Polynomial.eval₂_finset_prod : ∀ {R : Type u} {S : Type v} {ι : Type y} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S) (s : Finset ι)
  (g : ι → Polynomial R) (x : S), Polynomial.eval₂ f x (∏ i ∈ s, g i) = ∏ i ∈ s, Polynomial.eval₂ f x (g i)
-- Mathlib.Analysis.Normed.Field.Lemmas
TendstoLocallyUniformly.inv₀_of_disjoint : ∀ {α : Type u_1} [inst : NormedDivisionRing α] {X : Type u_4} {ι : Type u_5} [inst_1 : TopologicalSpace X]
  {F : ι → X → α} {f : X → α} {l : Filter ι},
  TendstoLocallyUniformly F f l →
    (∀ (x : X), Disjoint (Filter.map f (nhds x)) (nhds 0)) → TendstoLocallyUniformly F⁻¹ f⁻¹ l
-- Mathlib.Topology.Separation.DisjointCover
/-- If `f` is a continuous map from a profinite space to a topological space with a commutative monoid
structure, then we can approximate `f` by finite products of indicator functions of clopen sets.

(Note no compatibility is assumed between the monoid structure on `V` and the topology.)
 -/
ContinuousMap.exists_finite_sum_const_mulIndicator_approximation_of_mem_nhds_diagonal : ∀ {X : Type u_1} {V : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace V] [TotallyDisconnectedSpace X]
  [T2Space X] [CompactSpace X] {S : Set (V × V)} (f : C(X, V)) [inst_5 : CommMonoid V],
  S ∈ nhdsSet (Set.diagonal V) → ∃ n U v, ∀ (x : X), (f x, ∏ n, (↑(U n)).mulIndicator (fun x => v n) x) ∈ S
-- Mathlib.Analysis.Convex.Star
StarConvex.sub : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {x y : E} {s t : Set E}, StarConvex 𝕜 x s → StarConvex 𝕜 y t → StarConvex 𝕜 (x - y) (s - t)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.take.eq_2 : ∀ {α : Type u} (x : Stream'.Seq α) (n : ℕ),
  Stream'.Seq.take n.succ x =
    match x.destruct with
    | none => []
    | some (x, r) => x :: Stream'.Seq.take n r
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.vecMul_conjTranspose : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalSemiring α] [inst_1 : Fintype n] [inst_2 : StarRing α]
  (A : Matrix m n α) (x : n → α), Matrix.vecMul x A.conjTranspose = star (A.mulVec (star x))
-- Mathlib.Tactic.Determinant.Bird.Meta
/-- The evaluator context for the parsed determinant expression.  -/
Mathlib.Tactic.Determinant.ReifiedBirdDet.ctx : (self : Mathlib.Tactic.Determinant.ReifiedBirdDet) → Mathlib.Tactic.Determinant.Ctx self.rα
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.instIsAddMonHomWhiskerRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y Z : C} [inst_3 : CategoryTheory.AddMonObj X]
  [inst_4 : CategoryTheory.AddMonObj Y] [inst_5 : CategoryTheory.AddMonObj Z] {f : X ⟶ Y}
  [CategoryTheory.IsAddMonHom f], CategoryTheory.IsAddMonHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)
-- Init.System.IO
/-- Sets the current working directory of the calling process.  -/
IO.Process.setCurrentDir : System.FilePath → IO Unit
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
/-- The colimit cocone for the coproduct with a zero object is colimiting.  -/
CategoryTheory.Limits.binaryCofanZeroRightIsColimit : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (X : C) → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.binaryCofanZeroRight X)
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.sproj.inj : ∀ {n offset : ℕ} {x : Lean.IR.VarId} {n_1 offset_1 : ℕ} {x_1 : Lean.IR.VarId},
  Lean.IR.Expr.sproj n offset x = Lean.IR.Expr.sproj n_1 offset_1 x_1 → n = n_1 ∧ offset = offset_1 ∧ x = x_1
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.SmallCategoryOfSet.assoc : ∀ {Ω : Type w} (self : CategoryTheory.SmallCategoryOfSet Ω) {X Y Z T : ↑self.obj} (f : ↑(self.hom X Y))
  (g : ↑(self.hom Y Z)) (h : ↑(self.hom Z T)), self.comp (self.comp f g) h = self.comp f (self.comp g h)
-- Batteries.Data.List.Interleave
List.cons_interleave : ∀ {α : Type u_1} (a : α) (l₁ l₂ : List α), (a :: l₁).interleave l₂ = a :: l₂.interleave l₁
-- Lean.Parser.Term.Basic
/-- The `⋯` term denotes a term that was omitted by the pretty printer.
The presence of `⋯` in pretty printer output is controlled by the `pp.deepTerms` and `pp.proofs` options,
and these options can be further adjusted using `pp.deepTerms.threshold` and `pp.proofs.threshold`.

It is only meant to be used for pretty printing.
However, in case it is copied and pasted from the Infoview, `⋯` logs a warning and elaborates like `_`.
 -/
Lean.Parser.Term.omission : Lean.Parser.Parser
-- Mathlib.Util.PrintSorries
/-- The set of `sorry` expressions that have been found.
Note that unlabeled sorries will only be reported in the *first* declaration that uses them,
even if a later definition independently has a direct use of `sorryAx`.  -/
Mathlib.PrintSorries.State.sorries : Mathlib.PrintSorries.State → Std.HashSet Lean.Expr
-- Lean.Meta.Constructions.SparseCasesOnEq
_private.Lean.Meta.Constructions.SparseCasesOnEq.0.Lean.Meta.getSparseCasesOnEq.realize : Lean.Name → Lean.Name → Lean.MetaM Unit
-- Mathlib.LinearAlgebra.Matrix.DualNumber
/-- Matrices over dual numbers and dual numbers over matrices are isomorphic.  -/
Matrix.dualNumberEquiv : {R n : Type} →
  [inst : CommSemiring R] →
    [inst_1 : Fintype n] → [inst_2 : DecidableEq n] → Matrix n n (DualNumber R) ≃ₐ[R] DualNumber (Matrix n n R)
-- Mathlib.Order.CompleteSublattice
/-- A complete sublattice is a subset of a complete lattice that is closed under arbitrary suprema
and infima.  -/
CompleteSublattice : (α : Type u_1) → [CompleteLattice α] → Type u_1
-- Mathlib.Data.Finset.Max
Finset.max'_le_iff : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty) {x : α}, s.max' H ≤ x ↔ ∀ y ∈ s, y ≤ x
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instFromJsonDiagnosticRelatedInformation : Lean.FromJson Lean.Lsp.DiagnosticRelatedInformation
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
CategoryTheory.StrongEpiCategory.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (∀ {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f], CategoryTheory.StrongEpi f) → CategoryTheory.StrongEpiCategory C
-- Mathlib.Algebra.Torsor.Basic
Prod.fst_vadd : ∀ {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [inst : AddGroup G] [inst_1 : AddGroup G']
  [inst_2 : AddTorsor G P] [inst_3 : AddTorsor G' P'] (v : G × G') (p : P × P'), (v +ᵥ p).1 = v.1 +ᵥ p.1
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.instInhabitedDiscrInfo.default : Lean.Meta.Match.DiscrInfo
-- Mathlib.Topology.Path
/-- A path constructed from a continuous map `f` has the same underlying function.  -/
Path.coe_mk' : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (f : C(↑unitInterval, X)) (h₁ : f.toFun 0 = x)
  (h₂ : f.toFun 1 = y), ⇑{ toContinuousMap := f, source' := h₁, target' := h₂ } = ⇑f
-- Init.Prelude
/-- Throw an error with the given message and location information.  -/
Lean.Macro.throwErrorAt : {α : Type} → Lean.Syntax → String → Lean.MacroM α
-- Mathlib.Data.List.Permutation
Nat.factorial.eq_1 : Nat.factorial 0 = 1
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.instLinearOrder : {M : Type u_2} →
  [inst : AddCommMonoid M] → [inst_1 : LinearOrder M] → [IsOrderedCancelAddMonoid M] → LinearOrder (DivisibleHull M)
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.swap_comp : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq β] (f : α ↪ β) (x y : α),
  ⇑(Equiv.swap (f x) (f y)) ∘ ⇑f = ⇑f ∘ ⇑(Equiv.swap x y)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_erase_left : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : DecidableEq α] (a b : α),
  (Finset.Ico a b).erase a = Finset.Ioo a b
-- Mathlib.Data.Multiset.Defs
Multiset.le_iff_subset : ∀ {α : Type u_1} {s t : Multiset α}, s.Nodup → (s ≤ t ↔ s ⊆ t)
-- Mathlib.RingTheory.Derivation.Basic
Derivation.linearEquiv_coe_to_linearMap_comp : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M)
  {N : Type u_5} [inst_6 : AddCommMonoid N] [inst_7 : Module A N] [inst_8 : Module R N] [inst_9 : IsScalarTower R A M]
  [inst_10 : IsScalarTower R A N] (e : M ≃ₗ[A] N), ↑(e.compDer D) = ↑R ↑e ∘ₗ ↑D
-- Mathlib.Algebra.Order.IsBotOne
bot_eq_zero : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : Zero α] [IsBotZeroClass α] [inst_3 : OrderBot α], ⊥ = 0
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.InjectivePresentation.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (J : C)
  (injective : autoParam (CategoryTheory.Injective J) CategoryTheory.InjectivePresentation.injective._autoParam)
  (f : X ⟶ J) (mono : autoParam (CategoryTheory.Mono f) CategoryTheory.InjectivePresentation.mono._autoParam) (J_1 : C)
  (injective_1 : autoParam (CategoryTheory.Injective J_1) CategoryTheory.InjectivePresentation.injective._autoParam)
  (f_1 : X ⟶ J_1) (mono_1 : autoParam (CategoryTheory.Mono f_1) CategoryTheory.InjectivePresentation.mono._autoParam),
  ({ J := J, injective := injective, f := f, mono := mono } =
      { J := J_1, injective := injective_1, f := f_1, mono := mono_1 }) =
    (J = J_1 ∧ f ≍ f_1)
-- Init.Data.BitVec.Basic
BitVec.neg_eq : ∀ {w : ℕ} (x : BitVec w), x.neg = -x
-- Std.Sat.AIG.RefVecOperator.Fold
Std.Sat.AIG.RefVec.fold_lt_size_of_lt_aig_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len x : ℕ} (aig : Std.Sat.AIG α) (vec : aig.RefVec len)
  (func : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput func],
  x < aig.decls.size → x < (Std.Sat.AIG.RefVec.fold aig vec func).aig.decls.size
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.coe_mk : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₙ+ M₃) (h : ∀ (m : R) (x : M), f.toFun (m • x) = σ m • f.toFun x), ⇑{ toAddHom := f, map_smul' := h } = ⇑f
-- Init.Data.UInt.Lemmas
UInt32.mul_comm : ∀ (a b : UInt32), a * b = b * a
-- Mathlib.CategoryTheory.Monad.Algebra
/-- Given an algebra morphism whose carrier part is a monomorphism, we get an algebra monomorphism.
 -/
CategoryTheory.Monad.algebra_mono_of_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) {X Y : T.Algebra} (f : X ⟶ Y)
  [h : CategoryTheory.Mono f.f], CategoryTheory.Mono f
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.addCayley_singleton_zero : ∀ {M : Type u_1} [inst : AddZeroClass M], SimpleGraph.addCayley {0} = ⊥
-- Init.Data.Nat.Basic
_private.Init.Data.Nat.Basic.0.Nat.repeat.match_1.splitter : {α : Type u_2} →
  (motive : ℕ → α → Sort u_1) →
    (x : ℕ) → (x_1 : α) → ((a : α) → motive 0 a) → ((n : ℕ) → (a : α) → motive n.succ a) → motive x x_1
-- Mathlib.GroupTheory.Perm.Cycle.Factors
/-- Two cycles of a permutation commute.  -/
Equiv.Perm.cycleFactorsFinset_mem_commute' : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α) {g1 g2 : Equiv.Perm α},
  g1 ∈ f.cycleFactorsFinset → g2 ∈ f.cycleFactorsFinset → Commute g1 g2