mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.subtypeDomain_apply : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] {p : ι → Prop} [inst_1 : DecidablePred p] {i : Subtype p}
  {v : Π₀ (i : ι), β i}, (DFinsupp.subtypeDomain p v) i = v ↑i
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pushoutCoconeOfRightIso_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.IsIso g],
  (CategoryTheory.Limits.pushoutCoconeOfRightIso f g).inr = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) f
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.instIsSMulApplyUpperHalfPlaneComplex_1 : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {α : Type u_2} [inst : SMul α ℂ] [inst_1 : SMul α ℝ]
  [inst_2 : IsScalarTower α ℝ ℂ], IsSMulApply α (SlashInvariantForm Γ k) UpperHalfPlane ℂ
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.instZSMul.eq_1 : ∀ {M : Type uM} {N : Type uN} [inst : AddZeroClass M] [inst_1 : AddCommGroup N],
  AddMonoidHom.instZSMul = { smul := fun n f => { toFun := n • ⇑f, map_zero' := ⋯, map_add' := ⋯ } }
-- Mathlib.CategoryTheory.Linear.Basic
CategoryTheory.Linear.units_smul_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type w}
  [inst_2 : Semiring R] [inst_3 : CategoryTheory.Linear R C] {X Y Z : C} (r : Rˣ) (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (r • f) g = r • CategoryTheory.CategoryStruct.comp f g
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.support_comap : ∀ {X Y : AlgebraicGeometry.Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y), (I.comap f).support = I.support.preimage ⋯
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDateTime.instHSubOffset_4 : HSub Std.Time.PlainDateTime Std.Time.Millisecond.Offset Std.Time.PlainDateTime
-- Mathlib.Data.Set.Lattice.Image
Set.bijOn_iUnion : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : ι → Set α} {t : ι → Set β} {f : α → β},
  (∀ (i : ι), Set.BijOn f (s i) (t i)) → Set.InjOn f (⋃ i, s i) → Set.BijOn f (⋃ i, s i) (⋃ i, t i)
-- Aesop.Tree.Data
Aesop.RappUnsafe : Type
-- Std.Http.Data.URI.Basic
Std.Http.URI.Path.mk.sizeOf_spec : ∀ (segments : Array Std.Http.URI.EncodedSegment) (absolute : Bool),
  sizeOf { segments := segments, absolute := absolute } = 1 + sizeOf segments + sizeOf absolute
-- Mathlib.Data.Set.Restrict
Set.domRestrict_dite : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} [inst : (x : α) → Decidable (x ∈ s)] (f : (a : α) → a ∈ s → β)
  (g : (a : α) → a ∉ s → β), (s.domRestrict fun a => if h : a ∈ s then f a h else g a h) = fun a => f ↑a ⋯
-- Mathlib.LinearAlgebra.Projection
Submodule.projectionOnto.eq_1 : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (p q : Submodule R E)
  (h : IsCompl p q), p.projectionOnto q h = LinearMap.fst R ↥p ↥q ∘ₗ ↑(p.prodEquivOfIsCompl q h).symm
-- Mathlib.GroupTheory.CoprodI
/-- `fstIdx w` is `some i` if the first letter of `w` is `⟨i, m⟩` with `m : M i`. If `w` is empty
then it's `none`.  -/
Monoid.CoprodI.Word.fstIdx : {ι : Type u_1} → {M : ι → Type u_2} → [inst : (i : ι) → Monoid (M i)] → Monoid.CoprodI.Word M → Option ι
-- Init.WFExtrinsicFix
WellFounded.partialExtrinsicFix₂_eq_apply : ∀ {α : Sort u_2} {β : α → Sort u_3} {C₂ : (a : α) → β a → Sort u_1} [inst : ∀ (a : α) (b : β a), Nonempty (C₂ a b)]
  {R : (a : α) ×' β a → (a : α) ×' β a → Prop}
  {F : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b} {a : α} {b : β a},
  WellFounded R →
    WellFounded.partialExtrinsicFix₂ R F a b = F a b fun a' b' x => WellFounded.partialExtrinsicFix₂ R F a' b'
-- Mathlib.Algebra.Group.Basic
sub_sub_sub_cancel_right : ∀ {G : Type u_3} [inst : AddGroup G] (a b c : G), a - c - (b - c) = a - b
-- Mathlib.Tactic.FailIfNoProgress
_private.Mathlib.Tactic.FailIfNoProgress.0.Mathlib.Tactic.lctxIsDefEq.match_1.eq_3 : ∀ (motive : List (Option Lean.LocalDecl) → List (Option Lean.LocalDecl) → Sort u_1) (d₁ : Lean.LocalDecl)
  (l₁ : List (Option Lean.LocalDecl)) (d₂ : Lean.LocalDecl) (l₂ : List (Option Lean.LocalDecl))
  (h_1 : (l₁ l₂ : List (Option Lean.LocalDecl)) → motive (none :: l₁) l₂)
  (h_2 : (l₁ l₂ : List (Option Lean.LocalDecl)) → motive l₁ (none :: l₂))
  (h_3 :
    (d₁ : Lean.LocalDecl) →
      (l₁ : List (Option Lean.LocalDecl)) →
        (d₂ : Lean.LocalDecl) → (l₂ : List (Option Lean.LocalDecl)) → motive (some d₁ :: l₁) (some d₂ :: l₂))
  (h_4 : Unit → motive [] []) (h_5 : (x x_1 : List (Option Lean.LocalDecl)) → motive x x_1),
  (match some d₁ :: l₁, some d₂ :: l₂ with
    | none :: l₁, l₂ => h_1 l₁ l₂
    | l₁, none :: l₂ => h_2 l₁ l₂
    | some d₁ :: l₁, some d₂ :: l₂ => h_3 d₁ l₁ d₂ l₂
    | [], [] => h_4 ()
    | x, x_1 => h_5 x x_1) =
    h_3 d₁ l₁ d₂ l₂
-- Aesop.Rule.Name
Aesop.instHashablePhaseName : Hashable Aesop.PhaseName
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.eq_zero_cpow_iff : ∀ {x a : ℂ}, a = 0 ^ x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.disjoint_ker : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {f : M →ₛₗ[τ₁₂] M₂} {p : Submodule R M}, Disjoint p f.ker ↔ ∀ x ∈ p, f x = 0 → x = 0
-- Mathlib.Algebra.Algebra.Unitization
Unitization.algebraMap_eq_inlRingHom : ∀ (R : Type u_2) (A : Type u_3) [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A],
  algebraMap R (Unitization R A) = Unitization.inlRingHom R A
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.toArray_toList : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxo.IsAlwaysFinite α], r.toList.toArray = r.toArray
-- Mathlib.Condensed.Discrete.Module
LightCondMod.LocallyConstant.instFullModuleCatLightCondensedDiscrete : ∀ (R : Type u) [inst : Ring R], (LightCondensed.discrete (ModuleCat R)).Full
-- Mathlib.Topology.ContinuousMap.Star
/-- `ContinuousMap.compStarAlgHom'` as a `StarAlgEquiv` when the continuous map `f` is
actually a homeomorphism.  -/
Homeomorph.compStarAlgEquiv' : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (𝕜 : Type u_3) →
          [inst_2 : CommSemiring 𝕜] →
            (A : Type u_4) →
              [inst_3 : TopologicalSpace A] →
                [inst_4 : Semiring A] →
                  [inst_5 : IsTopologicalSemiring A] →
                    [inst_6 : StarRing A] →
                      [inst_7 : ContinuousStar A] → [inst_8 : Algebra 𝕜 A] → X ≃ₜ Y → C(Y, A) ≃⋆ₐ[𝕜] C(X, A)
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.curryFinFinset_symm_apply : ∀ {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [inst : CommSemiring R] [inst_1 : AddCommMonoid M']
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M'] [inst_4 : Module R M₂] {k l n : ℕ} {s : Finset (Fin n)}
  (hk : s.card = k) (hl : sᶜ.card = l) (f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂))
  (m : Fin n → M'),
  ((MultilinearMap.curryFinFinset R M₂ M' hk hl).symm f) m =
    (f fun i => m ((finSumEquivOfFinset hk hl) (Sum.inl i))) fun i => m ((finSumEquivOfFinset hk hl) (Sum.inr i))
-- Lean.Parser.Term
Lean.Parser.Term.letrec.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- A purely inseparable extension is normal.  -/
IsPurelyInseparable.normal : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [IsPurelyInseparable F E],
  Normal F E
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.ext_iff : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  {e e' : E ≃ₛₗᵢ[σ₁₂] E₂}, e = e' ↔ ∀ (x : E), e x = e' x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, k ∈ t.insert k v
-- Init.Data.Nat.Div.Basic
Nat.divExact_eq_div : ∀ {x y : ℕ} (h : y ∣ x), x.divExact y h = x / y
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbitRel.Quotient.orbit_mk : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (a : α),
  AddAction.orbitRel.Quotient.orbit (Quotient.mk'' a) = AddAction.orbit G a
-- Lean.Meta.LazyDiscrTree
/-- Creates the core context used for initializing a tree using the current context.  -/
Lean.Meta.LazyDiscrTree.createTreeCtx : Lean.Core.Context → Lean.Core.Context
-- Mathlib.RingTheory.IsGaloisGroup.Basic
/-- If `G` is finite and `A` is integrally closed then `IsGaloisGroup G A B` is equivalent to `B/A`
being integral and the fields of fractions `Frac(B)/Frac(A)` being Galois with Galois group `G`.  -/
IsGaloisGroup.iff_isFractionRing : ∀ (G : Type u_1) (A : Type u_2) (B : Type u_3) (K : Type u_4) (L : Type u_5) [inst : Group G] [inst_1 : CommRing A]
  [inst_2 : CommRing B] [inst_3 : MulSemiringAction G B] [inst_4 : Algebra A B] [inst_5 : Field K] [inst_6 : Field L]
  [inst_7 : Algebra K L] [inst_8 : Algebra A K] [inst_9 : Algebra B L] [inst_10 : Algebra A L] [IsFractionRing A K]
  [IsFractionRing B L] [IsScalarTower A K L] [IsScalarTower A B L] [inst_15 : MulSemiringAction G L]
  [SMulDistribClass G B L] [Finite G] [IsIntegrallyClosed A],
  IsGaloisGroup G A B ↔ Algebra.IsIntegral A B ∧ IsGaloisGroup G K L
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- Lax right unity.  -/
CategoryTheory.LaxFunctor.map₂_rightUnitor : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.LaxFunctor B C) {a b : B} (f : a ⟶ b),
  self.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (self.map f)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapId b))
        (self.mapComp f (CategoryTheory.CategoryStruct.id b)))
-- Mathlib.RingTheory.Regular.IsSMulRegular
isSMulRegular_on_quot_iff_lsmul_comap_eq : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M)
  (r : R), IsSMulRegular (M ⧸ N) r ↔ Submodule.comap ((LinearMap.lsmul R M) r) N = N
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_rpow : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] (a : A) (x y : ℝ),
  x ≠ 0 → autoParam (IsStrictlyPositive a) CFC.rpow_rpow._auto_1 → (a ^ x) ^ y = a ^ (x * y)
-- Mathlib.Tactic.DefEqAbuse
/-- PP option escalation levels for disambiguating `X =?= X` failures.
Each level adds more detail to pretty-printed expressions.
We prefer symmetric options (`pp.universes`, `pp.explicit`) over `pp.analyze`,
which is context-dependent and can add annotations to only one side.  -/
_private.Mathlib.Tactic.DefEqAbuse.0.Mathlib.Tactic.DefEqAbuse.ppEscalations : List (Lean.Options → Lean.Options)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.fastGrowingε₀_zero : ONote.fastGrowingε₀ 0 = 1
-- Mathlib.Algebra.Field.Subfield.Defs
SubfieldClass.nnqsmul_mem : ∀ {K : Type u} [inst : DivisionRing K] {S : Type u_1} [inst_1 : SetLike S K] [h : SubfieldClass S K] {x : K} (s : S)
  (q : ℚ≥0), x ∈ s → q • x ∈ s
-- Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra
LieAlgebra.instNonemptyCommutatorRing : ∀ (L : Type v) [Nonempty L], Nonempty (CommutatorRing L)
-- Mathlib.CategoryTheory.Sites.Coverage
/-- A precoverage with pullbacks defines a coverage.  -/
CategoryTheory.Precoverage.toCoverage : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (J : CategoryTheory.Precoverage C) → [J.HasPullbacks] → [J.IsStableUnderBaseChange] → CategoryTheory.Coverage C
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeGroup.toWord_injective : ∀ {α : Type u_1} [inst : DecidableEq α], Function.Injective FreeGroup.toWord
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- The canonical isomorphism relating `Span f.op g.op` and `(Cospan f g).op`  -/
CategoryTheory.Limits.spanOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          CategoryTheory.Limits.span f.op g.op ≅
            CategoryTheory.Limits.walkingCospanOpEquiv.inverse.comp (CategoryTheory.Limits.cospan f g).op
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.setCurr' : ∀ {l r : List Char} {c : Char} {it : String.Legacy.Iterator},
  String.Legacy.Iterator.ValidFor l r it →
    String.Legacy.Iterator.ValidFor l (List.modifyHead (fun x => c) r) (it.setCurr c)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.comp_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A₀ A₁ A₂ : CategoryTheory.Endofunctor.Algebra F} (f : A₀ ⟶ A₁) (g : A₁ ⟶ A₂),
  (CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f
-- Init.Data.UInt.BasicAux
USize.instOfNat : {n : ℕ} → OfNat USize n
-- Mathlib.NumberTheory.Divisors
Nat.disjoint_divisors_filter_isPrimePow : ∀ {a b : ℕ}, a.Coprime b → Disjoint (Finset.filter IsPrimePow a.divisors) (Finset.filter IsPrimePow b.divisors)
-- Mathlib.ModelTheory.Basic
/-- A first-order structure on a type `M` consists of interpretations of all the symbols in a given
language. Each function of arity `n` is interpreted as a function sending tuples of length `n`
(modeled as `(Fin n → M)`) to `M`, and a relation of arity `n` is a function from tuples of length
`n` to `Prop`.  -/
FirstOrder.Language.Structure : FirstOrder.Language → Type w → Type (max (max u v) w)
-- Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
/-- Helper lemma for the first part of the First Main Theorem: Given a meromorphic function `f`, compute
difference between the characteristic functions of `f` and of its inverse.
 -/
ValueDistribution.characteristic_sub_characteristic_inv : ∀ {f : ℂ → ℂ},
  Meromorphic f →
    ValueDistribution.characteristic f ⊤ - ValueDistribution.characteristic f⁻¹ ⊤ =
      Real.circleAverage (fun x => Real.log ‖f x‖) 0 -
        Function.locallyFinsuppWithin.logCounting (MeromorphicOn.divisor f Set.univ)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExProdNat.const.injEq : ∀ {e : Q(ℕ)} (value value_1 : Mathlib.Tactic.Ring.Common.btℕ e),
  (Mathlib.Tactic.Ring.Common.ExProdNat.const value = Mathlib.Tactic.Ring.Common.ExProdNat.const value_1) =
    (value = value_1)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctorCore.map₂_associator : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictPseudofunctorCore B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  self.map₂ (CategoryTheory.Bicategory.associator f g h).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator (self.map f) (self.map g) (self.map h)).hom (CategoryTheory.eqToHom ⋯))
-- Lean.Exception
/-- Throw an unknown constant error message.
The end position of the range of `ref` should point at the unknown identifier.
See also `mkUnknownIdentifierMessage`.
 -/
Lean.throwUnknownConstantAt : {m : Type → Type} → {α : Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Syntax → Lean.Name → m α
-- Mathlib.Data.Nat.Cast.SetInterval
Nat.image_cast_int_Iio : ∀ (a : ℕ), Nat.cast '' Set.Iio a = Set.Ico 0 ↑a
-- Mathlib.Algebra.Group.Subsemigroup.Membership
AddSubsemigroup.mem_sup_right : ∀ {M : Type u_2} [inst : Add M] {S T : AddSubsemigroup M} {x : M}, x ∈ T → x ∈ S ⊔ T
-- Init.Data.String.Lemmas.Pattern.Basic
/-- Predicate stating that there is a \(longest\) match starting at the given position.
 -/
String.Slice.Pattern.Model.MatchesAt : {ρ : Type} → (pat : ρ) → [String.Slice.Pattern.Model.PatternModel pat] → {s : String.Slice} → s.Pos → Prop
-- Mathlib.SetTheory.Ordinal.Veblen
/-- The epsilon function enumerates the fixed points of `ω ^ ⬝`.
This is an abbreviation for `veblen 1`. 

Conventions for notations in identifiers:

 * The recommended spelling of `ε_ ` in identifiers is `epsilon`. -/
Ordinal.termε_ : Lean.ParserDescr
-- Mathlib.Order.WithBot
WithTop.exists_lt_coe : ∀ {α : Type u_1} {a : α} [inst : Preorder α] {p : WithTop α → Prop}, (∃ x < ↑a, p x) ↔ ∃ b < a, p ↑b
-- Mathlib.Combinatorics.SimpleGraph.Star
/-- Every non-center vertex of a starGraph has degree one.  -/
SimpleGraph.degree_starGraph_of_ne_center : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] {r v : V}, v ≠ r → (SimpleGraph.starGraph r).degree v = 1
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.chromaticNumber_eq_biInf : ∀ {V : Type u} (G : SimpleGraph V), G.chromaticNumber = ⨅ n ∈ Set.ofPred G.Colorable, ↑n
-- Mathlib.Data.PNat.Prime
PNat.Coprime.gcd_mul_left_cancel_right : ∀ (m : ℕ+) {n k : ℕ+}, k.Coprime m → m.gcd (k * n) = m.gcd n
-- Mathlib.Algebra.Order.Group.Abs
eq_of_mabs_div_eq_one : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b : G}, |a / b|ₘ = 1 → a = b
-- Mathlib.Analysis.Normed.Module.Basic
/-- This is a simpler version of `dist_algebraMap` when `‖1‖ = 1` in `𝕜'`.  -/
dist_algebraMap' : ∀ {𝕜 : Type u_1} (𝕜' : Type u_2) [inst : NormedField 𝕜] [inst_1 : SeminormedRing 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜']
  [NormOneClass 𝕜'] (x y : 𝕜), dist ((algebraMap 𝕜 𝕜') x) ((algebraMap 𝕜 𝕜') y) = dist x y
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
/-- curve integral is defined using Bochner integral,
thus it is defined as zero whenever the codomain is not a complete space.  -/
curveIntegral_of_not_completeSpace : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E},
  ¬CompleteSpace F → ∀ (ω : E → E →L[𝕜] F) (γ : Path a b), ∫ᶜ (x : E) in γ, ω x = 0
-- Mathlib.Algebra.Star.Module
star_natCast_smul : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : StarAddMonoid M] (n : ℕ) (x : M), star (↑n • x) = ↑n • star x
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.isClosed : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] (a : A), IsClosed (spectrum 𝕜 a)
-- Mathlib.Order.Filter.IsBounded
/-- `f` is eventually bounded if and only if, there exists an admissible set on which it is
bounded.  -/
Filter.isBounded_iff : ∀ {α : Type u_1} {r : α → α → Prop} {f : Filter α}, Filter.IsBounded r f ↔ ∃ s ∈ f.sets, ∃ b, s ⊆ {x | r x b}
-- Mathlib.Data.Set.FiniteExhaustion
Set.FiniteExhaustion.prod_apply : ∀ {α : Type u_1} {s : Set α} (K : s.FiniteExhaustion) {β : Type u_2} {t : Set β} (K' : t.FiniteExhaustion) (n : ℕ),
  (K.prod K') n = K n ×ˢ K' n
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.upperCentralSeries.StrictMonoOn`. -/
upperCentralSeries.StrictMonoOn : ∀ (G : Type u_1) [inst : Group G], StrictMonoOn (Subgroup.upperCentralSeries G) (Set.Iic (Group.nilpotencyClass G))
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.comp_mapComp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.LaxFunctor B C) (G : CategoryTheory.LaxFunctor C D)
  {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (F.comp G).mapComp f g = CategoryTheory.CategoryStruct.comp (G.mapComp (F.map f) (F.map g)) (G.map₂ (F.mapComp f g))
-- Std.Time.Duration
Std.Time.Duration.instHSubOffset_1 : HSub Std.Time.Duration Std.Time.Week.Offset Std.Time.Duration
-- Batteries.Linter.UnreachableTactic
/-- Enables the 'unreachable tactic' linter. This will warn on any tactics that are never executed.
For example, in `example : True := by trivial <;> done`, the tactic `done` is never executed
because `trivial` produces no subgoals; you could put `sorry` or `apply I_don't_exist`
or anything else there and no error would result.

A common source of such things is `simp <;> tac` in the case that `simp` improves and
closes a subgoal that was previously being closed by `tac`.
 -/
Batteries.Linter.linter.unreachableTactic : Lean.Option Bool
-- Mathlib.Order.Atoms
Set.isCoatom_iff : ∀ {α : Type u_2} (s : Set α), IsCoatom s ↔ ∃ x, s = {x}ᶜ
-- Mathlib.Lean.Thunk
Thunk.get_mk : ∀ {α : Type u_1} (f : Unit → α), { fn := f }.get = f ()
-- Mathlib.Algebra.Colimit.Module
/-- Consider direct limits `lim G` and `lim G'` with direct system `f` and `f'` respectively, any
family of equivalences `eᵢ : Gᵢ ≅ G'ᵢ` such that `e ∘ f = f' ∘ e` induces an equivalence
`lim G ≅ lim G'`.
 -/
Module.DirectLimit.congr : {R : Type u_1} →
  [inst : Semiring R] →
    {ι : Type u_2} →
      [inst_1 : Preorder ι] →
        {G : ι → Type u_3} →
          [inst_2 : (i : ι) → AddCommMonoid (G i)] →
            [inst_3 : (i : ι) → Module R (G i)] →
              {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j} →
                [inst_4 : DecidableEq ι] →
                  {G' : ι → Type u_5} →
                    [inst_5 : (i : ι) → AddCommMonoid (G' i)] →
                      [inst_6 : (i : ι) → Module R (G' i)] →
                        {f' : (i j : ι) → i ≤ j → G' i →ₗ[R] G' j} →
                          (e : (i : ι) → G i ≃ₗ[R] G' i) →
                            (∀ (i j : ι) (h : i ≤ j), ↑(e j) ∘ₗ f i j h = f' i j h ∘ₗ ↑(e i)) →
                              Module.DirectLimit G f ≃ₗ[R] Module.DirectLimit G' f'
-- Mathlib.GroupTheory.Commutator.Basic
addCommutatorElement_neg_right : ∀ {G : Type u_1} [inst : AddGroup G] (a b : G), ⁅a, -b⁆ = -b + ⁅b, a⁆ + b
-- Init.Prelude
/-- Get the context name used in Note `Macro Scope Representation`.  -/
Lean.MonadQuotation.getMainModule : {m : Type → Type} → [self : Lean.MonadQuotation m] → m Lean.Name
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
CategoryTheory.IsGrothendieckAbelian.isomorphisms_le_pushouts_generatingMonomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : C) [CategoryTheory.Limits.HasZeroMorphisms C],
  CategoryTheory.MorphismProperty.isomorphisms C ≤
    (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms G).pushouts
-- Init.Prelude
/-- Replaces the current value of the mutable state with a new one.
 -/
MonadState.set : {σ : outParam (Type u)} → {m : Type u → Type v} → [self : MonadState σ m] → σ → m PUnit.{u + 1}
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.coe_orderIso_refl : ∀ (α : Type u_2) [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α], ↑(OrderRingIso.refl α) = OrderIso.refl α
-- Init.Data.List.Lemmas
List.getElem?_cons_succ : ∀ {α : Type u_1} {a : α} {i : ℕ} {l : List α}, (a :: l)[i + 1]? = l[i]?
-- Mathlib.Algebra.Category.Ring.Basic
/-- The object in the category of commutative rings associated to a type equipped with the
appropriate typeclasses.  -/
CommRingCat.of : (carrier : Type u) → [commRing : CommRing carrier] → CommRingCat
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.toCycles_eq_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i j : ι} [inst_2 : K.HasHomology j],
  ¬c.Rel i j → K.toCycles i j = 0