mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioo_self : ∀ {α : Type u_2} (a : α) [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], Finset.Ioo a a = ∅
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vlt_of_vle_of_vlt : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, x ≤ᵥ y → y <ᵥ z → x <ᵥ z
-- Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
GenContFract.IntFractPair.coe_stream_nth_rat_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] [IsStrictOrderedRing K] {v : K}
  {q : ℚ},
  v = ↑q →
    ∀ (n : ℕ),
      Option.map (GenContFract.IntFractPair.mapFr Rat.cast) (GenContFract.IntFractPair.stream q n) =
        GenContFract.IntFractPair.stream v n
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedCancelAddMonoid.toAddLeftReflectLT : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α], AddLeftReflectLT α
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
/-- The generators of the tensor algebra are disjoint from its scalars.  -/
TensorAlgebra.ι_range_disjoint_one : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Disjoint (TensorAlgebra.ι R).range 1
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry!_of_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α}
  [inst_2 : Inhabited ((a : α) × β a)],
  Std.Internal.List.DistinctKeys l → l.Perm l' → Std.Internal.List.getEntry! a l = Std.Internal.List.getEntry! a l'
-- Lean.Meta.Basic
Lean.Meta.MetaM.run' : {α : Type} → Lean.MetaM α → optParam Lean.Meta.Context { } → optParam Lean.Meta.State { } → Lean.CoreM α
-- Init.Data.BitVec.Lemmas
BitVec.umod_lt : ∀ {n : ℕ} (x : BitVec n) {y : BitVec n}, 0 < y → x % y < y
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.instDecidableOfDecidableEq : {α : Type u_1} → [DecidableEq α] → {f : α → α} → {n : ℕ} → {x : α} → Decidable (Function.IsPeriodicPt f n x)
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- State for `delabAppMatch` and helpers.  -/
Lean.PrettyPrinter.Delaborator.AppMatchState : Type
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.functorialityCompPrecompose_inv_app_hom : ∀ {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] {F : CategoryTheory.Functor J C}
  {H H' : CategoryTheory.Functor C D} (α : H ≅ H') (X : CategoryTheory.Limits.Cocone F),
  ((CategoryTheory.Functor.functorialityCompPrecompose α).inv.app X).hom = α.inv.app X.pt
-- Mathlib.Algebra.Torsor.Basic
Pi.sdiv_def : ∀ {I : Type u} {fg : I → Type v} [inst : (i : I) → Group (fg i)] {fp : I → Type w}
  [inst_1 : (i : I) → Torsor (fg i) (fp i)] (p q : (i : I) → fp i), p /ₛ q = fun i => p i /ₛ q i
-- Mathlib.Analysis.MeanInequalitiesPow
/-- Variant of `ENNReal.rpow_add_le_mul_rpow_add_rpow` using `LpAddConst` as the constant,
valid for all `0 ≤ p` (not just `1 ≤ p`).  -/
ENNReal.rpow_add_le_mul_rpow_add_rpow' : ∀ (z₁ z₂ : ENNReal) {p : ℝ}, 0 ≤ p → (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
algebraicIndependent_subtype : ∀ {R : Type u_2} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {s : Set A},
  AlgebraicIndependent R Subtype.val ↔ ∀ p ∈ MvPolynomial.supported R s, (MvPolynomial.aeval id) p = 0 → p = 0
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerLeftIso_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h),
  (CategoryTheory.Bicategory.whiskerLeftIso f η).inv = CategoryTheory.Bicategory.whiskerLeft f η.inv
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.Ordinal.instInhabitedOfDay : Inhabited Std.Time.Nanosecond.Ordinal.OfDay
-- Lean.Elab.Parallel
/-- Runs a list of MetaM computations in parallel (without cancellation hook).

Returns an iterator that yields results in completion order, wrapped in `Except Exception α`.
 -/
Lean.Meta.MetaM.parIterGreedy : {α : Type} → List (Lean.MetaM α) → Lean.MetaM (Std.IterM Lean.MetaM (Except Lean.Exception α))
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.single_sub : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddCommGroup (β i)] (p : ENNReal) (i : ι)
  {a b : β i}, PiLp.single p i (a - b) = PiLp.single p i a - PiLp.single p i b
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.eq_empty_or_encard_eq_top_or_encard_sdiff_singleton_lt`.

---

Every set is either empty, infinite, or can have its `encard` reduced by a removal. Intended
for well-founded induction on the value of `encard`.  -/
Set.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt : ∀ {α : Type u_1} (s : Set α), s = ∅ ∨ s.encard = ⊤ ∨ ∃ a ∈ s, (s \ {a}).encard < s.encard
-- Mathlib.Algebra.CharP.Defs
CharP.charP_zero_iff_charZero : ∀ (R : Type u_1) [inst : AddGroupWithOne R], CharP R 0 ↔ CharZero R
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.Limits.instHasColimitsOfShape : ∀ {J : Type u} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J],
  CategoryTheory.Limits.HasColimitsOfShape J PartOrdEmb
-- Mathlib.Topology.MetricSpace.Thickening
/-- The closed thickening `Metric.cthickening δ E` of a fixed subset `E` is an increasing function
of the thickening radius `δ`.  -/
Metric.cthickening_mono : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ₁ δ₂ : ℝ},
  δ₁ ≤ δ₂ → ∀ (E : Set α), Metric.cthickening δ₁ E ⊆ Metric.cthickening δ₂ E
-- Mathlib.Analysis.Normed.Group.Basic
SeminormedAddGroup.toNNNorm : {E : Type u_5} → [SeminormedAddGroup E] → NNNorm E
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.foldrM.eq_2 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [inst : Monad m] (f : (a : α) → β a → δ → m δ)
  (x : δ) (a : α) (b : β a) (es : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.foldrM f x (Std.DHashMap.Internal.AssocList.cons a b es) = do
    let d ← Std.DHashMap.Internal.AssocList.foldrM f x es
    f a b d
-- Batteries.Classes.Order
Std.instTransCmpCompareLex_batteries : ∀ {α : Type u_1} {cmp₁ cmp₂ : α → α → Ordering} [inst₁ : Std.TransCmp cmp₁] [inst₂ : Std.TransCmp cmp₂],
  Std.TransCmp (compareLex cmp₁ cmp₂)
-- Mathlib.Combinatorics.Enumerative.Schroder
Nat.largeSchroder_one : Nat.largeSchroder 1 = 2
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffWithinAt.sub_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : SubNegMonoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G]
  {E' : Type u_5} [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_6}
  [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace H' M] {f : M → G} {s : Set M} {x : M} (c : G),
  ContMDiffWithinAt I' I n f s x → ContMDiffWithinAt I' I n (fun x => f x - c) s x
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
/-- Composition of prelax functors.  -/
CategoryTheory.PrelaxFunctor.comp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {D : Type u₃} →
          [inst_2 : CategoryTheory.Bicategory D] →
            CategoryTheory.PrelaxFunctor B C → CategoryTheory.PrelaxFunctor C D → CategoryTheory.PrelaxFunctor B D
-- Mathlib.Data.List.Triplewise
List.triplewise_iff : ∀ {α : Type u_1} (p : α → α → α → Prop) (a : List α),
  List.Triplewise p a ↔ a = [] ∨ ∃ a_1 l, List.Pairwise (p a_1) l ∧ List.Triplewise p l ∧ a = a_1 :: l
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.map_polynomial : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) {S : Type s} [inst_1 : CommRing S]
  (f : R →+* S), (W'.map f).polynomial = (MvPolynomial.map f) W'.polynomial
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_zero : ∀ (f : (a : Ordinal.{u_3}) → a < 0 → Ordinal.{max u_3 u_4}), Ordinal.bsup 0 f = 0
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.RootFormIn.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_5)
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [inst_7 : FaithfulSMul S R] [inst_8 : Module S M]
  [inst_9 : IsScalarTower S R M] [inst_10 : P.IsValuedIn S] [inst_11 : Fintype ι], P.RootFormIn S = P.RootFormIn S
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.star_mk : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : CommRing R] (a₁ a₂ a₃ a₄ : R),
  star { re := a₁, imI := a₂, imJ := a₃, imK := a₄ } = { re := a₁ + c₂ * a₂, imI := -a₂, imJ := -a₃, imK := -a₄ }
-- Lean.Declaration
Lean.Constructor.mk.sizeOf_spec : ∀ (name : Lean.Name) (type : Lean.Expr), sizeOf { name := name, type := type } = 1 + sizeOf name + sizeOf type
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.Indep.augment_finset : ∀ {α : Type u_1} {M : Matroid α} {I J : Finset α},
  M.Indep ↑I → M.Indep ↑J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ M.Indep (insert e ↑I)
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
/-- Right whiskering of an oplax natural transformation and a modification.  -/
CategoryTheory.Lax.OplaxTrans.whiskerRight : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H : CategoryTheory.LaxFunctor B C} →
          {η θ : F ⟶ G} →
            (η ⟶ θ) → (ι : G ⟶ H) → CategoryTheory.CategoryStruct.comp η ι ⟶ CategoryTheory.CategoryStruct.comp θ ι
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.instIsEquivalenceTriangleInvRotate : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive],
  (CategoryTheory.Pretriangulated.invRotate C).IsEquivalence
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.instZeroHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → (G H : CategoryTheory.Grp C) → Zero (G ⟶ H)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.instInhabitedSimprocOLeanEntry.default : Lean.Meta.Simp.SimprocOLeanEntry
-- Mathlib.CategoryTheory.Widesubcategory
/-- Build an isomorphism in `WideSubcategory P` from an isomorphism in `C`.  -/
CategoryTheory.WideSubcategory.isoMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P : CategoryTheory.MorphismProperty C} →
      [inst_1 : P.IsMultiplicative] →
        {X Y : CategoryTheory.WideSubcategory P} → (e : X.obj ≅ Y.obj) → P e.hom → P e.inv → (X ≅ Y)
-- Batteries.Data.List.Lemmas
List.diff_cons : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (l₁ l₂ : List α) (a : α), l₁.diff (a :: l₂) = (l₁.erase a).diff l₂
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.op_horn : ∀ {n : ℕ} (i : Fin (n + 1)), (SSet.horn n i).op.preimage (SSet.stdSimplex.opIso { len := n }).inv = SSet.horn n i.rev
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.sheafify_hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {P Q : CategoryTheory.Functor Cᵒᵖ D}
  (η γ : J.sheafify P ⟶ Q),
  CategoryTheory.Presheaf.IsSheaf J Q →
    CategoryTheory.CategoryStruct.comp (J.toSheafify P) η = CategoryTheory.CategoryStruct.comp (J.toSheafify P) γ →
      η = γ
-- Mathlib.RingTheory.SimpleRing.Basic
IsSimpleRing.iff_injective_ringHom_or_subsingleton_codomain : ∀ (R : Type u) [inst : NonAssocRing R] [Nontrivial R],
  IsSimpleRing R ↔ ∀ {S : Type u} [inst_2 : NonAssocSemiring S] (f : R →+* S), Function.Injective ⇑f ∨ Subsingleton S
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.multispan_obj_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) (b : J.R),
  I.multispan.obj (CategoryTheory.Limits.WalkingMultispan.right b) = I.right b
-- Mathlib.Probability.Moments.Variance
/-- The variance of the sum of two independent random variables is the sum of the variances.  -/
ProbabilityTheory.IndepFun.variance_fun_add : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ},
  MeasureTheory.MemLp X 2 μ →
    MeasureTheory.MemLp Y 2 μ →
      ProbabilityTheory.IndepFun X Y μ →
        ProbabilityTheory.variance (fun ω => X ω + Y ω) μ =
          ProbabilityTheory.variance X μ + ProbabilityTheory.variance Y μ
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
/-- `Z^n(f, g)` identifies to a cokernel of the `H^n(f) ⟶ H^n(f ≫ g)`.  -/
CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles_exact : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ), (X.cokernelSequenceCycles f g fg h n).Exact
-- Mathlib.Algebra.Order.Module.Defs
/-- Scalar multiplication on the right by a nonnegative element preserves monotonicity.  -/
Monotone.smul_const : ∀ {α : Type u_1} {β : Type u_2} {b : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero β]
  [SMulPosMono α β] {γ : Type u_3} [inst_5 : Preorder γ] {f : γ → α}, Monotone f → 0 ≤ b → Monotone fun x => f x • b
-- Init.Data.List.Lemmas
List.mem_filterMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} {b : β}, b ∈ List.filterMap f l ↔ ∃ a ∈ l, f a = some b
-- Aesop.RuleTac.RuleTerm
Aesop.RuleTerm.const.sizeOf_spec : ∀ (decl : Lean.Name), sizeOf (Aesop.RuleTerm.const decl) = 1 + sizeOf decl
-- Mathlib.Data.PFunctor.Multivariate.Basic
/-- Destructor for functor composition  -/
MvPFunctor.comp.get : {n m : ℕ} →
  {P : MvPFunctor.{u} n} → {Q : Fin2 n → MvPFunctor.{u} m} → {α : TypeVec.{u} m} → ↑(P.comp Q) α → ↑P fun i => ↑(Q i) α
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.continuous_toCompletion : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  Continuous IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion
-- Mathlib.Computability.StateTransition
/-- The reflexive transitive closure of a state transition function. `Reaches f a b` means
there is a finite sequence of steps `f a = some a₁`, `f a₁ = some a₂`, ... such that `aₙ = b`.
This relation permits zero steps of the state transition function.  -/
StateTransition.Reaches : {σ : Type u_1} → (σ → Option σ) → σ → σ → Prop
-- Mathlib.AlgebraicGeometry.Scheme
/-- If `x = y`, the stalk maps are isomorphic.  -/
AlgebraicGeometry.Scheme.Hom.arrowStalkMapIsoOfEq : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    {x y : ↥X} →
      x = y →
        (CategoryTheory.Arrow.mk (AlgebraicGeometry.Scheme.Hom.stalkMap f x) ≅
          CategoryTheory.Arrow.mk (AlgebraicGeometry.Scheme.Hom.stalkMap f y))
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.Derives.reverse : ∀ {T : Type u_1} {g : ContextFreeGrammar T} {u v : List (Symbol T g.NT)},
  g.Derives u v → g.reverse.Derives u.reverse v.reverse
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.sdiv_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] (s : Set β) (b : β), s /ₛ {b} = (fun x => x /ₛ b) '' s
-- Init.Meta.Defs
Lean.Syntax.isNameLit? : Lean.Syntax → Option Lean.Name
-- Mathlib.Algebra.Module.LinearMap.End
/-- Applying a linear map at `v : M`, seen as a linear map from `M →ₗ[R] M₂` to `M₂`.
See also `LinearMap.applyₗ'` for a version that works with two different semirings.

This is the `LinearMap` version of `toAddMonoidHom.eval`.  -/
LinearMap.applyₗ : {R : Type u_1} →
  {M : Type u_4} →
    {M₂ : Type u_6} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] → [inst_3 : Module R M] → [inst_4 : Module R M₂] → M →ₗ[R] (M →ₗ[R] M₂) →ₗ[R] M₂
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- `G'.neighborSet v` is the set of vertices adjacent to `v` in `G'`.  -/
SimpleGraph.Subgraph.neighborSet : {V : Type u} → {G : SimpleGraph V} → G.Subgraph → V → Set V
-- Lean.Parser.Tactic
Lean.Parser.Tactic.unknown.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.Array.Lemmas
Array.push_eq_flatten_iff : ∀ {α : Type u_1} {xss : Array (Array α)} {ys : Array α} {y : α},
  ys.push y = xss.flatten ↔ ∃ as bs cs, xss = as.push (bs.push y) ++ cs ∧ (∀ xs ∈ cs, xs = #[]) ∧ ys = as.flatten ++ bs
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.map_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] {f : α ↪ β}, Finset.map f 0 = {f 0}
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If a `BinaryCofan` is a colimit, then its opposite is a limit.  -/
CategoryTheory.Limits.BinaryCofan.IsColimit.op : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {c : CategoryTheory.Limits.BinaryCofan X Y} →
        CategoryTheory.Limits.IsColimit c → CategoryTheory.Limits.IsLimit c.op
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.comp_sub : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁)
  (z₂ z₂' : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂),
  z₁.comp (z₂ - z₂') h = z₁.comp z₂ h - z₁.comp z₂' h
-- Mathlib.Algebra.Group.Basic
eq_add_neg_iff_add_eq : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, a = b + -c ↔ a + c = b
-- Init.Data.Range.Polymorphic.SInt
Int32.instRxcLawfulHasSize : Std.Rxc.LawfulHasSize Int32
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.torsionOrder_pos : ∀ (K : Type u_1) [inst : Field K] [NumberField K], 0 < NumberField.Units.torsionOrder K
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- The trivial zeroes of the sine zeta function.  -/
HurwitzZeta.sinZeta_neg_two_mul_nat_sub_one : ∀ (a : UnitAddCircle) (n : ℕ), HurwitzZeta.sinZeta a (-2 * ↑n - 1) = 0
-- Mathlib.RingTheory.Algebraic.Basic
Polynomial.transcendental : ∀ {R : Type u} [inst : CommRing R] (f : Polynomial R),
  f.natDegree ≠ 0 → f.leadingCoeff ∈ nonZeroDivisors R → Transcendental R f
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.precheckApp : Lean.Elab.Term.Quotation.Precheck
-- Mathlib.Topology.LocallyClosed
Topology.IsEmbedding.isLocallyClosed_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y},
  Topology.IsEmbedding f → (IsLocallyClosed s ↔ ∃ s', IsLocallyClosed s' ∧ s' ∩ Set.range f = f '' s)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Sub
/-- For any function `f : α → ℝ≥0∞`, there exists a measurable function `g ≤ f` with the same
integral over any measurable set.  -/
MeasureTheory.exists_measurable_le_setLIntegral_eq_of_integrable : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  ∫⁻ (a : α), f a ∂μ ≠ ⊤ →
    ∃ g, Measurable g ∧ g ≤ f ∧ ∀ (s : Set α), MeasurableSet s → ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatchAt.lt : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice} {startPos endPos : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAt pat startPos endPos → startPos < endPos
-- Init.System.IO
IO.Process.SpawnArgs.mk : IO.Process.StdioConfig →
  String → Array String → Option System.FilePath → Array (String × Option String) → Bool → Bool → IO.Process.SpawnArgs
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
/-- The multiset of normalized factors of `x` is nil if and only if `x` is a unit.
The converse is true without the nonzero assumption, see `normalizedFactors_of_isUnit`.
 -/
UniqueFactorizationMonoid.normalizedFactors_eq_zero_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {x : α}, x ≠ 0 → (UniqueFactorizationMonoid.normalizedFactors x = 0 ↔ IsUnit x)
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.linearEquivFunOnFinite_single : ∀ (R : Type u_9) (M : Type u_11) (α : Type u_12) [inst : Finite α] [inst_1 : AddCommMonoid M] [inst_2 : Semiring R]
  [inst_3 : Module R M] [inst_4 : DecidableEq α] (x : α) (m : M),
  ((Finsupp.linearEquivFunOnFinite R M α) fun₀ | x => m) = Pi.single x m
-- Mathlib.Condensed.Light.EffectiveEpi
instIsRegularEpiCategoryLightCondSet : CategoryTheory.IsRegularEpiCategory LightCondSet
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.lift_symm : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {E : Type u_9} [inst_3 : AddCommMonoid E] [inst_4 : Module R E]
  (φ' : (PiTensorProduct R fun i => s i) →ₗ[R] E),
  PiTensorProduct.lift.symm φ' = φ'.compMultilinearMap (PiTensorProduct.tprod R)
-- Mathlib.Algebra.Ring.BooleanRing
BooleanRing.toRing : {α : Type u_4} → [self : BooleanRing α] → Ring α
-- Mathlib.Algebra.Order.Group.PosPart
instLeOnePart.eq_1 : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : DivInvMonoid α], instLeOnePart = { leOnePart := fun a => a⁻¹ ⊔ 1 }
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instNonUnitalNormedCommRing : {α : Type u_1} →
  {R : Type u_3} →
    [inst : TopologicalSpace α] →
      [CompactSpace α] →
        [inst_2 : Zero α] → [inst_3 : NormedCommRing R] → NonUnitalNormedCommRing (ContinuousMapZero α R)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.of_forall_mem_unit_iff : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {t₁ t₂ : Std.TreeMap.Raw α Unit cmp},
  t₁.WF → t₂.WF → (∀ (k : α), k ∈ t₁ ↔ k ∈ t₂) → t₁.Equiv t₂
-- Mathlib.Data.ENat.Basic
ENat.exists_nat_gt : ∀ {n : ℕ∞}, n ≠ ⊤ → ∃ m, n < ↑m
-- Mathlib.Analysis.Complex.OperatorNorm
Complex.ofRealCLM_enorm : ‖Complex.ofRealCLM‖ₑ = 1
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.FiniteRangeSetoid.projection_equiv_zero_iff_isNoetherian : ∀ {K : Type u_1} {V : Type u_2} [inst : CommRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {S T : Submodule K V} (hST : IsCompl S T), S.projection T hST ≈ 0 ↔ IsNoetherian K ↥S
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- The zero module is linearly disjoint with any other submodules.  -/
Submodule.LinearDisjoint.bot_left : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (N : Submodule R S),
  ⊥.LinearDisjoint N
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.id_comp : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N), (MulHom.id N).comp f = f
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.eq_bot_iff : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M), N = ⊥ ↔ ∀ m ∈ N, m = 0