mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.JacobsonSpace
/-- The set of closed points.  -/
closedPoints : (X : Type u_1) → [TopologicalSpace X] → Set X
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.EffectiveEpiStruct.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f : Y ⟶ X} [inst_1 : SizeOf C]
  (desc :
    {W : C} →
      (e : Y ⟶ W) →
        (∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
            CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
              CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e) →
          (X ⟶ W))
  (fac :
    ∀ {W : C} (e : Y ⟶ W)
      (h :
        ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
          CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
            CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e),
      CategoryTheory.CategoryStruct.comp f (desc e ⋯) = e)
  (uniq :
    ∀ {W : C} (e : Y ⟶ W)
      (h :
        ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
          CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
            CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e)
      (m : X ⟶ W), CategoryTheory.CategoryStruct.comp f m = e → m = desc e ⋯),
  sizeOf { desc := desc, fac := fac, uniq := uniq } = 1
-- Init.Data.List.Basic
List.zipWith_nil_left : ∀ {α : Type u} {β : Type v} {γ : Type w} {l : List β} {f : α → β → γ}, List.zipWith f [] l = []
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.inv_eq : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (a : α) (v₁ v : ℚ),
  (v == v₁⁻¹) = true → a = Lean.Grind.Field.NormNum.ofRat v₁ → a⁻¹ = Lean.Grind.Field.NormNum.ofRat v
-- Mathlib.Topology.Algebra.Group.Basic
nhds_zero_symm' : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G],
  Filter.map Neg.neg (nhds 0) = nhds 0
-- Mathlib.Algebra.Group.Basic
zsmul_add : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b : α) (n : ℤ), n • (a + b) = n • a + n • b
-- Init.Data.List.Basic
List.dropLast_cons₂ : ∀ {α : Type u_1} {x y : α} {zs : List α}, (x :: y :: zs).dropLast = x :: (y :: zs).dropLast
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.of_addEquivOfAddEquiv : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {T : AddSubmonoid P} {Q : Type u_4} [inst_3 : AddCommMonoid Q]
  {k : T.LocalizationMap Q} {j : M ≃+ P} (H : AddSubmonoid.map j.toAddMonoidHom S = T),
  (f.ofAddEquivOfLocalizations (f.addEquivOfAddEquiv k H)).toAddMonoidHom = k.toAddMonoidHom.comp j.toAddMonoidHom
-- Mathlib.Topology.MetricSpace.IsometricSMul
Multiplicative.isIsometricSMul : ∀ {M : Type u_2} {X : Type u_3} [inst : VAdd M X] [inst_1 : PseudoEMetricSpace X] [IsIsometricVAdd M X],
  IsIsometricSMul (Multiplicative M) X
-- Mathlib.Algebra.Group.Units.Defs
one_divp : ∀ {α : Type u} [inst : Monoid α] (u : αˣ), 1 /ₚ u = ↑u⁻¹
-- Mathlib.Topology.UnitInterval
unitInterval.image_coe_preimage_symm : ∀ {s : Set ↑unitInterval}, Subtype.val '' unitInterval.symm ⁻¹' s = (fun x => 1 - x) ⁻¹' Subtype.val '' s
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapIso_unitIso_inv_app_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S S' : D} {T : CategoryTheory.Functor C D} (i : S ≅ S')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) T),
  ((CategoryTheory.StructuredArrow.mapIso i).unitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.FieldTheory.Relrank
Subfield.relrank_inf_mul_relrank : ∀ {E : Type v} [inst : Field E] (A B C : Subfield E), A.relrank (B ⊓ C) * B.relrank C = (A ⊓ B).relrank C
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Decl.instantiateParamsLevelParams : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Decl pu → List Lean.Level → Array (Lean.Compiler.LCNF.Param pu)
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.bif_eq_not_bif' : ∀ {w : ℕ} (d : Bool) (a b c : BitVec w),
  ((bif d then a else c) == ~~~bif d then b else c) = bif d then a == ~~~b else c == ~~~c
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitAnchorRefInfo.ordinal : Lean.Meta.Grind.SplitAnchorRefInfo → ℕ
-- Mathlib.RingTheory.IsTensorProduct
Algebra.pushoutDesc_left : ∀ {R : Type u_1} {S : Type v₃} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {R' : Type u_6}
  (S' : Type u_7) [inst_3 : CommSemiring R'] [inst_4 : CommSemiring S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S']
  [inst_7 : Algebra R' S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S']
  [inst_11 : Algebra.IsPushout R S R' S'] {A : Type u_8} [inst_12 : Semiring A] [inst_13 : Algebra R A] (f : S →ₐ[R] A)
  (g : R' →ₐ[R] A) (H : ∀ (x : S) (y : R'), f x * g y = g y * f x) (x : S),
  (Algebra.pushoutDesc S' f g H) ((algebraMap S S') x) = f x
-- Mathlib.Analysis.InnerProductSpace.TwoDim
/-- For a nonzero vector `x` in an oriented two-dimensional real inner product space `E`,
`![x, J x]` forms an (orthogonal) basis for `E`.  -/
Orientation.basisRightAngleRotation : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] →
      [Fact (Module.finrank ℝ E = 2)] → Orientation ℝ E (Fin 2) → (x : E) → x ≠ 0 → Module.Basis (Fin 2) ℝ E
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The canonical linear map interpreting `s ∈ M_f` as a section of the structure sheaf
on the basic open defined by `f ∈ R`.  -/
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.toBasicOpenₗ : (R M : Type u) →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] →
        (f : R) →
          LocalizedModule.Away f M →ₗ[R]
            (AlgebraicGeometry.structureSheafInType R M).obj.obj (Opposite.op (PrimeSpectrum.basicOpen f))
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.instEquivLike : {α : Type u} → {β : Type v} → [inst : PseudoEMetricSpace α] → [inst_1 : PseudoEMetricSpace β] → EquivLike (α ≃ᵢ β) α β
-- Mathlib.RingTheory.Adjoin.PowerBasis
/-- Let `B : PowerBasis S A` be such that `IsIntegral R B.gen`, and let `x y : A` be elements with
integral coordinates in the base `B.basis`. Then `IsIntegral R ((B.basis.repr (x * y) i)` for all
`i` if `minpoly S B.gen = (minpoly R B.gen).map (algebraMap R S)`. This is the case if `R` is a GCD
domain and `S` is its fraction ring.  -/
PowerBasis.repr_mul_isIntegral : ∀ {S : Type u_2} [inst : CommRing S] {R : Type u_3} [inst_1 : CommRing R] [inst_2 : Algebra R S] {A : Type u_4}
  [inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] {B : PowerBasis S A},
  IsIntegral R B.gen →
    ∀ {x y : A},
      (∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)) →
        (∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr y) i)) →
          minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen) →
            ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr (x * y)) i)
-- Mathlib.Order.WithBot
WithTop.lt_iff_exists_coe : ∀ {α : Type u_1} [inst : LT α] {x y : WithTop α}, y < x ↔ ∃ b, y = ↑b ∧ ↑b < x
-- Mathlib.Data.PNat.Xgcd
/-- The map `v` gives the product of the matrix
`[[w, x], [y, z]] = [[wp + 1, x], [y, zp + 1]]`
and the vector `[a, b] = [ap + 1, bp + 1]`.  The map
`vp` gives `[sp, tp]` such that `v = [sp + 1, tp + 1]`.
 -/
PNat.XgcdType.vp : PNat.XgcdType → ℕ × ℕ
-- Mathlib.Order.Filter.Map
Filter.map_sumElim_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (l : Filter (α ⊕ β)) (m₁ : α → γ) (m₂ : β → γ),
  Filter.map (Sum.elim m₁ m₂) l = Filter.map m₁ (Filter.comap Sum.inl l) ⊔ Filter.map m₂ (Filter.comap Sum.inr l)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int32.reduceLE : Lean.Meta.Simp.Simproc
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_neg : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] (a : M),
  ArchimedeanClass.mk (-a) = ArchimedeanClass.mk a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.insertMany_cons : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} (h : t.WF)
  {l : List ((a : α) × β a)} {k : α} {v : β k},
  ↑(t.insertMany (⟨k, v⟩ :: l) ⋯) = ↑((Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.insertMany l ⋯)
-- Mathlib.Algebra.Category.ModuleCat.Abelian
ModuleCat.forget₂_reflectsLimitsOfSize : ∀ {R : Type u} [inst : Ring R],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{v, v, max v w, max v w, max (max u (v + 1)) (w + 1), max (v + 1) (w + 1)}
    (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
log_deriv_riemannZeta_add_inv_sub_sub_isLittleO : (fun s => deriv riemannZeta s / riemannZeta s + (s - 1)⁻¹ - ↑Real.eulerMascheroniConstant) =o[nhdsWithin 1 {1}ᶜ]
  fun x => 1
-- Std.Data.HashSet.Raw
/-- Creates a hash set from an array of elements. Note that unlike repeatedly calling `insert`, if the
collection contains multiple elements that are equal (with regard to `==`), then the last element
in the collection will be present in the returned hash set.
 -/
Std.HashSet.Raw.ofArray : {α : Type u} → [BEq α] → [Hashable α] → Array α → Std.HashSet.Raw α
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndep_of_condIndep_of_le_right : ∀ {Ω : Type u_1} {m' m₁ m₂ m₃ mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ → m₃ ≤ m₂ → ProbabilityTheory.CondIndep m' m₁ m₃ hm' μ
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.get?_congr : ∀ {α : Type u} {s t : Stream'.WSeq α}, s ~ʷ t → ∀ (n : ℕ), (s.get? n).Equiv (t.get? n)
-- Mathlib.RingTheory.IsTensorProduct
IsBaseChange.of_lift_unique : ∀ {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] (f : M →ₗ[R] N),
  (∀ (Q : Type (max v₁ v₂ v₃)) [inst_9 : AddCommMonoid Q] [inst_10 : Module R Q] [inst_11 : Module S Q]
      [inst_12 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g) →
    IsBaseChange S f
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.dvd_antisymm : ∀ {a b : Ordinal.{u_4}}, a ∣ b → b ∣ a → a = b
-- Mathlib.CategoryTheory.Shift.Basic
/-- A category has a shift indexed by an additive monoid `A`
if there is a monoidal functor from `A` to `C ⥤ C`.  -/
CategoryTheory.HasShift : (C : Type u) → (A : Type u_2) → [CategoryTheory.Category.{v, u} C] → [AddMonoid A] → Type (max (max u u_2) v)
-- Mathlib.Order.Category.BddLat
/-- Typecheck a `BoundedLatticeHom` as a morphism in `BddLat`.  -/
BddLat.ofHom : {X Y : Type u} →
  [inst : Lattice X] →
    [inst_1 : BoundedOrder X] →
      [inst_2 : Lattice Y] → [inst_3 : BoundedOrder Y] → BoundedLatticeHom X Y → (BddLat.of X ⟶ BddLat.of Y)
-- Mathlib.Topology.EMetricSpace.Defs
/-- Reformulation of the uniform structure in terms of the extended distance  -/
uniformity_edist : ∀ {γ : Type w} [inst : EMetricSpace γ], uniformity γ = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | edist p.1 p.2 < ε}
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- Auxiliary definition for `lift`.  -/
_private.Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense.0.CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.liftAux : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              {A : Type u'} →
                [inst_2 : CategoryTheory.Category.{v', u'} A] →
                  [CategoryTheory.Functor.IsDenseSubsite J₀ J F] →
                    {data : (X : C) → F.OneHypercoverDenseData J₀ J X} →
                      {G : CategoryTheory.Functor Cᵒᵖ A} →
                        CategoryTheory.Presheaf.IsSheaf J₀ (F.op.comp G) →
                          {X : C} →
                            {S : J.Cover X} →
                              (s : CategoryTheory.Limits.Multifork (S.index G)) →
                                (i : (data X).I₀) → s.pt ⟶ G.obj (Opposite.op (F.obj ((data X).X i)))
-- Mathlib.Probability.Process.PartitionFiltration
ProbabilityTheory.measurableSet_partitionFiltration_of_mem : ∀ {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ (n : ℕ), MeasurableSet (t n)) (n : ℕ) {s : Set α},
  s ∈ memPartition t n → MeasurableSet s
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Algebra.ker_algebraMap_isMaximal_of_isIntegral : ∀ (R : Type u_1) [inst : CommRing R] (k : Type u_6) [inst_1 : Field k] [inst_2 : Algebra R k] [Algebra.IsIntegral R k],
  (RingHom.ker (algebraMap R k)).IsMaximal
-- Mathlib.Data.Sigma.Order
/-- The lexicographical `<` on a sigma type.  -/
Sigma.Lex.LT : {ι : Type u_1} → {α : ι → Type u_2} → [LT ι] → [(i : ι) → LT (α i)] → LT (Σₗ (i : ι), α i)
-- Std.Do.Triple.SpecLemmas
Std.Do.Iter.foldM_mapM : ∀ {ps : Std.Do.PostShape} {α β γ δ : Type w} {n : Type w → Type w''} {o : Type w → Type w'''}
  [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n]
  [WeaklyLawfulMonadAttach n] [inst_6 : Monad o] [LawfulMonad o] [inst_8 : Std.Do.WPMonad o ps]
  [inst_9 : Std.IteratorLoop α Id n] [inst_10 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id n]
  [Std.LawfulIteratorLoop α Id o] [inst_13 : MonadLiftT n o] [LawfulMonadLiftT n o] {f : β → n γ} {g : δ → γ → o δ}
  {init : δ} {it : Std.Iter β} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.Iter.foldM
        (fun d b => do
          let c ← liftM (f b)
          g d c)
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.foldM g init (Std.Iter.mapM f it) ⦃Q⦄
-- Init.Data.Nat.Internal.Linear
_private.Init.Data.Nat.Internal.Linear.0.Nat.Internal.Linear.instBEqPolyCnstr.beq.match_1.eq_1 : ∀ (motive : Nat.Internal.Linear.PolyCnstr → Nat.Internal.Linear.PolyCnstr → Sort u_1) (a : Bool)
  (a_1 a_2 : Nat.Internal.Linear.Poly) (b : Bool) (b_1 b_2 : Nat.Internal.Linear.Poly)
  (h_1 :
    (a : Bool) →
      (a_3 a_4 : Nat.Internal.Linear.Poly) →
        (b : Bool) →
          (b_3 b_4 : Nat.Internal.Linear.Poly) →
            motive { eq := a, lhs := a_3, rhs := a_4 } { eq := b, lhs := b_3, rhs := b_4 })
  (h_2 : (x x_1 : Nat.Internal.Linear.PolyCnstr) → motive x x_1),
  (match { eq := a, lhs := a_1, rhs := a_2 }, { eq := b, lhs := b_1, rhs := b_2 } with
    | { eq := a, lhs := a_3, rhs := a_4 }, { eq := b, lhs := b_3, rhs := b_4 } => h_1 a a_3 a_4 b b_3 b_4
    | x, x_1 => h_2 x x_1) =
    h_1 a a_1 a_2 b b_1 b_2
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr.congr_simp : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {T₁ T₂ : AlgebraicGeometry.Scheme.Pullback.Triplet f g}
  (e : T₁ = T₂),
  AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr e = AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr e
-- Lean.Expr
Lean.Expr.forallName : (a : Lean.Expr) → a.isForall = true → Lean.Name
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.IdNode.mk.inj : ∀ {vPos hPosSrc hPosTar : ℕ} {id : Mathlib.Tactic.BicategoryLike.Atom₁} {vPos_1 hPosSrc_1 hPosTar_1 : ℕ}
  {id_1 : Mathlib.Tactic.BicategoryLike.Atom₁},
  { vPos := vPos, hPosSrc := hPosSrc, hPosTar := hPosTar, id := id } =
      { vPos := vPos_1, hPosSrc := hPosSrc_1, hPosTar := hPosTar_1, id := id_1 } →
    vPos = vPos_1 ∧ hPosSrc = hPosSrc_1 ∧ hPosTar = hPosTar_1 ∧ id = id_1
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.match_19.eq_1 : ∀ (aig : Std.Sat.AIG ℕ) (upper : ℕ) (h : upper < aig.decls.size) (lhs rhs : Std.Sat.AIG.Fanin)
  (this : lhs.gate < upper ∧ rhs.gate < upper) (lstate : Std.Sat.AIG.toCNF.State✝ aig)
  (motive : { out // Std.Sat.AIG.toCNF.State.IsExtensionBy✝ lstate out rhs.gate ⋯ } → Sort u_1)
  (rstate : Std.Sat.AIG.toCNF.State✝ aig) (hrstate : Std.Sat.AIG.toCNF.State.IsExtensionBy✝ lstate rstate rhs.gate ⋯)
  (h_1 :
    (rstate : Std.Sat.AIG.toCNF.State✝ aig) →
      (hrstate : Std.Sat.AIG.toCNF.State.IsExtensionBy✝ lstate rstate rhs.gate ⋯) → motive ⟨rstate, hrstate⟩),
  (match ⟨rstate, hrstate⟩ with
    | ⟨rstate, hrstate⟩ => h_1 rstate hrstate) =
    h_1 rstate hrstate
-- Mathlib.Tactic.FunProp.Decl
/-- argument index of a function this function property talks about.
For example, this would be 4 for `@Continuous α β _ _ f`  -/
Mathlib.Meta.FunProp.FunPropDecl.funArgId : Mathlib.Meta.FunProp.FunPropDecl → ℕ
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- A point in a projective space is contained in the span of a set of points if and only if the
point is contained in all subspaces of the projective space which contain the set of points.  -/
Projectivization.Subspace.mem_span : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {S : Set (Projectivization K V)} (u : Projectivization K V),
  u ∈ Projectivization.Subspace.span S ↔ ∀ (W : Projectivization.Subspace K V), S ⊆ ↑W → u ∈ W
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.addMonoidWithOne : {α : Type u} → [AddMonoidWithOne α] → AddMonoidWithOne (WithBot α)
-- Mathlib.Topology.MetricSpace.Cover
/-- A relatively compact set admits a finite cover.  -/
Metric.exists_finite_isCover_of_isCompact_closure : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ε : NNReal} {s : Set X},
  ε ≠ 0 → IsCompact (closure s) → ∃ N ⊆ s, N.Finite ∧ Metric.IsCover ε s N
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.rotate'.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → ℕ → Sort u_2) (l : List α) (h_1 : (x : ℕ) → motive [] x)
  (h_2 : (l : List α) → motive l 0) (h_3 : (a : α) → (l : List α) → (n : ℕ) → motive (a :: l) n.succ),
  (l = [] → False) →
    (match l, 0 with
      | [], x => h_1 x
      | l, 0 => h_2 l
      | a :: l, n.succ => h_3 a l n) =
      h_2 l
-- Std.Data.Iterators.Producers.Monadic.Array
_private.Std.Data.Iterators.Producers.Monadic.Array.0.Std.Iterators.Types.ArrayIterator.instFinitenessRelation : {α : Type w} →
  {m : Type w → Type w'} → [inst : Pure m] → Std.Iterators.FinitenessRelation (Std.Iterators.Types.ArrayIterator α) m
-- Mathlib.Algebra.BigOperators.Finprod
finprod_apply_ne_zero : ∀ {ι : Type u_7} {N₀ : Type u_8} {M₀ : Type u_9} [inst : CommMonoidWithZero M₀] [Nontrivial M₀] [NoZeroDivisors M₀]
  {n : N₀} {f : ι → N₀ → M₀}, (∀ (i : ι), f i n ≠ 0) → (∏ᶠ (i : ι), f i) n ≠ 0
-- Mathlib.Algebra.Order.Group.DenselyOrdered
exists_lt_nsmul_of_neg : ∀ {M : Type u_2} [inst : LinearOrder M] [DenselyOrdered M] {x : M} [inst_2 : AddCommGroup M]
  [IsOrderedCancelAddMonoid M], x < 0 → ∀ (n : ℕ), ∃ y < 0, x < n • y
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.ae_eq_dirac' : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [MeasurableSingletonClass β]
  {a : α} {f : α → β}, Measurable f → f =ᵐ[MeasureTheory.Measure.dirac a] Function.const α (f a)
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.arg.mkAnon : ℕ → Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.Algebra.Order.SuccPred
Order.succ_eq_zero : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddZeroClass α] [inst_2 : OrderBot α] [IsBotZeroClass α]
  [inst_4 : One α] [NoMaxOrder α] [inst_6 : SuccAddOrder α] {a : WithBot α}, a.succ = 0 ↔ a = ⊥
-- Init.Data.UInt.Lemmas
USize.ofInt_neg_one : USize.ofInt (-1) = -1
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
OpenPartialHomeomorph.map_nhdsWithin_eq : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : X},
  x ∈ e.source → ∀ (s : Set X), Filter.map (↑e) (nhdsWithin x s) = nhdsWithin (↑e x) (↑e '' (e.source ∩ s))
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.zero_mem_smul_set : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero β] [inst_1 : SMulZeroClass α β] {t : Set β} {a : α}, 0 ∈ t → 0 ∈ a • t
-- Mathlib.Data.Set.Subsingleton
Set.Subsingleton.denselyOrdered : ∀ {α : Type u} {s : Set α} [inst : LT α], s.Subsingleton → DenselyOrdered ↑s
-- Mathlib.Probability.Density
MeasureTheory.HasPDF.mk : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} {X : Ω → E}
  {ℙ : MeasureTheory.Measure Ω} {μ : autoParam (MeasureTheory.Measure E) MeasureTheory.HasPDF._auto_1},
  AEMeasurable X ℙ →
    (MeasureTheory.Measure.map X ℙ).HaveLebesgueDecomposition μ →
      (MeasureTheory.Measure.map X ℙ).AbsolutelyContinuous μ → MeasureTheory.HasPDF X ℙ μ
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.zsmul_nonpos : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.IntModule M] [Lean.Grind.OrderedAdd M]
  {k : ℤ} {a : M}, 0 ≤ k → a ≤ 0 → k • a ≤ 0
-- Init.Internal.Order.Basic
Lean.Order.implication_order_monotone_exists : ∀ {α : Sort u_1} [inst : Lean.Order.PartialOrder α] {β : Sort u_2} (f : α → β → Lean.Order.ImplicationOrder),
  Lean.Order.monotone f → Lean.Order.monotone fun x => Exists (f x)
-- Mathlib.Analysis.Convex.StrictCombination
Affine.Simplex.dist_lt_of_mem_interior_of_strictConvexSpace : ∀ {V : Type u_2} {P : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [StrictConvexSpace ℝ V]
  [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) {r : ℝ} {p₀ p : P},
  p ∈ s.interior → (∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r) → dist p p₀ < r
-- Lean.Parser.Term
Lean.Parser.Term.arrow : Lean.Parser.TrailingParser
-- Init.Data.Int.DivMod.Lemmas
Int.sub_fdiv_of_dvd : ∀ (a : ℤ) {b c : ℤ}, c ∣ b → (a - b).fdiv c = a.fdiv c - b.fdiv c
-- Mathlib.RingTheory.Algebraic.Integral
instIsAlgebraicPolynomialOfNoZeroDivisors_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [alg : Algebra.IsAlgebraic R S] [NoZeroDivisors S], Algebra.IsAlgebraic (Polynomial R) (Polynomial S)
-- Init.Data.Nat.Basic
Nat.instNeZeroHPow : ∀ {n m : ℕ} [NeZero n], NeZero (n ^ m)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.coe_recolorOfCardLE : ∀ {V : Type u} (G : SimpleGraph V) {α : Type u_2} {β : Type u_3} [inst : Fintype α] [inst_1 : Fintype β]
  (hαβ : Fintype.card α ≤ Fintype.card β),
  ⇑(G.recolorOfCardLE hαβ) = (SimpleGraph.Embedding.completeGraph ⋯.some).toHom.comp
-- Mathlib.RingTheory.Ideal.GoingUp
/-- `B ⧸ P` is an integral `A ⧸ p`-algebra if `B` is an integral `A`-algebra.  -/
Ideal.Quotient.algebra_isIntegral_of_liesOver : ∀ {A : Type u_1} [inst : CommRing A] {B : Type u_2} [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [Algebra.IsIntegral A B] (P : Ideal B) (p : Ideal A) [inst_4 : P.LiesOver p], Algebra.IsIntegral (A ⧸ p) (B ⧸ P)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.coe_equivMapOfInjective_apply : ∀ {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] (s : NonUnitalSubsemiring R) (f : F)
  (hf : Function.Injective ⇑f) (x : ↥s), ↑((s.equivMapOfInjective f hf) x) = f ↑x
-- Mathlib.Algebra.Group.Units.Basic
inv_eq_one_divp' : ∀ {α : Type u} [inst : Monoid α] (u : αˣ), ↑(1 / u) = 1 /ₚ u
-- Batteries.Data.List.Lemmas
List.countPBefore.eq_1 : ∀ {α : Type u_1} (p : α → Bool) (xs : List α) (i : ℕ), List.countPBefore p xs i = List.countPBefore.go p xs i 0
-- Mathlib.Data.Finset.Max
Finset.le_min_iff : ∀ {α : Type u_2} [inst : LinearOrder α] {m : WithTop α} {s : Finset α}, m ≤ s.min ↔ ∀ a ∈ s, m ≤ ↑a
-- Mathlib.Algebra.Symmetrized
SymAlg.instIsCommJordan : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : Invertible 2], IsCommJordan αˢʸᵐ
-- Mathlib.Order.Filter.AtTopBot.Archimedean
Rat.comap_cast_atTop : ∀ {R : Type u_2} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [Archimedean R],
  Filter.comap Rat.cast Filter.atTop = Filter.atTop