mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Indization.LocallySmall
CategoryTheory.colimitYonedaHomEquiv_π_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} I]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape I (Type v)]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type v)]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u v))] (F : CategoryTheory.Functor I C)
  (G : CategoryTheory.Functor Cᵒᵖ (Type v)) (η : CategoryTheory.Limits.colimit (F.comp CategoryTheory.yoneda) ⟶ G)
  (i : Iᵒᵖ),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π (F.op.comp G) i))
      ((CategoryTheory.colimitYonedaHomEquiv F G) η) =
    (CategoryTheory.ConcreteCategory.hom (η.app (Opposite.op (F.obj (Opposite.unop i)))))
      ((CategoryTheory.ConcreteCategory.hom
          ((CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.yoneda) (Opposite.unop i)).app
            (Opposite.op (F.obj (Opposite.unop i)))))
        (CategoryTheory.CategoryStruct.id (F.obj (Opposite.unop i))))
-- Mathlib.Control.Fold
Monoid.foldrM.mk : {m : Type u → Type u} → [inst : Monad m] → {α : Type u} → (α → m α) → Monoid.foldrM m α
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.toList_eq_nil : ∀ {p : DyckWord}, ↑p = [] ↔ p = 0
-- Lean.Parser.Do
Lean.Parser.Term.doIf : Lean.Parser.Parser
-- Batteries.Util.ProofWanted
/-- Configuration distinguishing the wanted commands at the elaborator level.  -/
_private.Batteries.Util.ProofWanted.0.WantedCmdKind : Type
-- Mathlib.Topology.Algebra.GroupWithZero
/-- If a group with zero has continuous multiplication and `fun x ↦ x⁻¹` is continuous at one,
then it is continuous at any unit.  -/
ContinuousInv₀.of_nhds_one : ∀ {G₀ : Type u_3} [inst : TopologicalSpace G₀] [inst_1 : GroupWithZero G₀] [SeparatelyContinuousMul G₀],
  Filter.Tendsto Inv.inv (nhds 1) (nhds 1) → ContinuousInv₀ G₀
-- Mathlib.Analysis.Normed.Module.HahnBanach
/-- Variant of Hahn-Banach, eliminating the hypothesis that `x` be nonzero, and choosing
the dual element arbitrarily when `x = 0`.  -/
exists_dual_vector' : ∀ (𝕜 : Type v) [inst : RCLike 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [Nontrivial E]
  (x : E), ∃ g, ‖g‖ = 1 ∧ g x = ↑‖x‖
-- Mathlib.Order.Interval.Set.Nat
Set.ncard_Icc_nat : ∀ (a b : ℕ), (Set.Icc a b).ncard = b + 1 - a
-- Mathlib.Algebra.Module.Presentation.Tensor
/-- The presentation of the `A`-module `M₁ ⊗[A] M₂` that is deduced from
a presentation of `M₁` and a presentation of `M₂`.  -/
Module.Presentation.tensor : {A : Type u} →
  [inst : CommRing A] →
    {M₁ : Type v₁} →
      {M₂ : Type v₂} →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : AddCommGroup M₂] →
            [inst_3 : Module A M₁] →
              [inst_4 : Module A M₂] →
                Module.Presentation A M₁ → Module.Presentation A M₂ → Module.Presentation A (TensorProduct A M₁ M₂)
-- Mathlib.Order.CompleteBooleanAlgebra
/-- The `CompleteDistribLattice.MinimalAxioms` element corresponding to a complete distrib lattice.
 -/
CompleteDistribLattice.MinimalAxioms.of : ∀ {α : Type u} [inst : CompleteDistribLattice α], CompleteDistribLattice.MinimalAxioms α
-- Mathlib.SetTheory.Lists
Finsets.instEmptyCollection : {α : Type u_1} → EmptyCollection (Finsets α)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_eq_none : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α}, a ∉ m → m.get? a = none
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.map_boundedFormula : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.ElementaryEmbedding M N) {α : Type u_5} {n : ℕ} (φ : L.BoundedFormula α n) (v : α → M) (xs : Fin n → M),
  φ.Realize (⇑f ∘ v) (⇑f ∘ xs) ↔ φ.Realize v xs
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.mk : ∀ {α : Type u_1} {C : Set (Set α)},
  ∅ ∈ C →
    (∀ s ∈ C, ∀ t ∈ C, s ∩ t ∈ C) →
      (∀ s ∈ C, ∀ t ∈ C, ∃ I, ↑I ⊆ C ∧ (↑I).PairwiseDisjoint id ∧ s \ t = ⋃₀ ↑I) → MeasureTheory.IsSetSemiring C
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey_le_maxKey_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k} {he : t.isEmpty = false},
  (compare (t.maxKey he) ((Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.maxKey ⋯)).isLE = true
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.gc_map_comap : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_1}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f : F),
  GaloisConnection (NonUnitalSubsemiring.map f) (NonUnitalSubsemiring.comap f)
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.listDecode.eq_4 : ∀ {L : FirstOrder.Language} {α : Type u'} (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
  FirstOrder.Language.BoundedFormula.listDecode (Sum.inr (Sum.inr 0) :: l) =
    if h : 2 ≤ (FirstOrder.Language.BoundedFormula.listDecode l).length then
      FirstOrder.Language.BoundedFormula.sigmaImp (FirstOrder.Language.BoundedFormula.listDecode l)[0]
          (FirstOrder.Language.BoundedFormula.listDecode l)[1] ::
        List.drop 2 (FirstOrder.Language.BoundedFormula.listDecode l)
    else []
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- Two matrices agree if their columns agree.  -/
Matrix.ext_col : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {A B : Matrix m n α}, (∀ (j : n), A.col j = B.col j) → A = B
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
/-- Given a matrix with unit determinant, we get an element of `GL n R`.  -/
Matrix.GeneralLinearGroup.mk'' : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] → {R : Type v} → [inst_2 : CommRing R] → (A : Matrix n n R) → IsUnit A.det → GL n R
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.add_zero : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (x : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F (x.add RingCat.Colimits.Prequotient.zero) x
-- Mathlib.Probability.Kernel.WithDensity
ProbabilityTheory.Kernel.withDensity.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ κ_1 : ProbabilityTheory.Kernel α β)
  (e_κ : κ = κ_1) [inst : ProbabilityTheory.IsSFiniteKernel κ] (f f_1 : α → β → ENNReal),
  f = f_1 → κ.withDensity f = κ_1.withDensity f_1
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
/-- Given `A : Rep k G` and a chain complex `P` in `Rep k G`, this is the chain complex whose
`n`th object is `(A ⊗ Pₙ)_G`.  -/
HomologicalComplex.coinvariantsTensorObj : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      {α : Type u_1} →
        [inst_2 : AddRightCancelSemigroup α] →
          [inst_3 : One α] → Rep.{u, u, u} k G → ChainComplex (Rep.{u, u, u} k G) α → ChainComplex (ModuleCat k) α
-- Mathlib.RingTheory.Grassmannian
Module.Grassmannian.functor_map : ∀ {R : Type u} [inst : CommRing R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (k : ℕ)
  {X Y : CommAlgCat R} (f : X ⟶ Y),
  (Module.Grassmannian.functor k).map f = TypeCat.ofHom (Module.Grassmannian.map (CommAlgCat.Hom.hom f))
-- Mathlib.Algebra.Group.Finsupp
/-- `Finsupp.erase` as an `AddMonoidHom`.  -/
Finsupp.eraseAddHom : {ι : Type u_1} → {M : Type u_3} → [inst : AddZeroClass M] → ι → (ι →₀ M) →+ ι →₀ M
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyι_descOpcycles_eq_zero_of_boundary_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} [inst_2 : S.HasHomology] (k : S.X₂ ⟶ A) (x : S.X₃ ⟶ A)
  (hx : k = CategoryTheory.CategoryStruct.comp S.g x) {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.homologyι (CategoryTheory.CategoryStruct.comp (S.descOpcycles k ⋯) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Batteries.Data.Fin.Coding
Fin.decodeSigma.eq_def : ∀ {n : ℕ} (f : Fin n → ℕ) (x : Fin (Fin.sum f)),
  Fin.decodeSigma f x =
    match n, f, x with
    | 0, x, ⟨val, h⟩ => ⋯.elim
    | n.succ, f, ⟨x, hx⟩ =>
      if hx0 : x < f 0 then ⟨0, ⟨x, hx0⟩⟩
      else
        have hxf := ⋯;
        match Fin.decodeSigma (fun x => f x.succ) ⟨x - f 0, hxf⟩ with
        | ⟨⟨i, hi⟩, y⟩ => ⟨⟨i + 1, ⋯⟩, y⟩
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.instIsGEObjTruncGTHSubIntOfNat : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C), t.IsGE ((t.truncGT (n - 1)).obj X) n
-- Init.Data.List.Nat.Basic
_private.Init.Data.List.Nat.Basic.0.List.eraseIdx.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → ℕ → Sort u_2) (x : ℕ) (h_1 : (x : ℕ) → motive [] x)
  (h_2 : (head : α) → (as : List α) → motive (head :: as) 0)
  (h_3 : (a : α) → (as : List α) → (n : ℕ) → motive (a :: as) n.succ),
  (match [], x with
    | [], x => h_1 x
    | head :: as, 0 => h_2 head as
    | a :: as, n.succ => h_3 a as n) =
    h_1 x
-- Mathlib.Data.Nat.Bitwise
Nat.xor_one_of_odd : ∀ {n : ℕ}, Odd n → n ^^^ 1 = n - 1
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.coeCarrier : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → CoeOut (AlgebraicGeometry.PresheafedSpace C) TopCat
-- Mathlib.Topology.Order.Compact
IsCompact.exists_isMinOn_mem_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
  [ClosedIicTopology α] {f : β → α} {s t : Set β} {z : β},
  IsCompact t → ContinuousOn f t → z ∈ t → (∀ z' ∈ t \ s, f z < f z') → ∃ x ∈ s, IsMinOn f t x
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.edist_bot : ∀ {V : Type u_1} {u v : V} [inst : DecidableEq V], ⊥.edist u v = if u = v then 0 else ⊤
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- The category of based categories.  -/
CategoryTheory.BasedCategory.instCategory : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    CategoryTheory.Category.{max u₂ v₂, max (max (max (u₂ + 1) (v₂ + 1)) u₁) v₁} (CategoryTheory.BasedCategory 𝒮)
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.LetRecClosure.toLift : Lean.Elab.Term.MutualClosure.LetRecClosure → Lean.Elab.Term.LetRecToLift
-- Mathlib.CategoryTheory.Yoneda
/-- The Yoneda embedding, as a functor from `C` into presheaves on `C`.  -/
CategoryTheory.yoneda : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor C (CategoryTheory.Functor Cᵒᵖ (Type v₁))
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Affine.CoordinateRing.mk_ψ₂_sq : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R),
  (WeierstrassCurve.Affine.CoordinateRing.mk W) W.ψ₂ ^ 2 =
    (WeierstrassCurve.Affine.CoordinateRing.mk W) (Polynomial.C W.Ψ₂Sq)
-- Mathlib.Order.WithBot
WithTop.map₂_coe_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : WithTop β),
  WithTop.map₂ f (↑a) b = WithTop.map (fun b => f a b) b
-- Mathlib.CategoryTheory.Elements
CategoryTheory.NatTrans.mapElements_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C (Type w)} (φ : F ⟶ G)
  {p q : F.Elements} (x : p ⟶ q),
  (CategoryTheory.NatTrans.mapElements φ).map x =
    match x with
    | ⟨f, h⟩ => ⟨f, ⋯⟩
-- Mathlib.Tactic.CrossRefAttribute
/-- The formatter for LMFDB identifier syntax.  -/
Lean.PrettyPrinter.Formatter.lmfdbIdNoAntiquot.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Order.Monotone.Basic
MonotoneOn.strictMonoOn_iff_injOn : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : PartialOrder β] {f : α → β} {s : Set α},
  MonotoneOn f s → (StrictMonoOn f s ↔ Set.InjOn f s)
-- Init.Data.Fin.Lemmas
Fin.castSucc_succ : ∀ {n : ℕ} (i : Fin n), i.succ.castSucc = i.castSucc.succ
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.ServerInfo.mk.sizeOf_spec : ∀ (name : String) (version? : Option String),
  sizeOf { name := name, version? := version? } = 1 + sizeOf name + sizeOf version?
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasPosAssignment : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Bool
-- Mathlib.Order.CompleteLattice.Basic
iInf_le_iInf_of_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {s t : Set β},
  s ⊆ t → ⨅ x ∈ t, f x ≤ ⨅ x ∈ s, f x
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.MVarValue.mvarId.injEq : ∀ (mvarId mvarId_1 : Lean.MVarId),
  (Aesop.EqualUpToIds.MVarValue.mvarId mvarId = Aesop.EqualUpToIds.MVarValue.mvarId mvarId_1) = (mvarId = mvarId_1)
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.mono_left : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μa μa' : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β},
  MeasureTheory.Measure.QuasiMeasurePreserving f μa μb →
    μa'.AbsolutelyContinuous μa → MeasureTheory.Measure.QuasiMeasurePreserving f μa' μb
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.Hom.hom.eq_1 : ∀ {X Y : AddSemigrp} (f : X.Hom Y), f.hom = CategoryTheory.ConcreteCategory.hom f
-- Init.Data.String.Lemmas.Pattern.Find.String
String.contains_string_eq_false_iff : ∀ {t s : String}, s.contains t = false ↔ ¬t.toList <:+: s.toList
-- Init.Data.Order.PackageFactories
Std.Packages.LinearPreorderOfOrdArgs.decidableLE : {α : Type u} →
  (self : Std.Packages.LinearPreorderOfOrdArgs α) →
    let this := self.ord;
    let this := self.le;
    have this_1 := ⋯;
    DecidableLE α
-- Mathlib.CategoryTheory.Shift.Quotient
CategoryTheory.Quotient.liftCommShift_compatibility : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D) (r : HomRel C) (A : Type w) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : r.IsCompatibleWithShift A]
  [inst_6 : F.CommShift A] (hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂),
  CategoryTheory.NatTrans.CommShift (CategoryTheory.Quotient.lift.isLift r F hF).hom A
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
/-- `toIdeal : HomogeneousIdeal 𝒜 → Ideal A` and `Ideal.homogeneousCore 𝒜` forms a Galois
coinsertion.  -/
Ideal.homogeneousCore.gi : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : DecidableEq ι] →
          [inst_2 : AddMonoid ι] →
            [inst_3 : SetLike σ A] →
              [inst_4 : AddSubmonoidClass σ A] →
                (𝒜 : ι → σ) →
                  [inst_5 : GradedRing 𝒜] → GaloisCoinsertion HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.edgeSet_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  (SimpleGraph.Walk.cons h p).edgeSet = insert s(u, v) p.edgeSet
-- Mathlib.Algebra.Order.Module.Defs
MulPosReflectLT.toSMulPosReflectLT : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Mul α] [inst_2 : Preorder α] [MulPosReflectLT α], SMulPosReflectLT α α
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.mem_bihimp_iff : ∀ {α : Type u_1} {s t : Finset α} [inst : Fintype α] [inst_1 : DecidableEq α] {a : α}, a ∈ bihimp s t ↔ (a ∈ s ↔ a ∈ t)
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- A morphism `f : X ⟶ Y` induces a functor `Over X ⥤ Over Y` in the obvious way.  -/
CategoryTheory.Over.map : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X Y : T} → (X ⟶ Y) → CategoryTheory.Functor (CategoryTheory.Over X) (CategoryTheory.Over Y)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_filter_eq_false_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {f : (a : α) → β a → Bool},
  m.WF → ((Std.DHashMap.Raw.filter f m).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ m), f k (m.get k h) = true)
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_right_split : Int.Internal.Linear.Context → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → ℕ → Prop
-- Init.MethodSpecsSimp
Div.div_eq_hDiv : ∀ {α : Type u_1} [inst : Div α], Div.div = HDiv.hDiv
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.MVarErrorKind.implicitArg.sizeOf_spec : ∀ (lctx : Lean.LocalContext) (ctx : Lean.Expr),
  sizeOf (Lean.Elab.Term.MVarErrorKind.implicitArg lctx ctx) = 1 + sizeOf lctx + sizeOf ctx
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.boundary.ι_ι : ∀ {n : ℕ} (i : Fin (n + 2)),
  CategoryTheory.CategoryStruct.comp (SSet.boundary.ι i) (SSet.boundary (n + 1)).ι = SSet.stdSimplex.δ i
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- A simple graph having no vertices is contained in any simple graph.  -/
SimpleGraph.IsContained.of_isEmpty : ∀ {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} [IsEmpty α], A.IsContained B
-- Mathlib.Data.List.Chain
List.isChain_isInfix : ∀ {α : Type u_1} (l : List α), List.IsChain (fun x y => [x, y] <:+: l) l
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono_attachCells_isColimit₁ : ∀ {X Y : SSet} (i : X ⟶ Y) [inst : CategoryTheory.Mono i] (d : ℕ) (x : ¬IsMax d),
  ((SSet.relativeCellComplexOfMono i).attachCells d x).isColimit₁ =
    CategoryTheory.Limits.coproductIsCoproduct fun i => (SSet.boundary d).toSSet
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey_beq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} (h : k ∈ m), (m.getKey k h == k) = true
-- Mathlib.Algebra.Homology.Homotopy
_private.Mathlib.Algebra.Homology.Homotopy.0.Homotopy.mkInductiveAux₁.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → (Unit → motive 1) → ((n : ℕ) → motive n.succ.succ) → motive x
-- Mathlib.Algebra.Exact.Basic
/-- Two maps `f : M → N` and `g : N → P` are exact if and only if the induced maps
`Set.range f → N → Set.range g` are exact.

Note that if you already have an instance `[One (Set.range g)]` (which is unlikely) this lemma
may not apply if the one of `Set.range g` is not definitionally equal to `⟨1, hg⟩`.  -/
Function.MulExact.iff_rangeFactorization : ∀ {M : Type u_2} {N : Type u_4} {P : Type u_6} {f : M → N} {g : N → P} [inst : One P] (hg : 1 ∈ Set.range g),
  Function.MulExact f g ↔ Function.MulExact Subtype.val (Set.rangeFactorization g)
-- Mathlib.Data.List.Sublists
List.sublistsLenAux.eq_3 : ∀ {α : Type u} {β : Type v} (x : List α → β) (x_1 : List β) (n : ℕ) (a : α) (l : List α),
  List.sublistsLenAux n.succ (a :: l) x x_1 =
    List.sublistsLenAux (n + 1) l x (List.sublistsLenAux n l (x ∘ List.cons a) x_1)
-- Mathlib.Data.Finite.Defs
finite_or_infinite : ∀ (α : Sort u_3), Finite α ∨ Infinite α
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.instNontrivialId : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] [Nontrivial M₁], Nontrivial (M₁ →L[R₁] M₁)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- The sum `∑ (l - x)⁻ʳ` over `l ∈ L`. This converges when `2 < r`, see `hasSum_sumInvPow`.  -/
PeriodPair.sumInvPow : PeriodPair → ℂ → ℕ → ℂ
-- Mathlib.RingTheory.OrderOfVanishing.Basic
/-- Variation of `ord_mul` where the user has to show the first input is a non
zero divisor rather than the second.
 -/
Ring.ord_mul' : ∀ (R : Type u_1) [inst : CommRing R] {a b : R}, a ∈ nonZeroDivisors R → Ring.ord R (a * b) = Ring.ord R a + Ring.ord R b
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
abs_fst_of_mem_pi_polarCoord_target : ∀ {ι : Type u_1} {p : ι → ℝ × ℝ}, (p ∈ Set.univ.pi fun x => polarCoord.target) → ∀ (i : ι), |(p i).1| = (p i).1
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- `e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`.  -/
ContinuousMulEquiv.apply_symm_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (e : M ≃ₜ* N) (y : N), e (e.symm y) = y
-- Init.Data.String.Bootstrap
String.Internal.posOf : String → Char → String.Pos.Raw
-- Mathlib.Analysis.Complex.CoveringMap
isQuotientCoveringMap_zpow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [ProperSpace 𝕜] (n : ℤ),
  ↑n ≠ 0 → (Function.Surjective fun x => x ^ n) → IsQuotientCoveringMap (fun x => x ^ n) ↥(zpowGroupHom n).ker
-- Std.Data.Iterators.Lemmas.Producers.Vector
Std.Iterators.Vector.isPlausibleStep_iterFromIdx_of_lt : ∀ {β : Type w} {n : ℕ} {xs : Vector β n} {pos : ℕ} (h : pos < n),
  (xs.iterFromIdx pos).IsPlausibleStep (Std.IterStep.yield (xs.iterFromIdx (pos + 1)) xs[pos])
-- Mathlib.Order.Interval.Basic
NonemptyInterval.mem_coe_interval : ∀ {α : Type u_1} [inst : PartialOrder α] {s : NonemptyInterval α} {x : α}, x ∈ ↑s ↔ x ∈ s
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.hom_inv_id_toNatTrans : ∀ {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G),
  CategoryTheory.CategoryStruct.comp e.hom.toNatTrans e.inv.toNatTrans = CategoryTheory.CategoryStruct.id F.toFunctor
-- Mathlib.Data.Seq.Computation
/-- Recursor based on assertion of `Terminates`  -/
Computation.terminatesRecOn : {α : Type u} →
  {C : Computation α → Sort v} →
    (s : Computation α) →
      [s.Terminates] → ((a : α) → C (Computation.pure a)) → ((s : Computation α) → C s → C s.think) → C s
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.HasSubst.add : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {f g : MvPowerSeries τ R},
  PowerSeries.HasSubst f → PowerSeries.HasSubst g → PowerSeries.HasSubst (f + g)
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.Truncated.StrictSegal.mk.inj : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)}
  {spineToSimplex :
    (m : ℕ) →
      (h : autoParam (m ≤ n + 1) SSet.Truncated.StrictSegal._auto_1) →
        X.Path m → X.obj (Opposite.op { obj := { len := m }, property := h })}
  {spine_spineToSimplex : ∀ (m : ℕ) (h : m ≤ n + 1), X.spine m h ∘ spineToSimplex m ⋯ = id}
  {spineToSimplex_spine : ∀ (m : ℕ) (h : m ≤ n + 1), spineToSimplex m ⋯ ∘ X.spine m h = id}
  {spineToSimplex_1 :
    (m : ℕ) →
      (h : autoParam (m ≤ n + 1) SSet.Truncated.StrictSegal._auto_1) →
        X.Path m → X.obj (Opposite.op { obj := { len := m }, property := h })}
  {spine_spineToSimplex_1 : ∀ (m : ℕ) (h : m ≤ n + 1), X.spine m h ∘ spineToSimplex_1 m ⋯ = id}
  {spineToSimplex_spine_1 : ∀ (m : ℕ) (h : m ≤ n + 1), spineToSimplex_1 m ⋯ ∘ X.spine m h = id},
  { spineToSimplex := spineToSimplex, spine_spineToSimplex := spine_spineToSimplex,
        spineToSimplex_spine := spineToSimplex_spine } =
      { spineToSimplex := spineToSimplex_1, spine_spineToSimplex := spine_spineToSimplex_1,
        spineToSimplex_spine := spineToSimplex_spine_1 } →
    spineToSimplex = spineToSimplex_1
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycleOn.pow_apply_eq_pow_apply : ∀ {α : Type u_2} {f : Equiv.Perm α} {a : α} {s : Finset α},
  f.IsCycleOn ↑s → a ∈ s → ∀ {m n : ℕ}, (f ^ m) a = (f ^ n) a ↔ m ≡ n [MOD s.card]
-- Init.Data.Int.Basic
/-- Non-truncating subtraction of two natural numbers.

Examples:
* `Int.subNatNat 5 2 = 3`
* `Int.subNatNat 2 5 = -3`
* `Int.subNatNat 0 13 = -13`
 -/
Int.subNatNat : ℕ → ℕ → ℤ
-- Lean.Environment
Lean.instOrdOLeanLevel : Ord Lean.OLeanLevel
-- Mathlib.RingTheory.Ideal.MinimalPrime.Basic
Ideal.minimalPrimes_top : ∀ {R : Type u_1} [inst : CommSemiring R], ⊤.minimalPrimes = ∅
-- Mathlib.Tactic.Core
Mathlib.Tactic.usingArg : Lean.ParserDescr