mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Analytic.Basic
/-- Given a function `f : E → F`, we say that `f` is analytic at `x` if it admits a convergent power
series expansion around `x`.  -/
AnalyticAt : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [NormedSpace 𝕜 E] → [inst_3 : NormedAddCommGroup F] → [NormedSpace 𝕜 F] → (E → F) → E → Prop
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.SubmersivePresentation.HasCoeffs.coeffs_subset_range : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} {inst : CommRing R} {inst_1 : CommRing S}
  {inst_2 : Algebra R S} {inst_3 : Finite σ} {P : Algebra.SubmersivePresentation R S ι σ} {R₀ : Type u_5}
  {inst_4 : CommRing R₀} {inst_5 : Algebra R₀ R} {inst_6 : Algebra R₀ S} {inst_7 : IsScalarTower R₀ R S}
  [self : P.HasCoeffs R₀], P.coeffs ⊆ ↑(algebraMap R₀ R).range
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.add_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  {f g : E →SWOT[σ] F} (x : E), (f + g) x = f x + g x
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.Infinitesimal.eq_zero : ∀ {r : ℝ}, (↑r).Infinitesimal → r = 0
-- Mathlib.Topology.NhdsWithin
instNeBotNhdsWithinUnivPi : ∀ {ι : Type u_5} {X : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (X i)] {s : (i : ι) → Set (X i)}
  {x : (i : ι) → X i} [∀ (i : ι), (nhdsWithin (x i) (s i)).NeBot], (nhdsWithin x (Set.univ.pi s)).NeBot
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
/-- the index attached to the corresponding type (II) simplex  -/
SSet.prodStdSimplex.pairingCore.Type₁.index : {m : ℕ} → {k : Fin (m + 1)} → {n : ℕ} → (self : SSet.prodStdSimplex.pairingCore.Type₁ k n) → Fin (self.d + 1)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instSupSet.eq_1 : ∀ {R : Type u} {M : Type v} [inst : SMul R M],
  SubMulAction.instSupSet = { sSup := fun S => { carrier := ⋃ s ∈ S, ↑s, smul_mem' := ⋯ } }
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.commMonoid : {α : Type u_2} → [inst : CommMonoid α] → [inst_1 : Preorder α] → [IsOrderedMonoid α] → CommMonoid (NonemptyInterval α)
-- Std.Data.Iterators.Lemmas.Equivalence.Basic
/-- Makes a step with a bundled iterator in the `HetT` monad.
 -/
Std.BundledIterM.step : {β : Type w} →
  {m : Type w → Type w'} →
    [inst : Monad m] →
      [LawfulMonad m] → Std.BundledIterM m β → Std.Iterators.HetT m (Std.IterStep (Std.BundledIterM m β) β)
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
MvPowerSeries.WithPiTopology.instTopologicalSpace_mono : ∀ (σ : Type u_3) {R : Type u_4} {t u : TopologicalSpace R},
  t ≤ u → MvPowerSeries.WithPiTopology.instTopologicalSpace R ≤ MvPowerSeries.WithPiTopology.instTopologicalSpace R
-- Mathlib.Dynamics.Flow
/-- Restrict a flow by `τ` to a flow by the additive submonoid of nonnegative elements of `τ`.  -/
Flow.restrictNonneg : {τ : Type u_1} →
  {α : Type u_2} →
    [inst : TopologicalSpace τ] →
      [inst_1 : TopologicalSpace α] →
        [inst_2 : AddMonoid τ] →
          Flow τ α → [inst_3 : Preorder τ] → [inst_4 : AddLeftMono τ] → Flow (↥(AddSubmonoid.nonneg τ)) α
-- Mathlib.CategoryTheory.Localization.Construction
/-- The morphism in the path category associated to a morphism in the original category.  -/
CategoryTheory.Localization.Construction.ψ₁ : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    (W : CategoryTheory.MorphismProperty C) →
      {X Y : C} →
        (X ⟶ Y) →
          (CategoryTheory.Localization.Construction.ιPaths W X ⟶ CategoryTheory.Localization.Construction.ιPaths W Y)
-- Init.Data.Order.Opposite
Std.OppositeOrderInstances.instLETotalOpposite : ∀ {α : Type u_1} {i : LE α} [Std.Total fun x1 x2 => x1 ≤ x2], Std.Total fun x1 x2 => x1 ≤ x2
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_inv_limit_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  {i j : K} (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (f : i ⟶ j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F i).inv
      ((CategoryTheory.Limits.limit F).map f) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limMap (F.whiskerLeft ((CategoryTheory.evaluation K C).map f)))
      (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F j).inv
-- Init.Data.SInt.Lemmas
Int16.add_zero : ∀ (a : Int16), a + 0 = a
-- Mathlib.ModelTheory.LanguageMap
/-- A language homomorphism maps the symbols of one language to symbols of another.  -/
FirstOrder.Language.«term_→ᴸ_» : Lean.TrailingParserDescr
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry?_eq_minEntry?ₘ' : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {l : Std.DTreeMap.Internal.Impl α β}, l.minEntry? = l.minEntry?ₘ'
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneUnopOfCoconeEquiv_inverse_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cone F.unop),
  CategoryTheory.Limits.coneUnopOfCoconeEquiv.inverse.obj c = Opposite.op (CategoryTheory.Limits.coconeOfConeUnop c)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.IsSymmetric.isSelfAdjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {A : E →L[𝕜] E}, (↑A).IsSymmetric → IsSelfAdjoint A
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_nat_mul_two_pi_sub_pi : ∀ (n : ℕ), Complex.cos (↑n * (2 * ↑Real.pi) - ↑Real.pi) = -1
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.isSome_getElem?_eq_contains : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, m[a]?.isSome = m.contains a
-- Mathlib.Order.BooleanAlgebra.Set
Set.mem_compl_singleton_iff : ∀ {α : Type u_1} {a b : α}, a ∈ {b}ᶜ ↔ a ≠ b
-- Mathlib.Data.List.Cycle
Cycle.chain_singleton : ∀ {α : Type u_1} (r : α → α → Prop) (a : α), Cycle.Chain r ↑[a] ↔ r a a
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instZeroAtInftyContinuousMapClass : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [ProperSpace E], ZeroAtInftyContinuousMapClass (SchwartzMap E F) E F
-- Mathlib.Order.Lex
ofColex_inj : ∀ {α : Type u_1} {a b : Colex α}, ofColex a = ofColex b ↔ a = b
-- Mathlib.Order.Category.BddLat
BddLat.dualEquiv_inverse : BddLat.dualEquiv.inverse = BddLat.dual
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.toBCF_injective : ∀ (α : Type u) (β : Type v) [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero β],
  Function.Injective ZeroAtInftyContinuousMap.toBCF
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roc_add_succ_right_eq_append' : ∀ {m n : ℕ}, (m<...=m + (n + 1)).toList = (m<...=m + n).toList ++ [m + n + 1]
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.symm_symm : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N), e.symm.symm = e
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.instNNNorm : {α : Type u_1} →
  {E : Type u_4} →
    {m : MeasurableSpace α} →
      {p : ENNReal} → {μ : MeasureTheory.Measure α} → [inst : NormedAddCommGroup E] → NNNorm ↥(MeasureTheory.Lp E p μ)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isSome_maxKey?_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t.contains k = true → t.maxKey?.isSome = true
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- Typeclass for a measurable space `α` for which the diagonal of `α × α` is measurable.  -/
MeasurableEq : (α : Type u_1) → [MeasurableSpace α] → Prop
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
/-- the dimension of the simplex  -/
SSet.S.dim : {X : SSet} → X.S → ℕ
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect.eq_1 : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] (s : Finset ι) (f : ι → M),
  s.expect f = (↑s.card)⁻¹ • ∑ i ∈ s, f i
-- Std.Http.Protocol.H1.Parser
/-- Parses `HTTP-version = HTTP-name "/" DIGIT "." DIGIT` and returns the major and
minor version numbers as a pair.
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.parseHttpVersionNumber : Std.Internal.Parsec.ByteArray.Parser (ℕ × ℕ)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.sum_add_index : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : AddCommMonoid S] (p q : Polynomial R) (f : ℕ → R → S),
  (∀ (i : ℕ), f i 0 = 0) → (∀ (a : ℕ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂) → (p + q).sum f = p.sum f + q.sum f
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instToJsonCodeActionLiteralSupportValueSet : Lean.ToJson Lean.Lsp.CodeActionLiteralSupportValueSet
-- Mathlib.Algebra.Order.Ring.Synonym
Lex.instNonUnitalNonAssocRing : {R : Type u_1} → [NonUnitalNonAssocRing R] → NonUnitalNonAssocRing (Lex R)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.RepToAction_obj_ρ : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G] (X : Rep.{w, u, v} k G),
  ((Rep.RepToAction k G).obj X).ρ = (ModuleCat.of k ↑X).endRingEquiv.symm.toMonoidHom.comp X.ρ
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.maxEntryD : {α : Type u} → {β : Type v} → (Std.DTreeMap.Internal.Impl α fun x => β) → α × β → α × β
-- Mathlib.AlgebraicGeometry.AlgClosed.Basic
AlgebraicGeometry.pointOfClosedPoint_comp_assoc : ∀ {X : AlgebraicGeometry.Scheme} {K : Type u} [inst : Field K] [inst_1 : IsAlgClosed K]
  (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K)) [inst_2 : AlgebraicGeometry.LocallyOfFiniteType f] (x : ↥X)
  (hx : IsClosed {x}) {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pointOfClosedPoint f x hx)
      (CategoryTheory.CategoryStruct.comp f h) =
    h
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_fst : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j k : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j k)
          (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j i))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
            (𝒰.f k))
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
        (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
      (CategoryTheory.Limits.pullback.snd
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
        (𝒰.f j))
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.range_inl : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W},
  Representation.IntertwiningMap.range ρ (ρ.prod σ) (Representation.IntertwiningMap.inl A ρ σ) =
    Representation.IntertwiningMap.ker (ρ.prod σ) σ (Representation.IntertwiningMap.snd A ρ σ)
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Prequotient.of.injEq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} (j : J)
  (x : ↑(F.obj j)) (j_1 : J) (x_1 : ↑(F.obj j_1)),
  (CommRingCat.Colimits.Prequotient.of j x = CommRingCat.Colimits.Prequotient.of j_1 x_1) = (j = j_1 ∧ x ≍ x_1)
-- Mathlib.Order.Concept
lowerPolar_iUnion : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (f : ι → Set β),
  lowerPolar r (⋃ i, f i) = ⋂ i, lowerPolar r (f i)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.comap_inf : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (S T : AddSubmonoid N) (f : F),
  AddSubmonoid.comap f (S ⊓ T) = AddSubmonoid.comap f S ⊓ AddSubmonoid.comap f T
-- Mathlib.Order.Heyting.Regular
/-- The Boolean algebra of Heyting regular elements.  -/
Heyting.Regular : (α : Type u_1) → [HeytingAlgebra α] → Type u_1
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
AddCircle.volume_closedBall : ∀ (T : ℝ) [hT : Fact (0 < T)] {x : AddCircle T} (ε : ℝ),
  MeasureTheory.volume (Metric.closedBall x ε) = ENNReal.ofReal (min T (2 * ε))
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- Lax associativity.  -/
CategoryTheory.LaxFunctor.map₂_associator : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.LaxFunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g) (self.map h))
      (CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h)
        (self.map₂ (CategoryTheory.Bicategory.associator f g h).hom)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (self.map f) (self.map g) (self.map h)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapComp g h))
        (self.mapComp f (CategoryTheory.CategoryStruct.comp g h)))
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycleOn.exists_pow_eq : ∀ {α : Type u_2} {f : Equiv.Perm α} {a b : α} {s : Finset α},
  f.IsCycleOn ↑s → a ∈ s → b ∈ s → ∃ n < s.card, (f ^ n) a = b
-- Mathlib.Topology.UniformSpace.UniformApproximation
/-- A function which can be uniformly approximated by functions which are continuous on a set
is continuous on this set.  -/
continuousOn_of_uniform_approx_of_continuousOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {f : α → β} {s : Set α},
  (∀ u ∈ uniformity β, ∃ F, ContinuousOn F s ∧ ∀ y ∈ s, (f y, F y) ∈ u) → ContinuousOn f s
-- Init.Data.List.Sublist
List.suffix_or_suffix_of_suffix : ∀ {α : Type u_1} {l₁ l₃ l₂ : List α}, l₁ <:+ l₃ → l₂ <:+ l₃ → l₁ <:+ l₂ ∨ l₂ <:+ l₁
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplexEquivIcc_zero : ∀ (𝕜 : Type u_1) [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : IsOrderedRing 𝕜],
  (stdSimplexEquivIcc 𝕜) ⟨Pi.single 0 1, ⋯⟩ = 0
-- Mathlib.Order.Preorder.Chain
/-- The type of flags, aka maximal chains, of an order.  -/
Flag : (α : Type u_4) → [LE α] → Type u_4
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
/-- Given an inequality `x ≤ y` between nondegenerate simplices of a
nonsingular simplicial set `X`, this is the corresponding morphism
`⦋x.dim⦌ ⟶ ⦋y.dim⦌` in the simplex category.  -/
SSet.N.monoOfLE : {X : SSet} → [X.Nonsingular] → {x y : X.N} → x ≤ y → ({ len := x.dim } ⟶ { len := y.dim })
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_mul_of_lt_of_one_lt : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftStrictMono α] {a b c : α},
  b < c → 1 < a → b < c * a
-- Mathlib.Data.List.NodupEquivFin
List.getEquivOfForallCountEqOne_symm_apply_val : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (h : ∀ (x : α), List.count x l = 1) (a : α),
  ↑((l.getEquivOfForallCountEqOne h).symm a) = List.idxOf a l
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.support_prefix_support_concat : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (hadj : G.Adj v w),
  p.support <+: (p.concat hadj).support
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- `δ` is the function underlying the arithmetic function `1`.  -/
ArithmeticFunction.one_eq_delta : (fun n => 1 n) = LSeries.delta
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.InductiveElabStep1.checkLevelNames : Array Lean.Elab.Command.InductiveView → Lean.Elab.TermElabM Unit
-- Mathlib.Topology.Compactification.StoneCech
stoneCechExtend_stoneCechUnit : ∀ {α : Type u} [inst : TopologicalSpace α] {β : Type v} [inst_1 : TopologicalSpace β] [inst_2 : T2Space β] {g : α → β}
  (hg : Continuous g) [inst_3 : CompactSpace β] (a : α), stoneCechExtend hg (stoneCechUnit a) = g a
-- Mathlib.Algebra.Module.LinearMap.Index
LinearMap.index_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {R : Type u_3} [inst_2 : Ring R]
  [inst_3 : Module R M] [inst_4 : Module R N] {f : M →ₗ[R] N} [StrongRankCondition R],
  Function.Surjective ⇑f → f.index = ↑(Module.finrank R ↥f.ker)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- The `carrier` of a `NonUnitalStarSubalgebra` is closed under the `star` operation.  -/
NonUnitalStarSubalgebra.star_mem' : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] (self : NonUnitalStarSubalgebra R A) {a : A}, a ∈ self.carrier → star a ∈ self.carrier
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.add_equiv : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P P' Q Q' : Fin 3 → R},
  P ≈ P' → Q ≈ Q' → W'.add P Q ≈ W'.add P' Q'
-- Mathlib.Logic.Function.FromTypes
/-- The definitional equality between `(vecCons α p)`-ary heterogeneous functions into `τ`
and function from `α` to `p`-ary heterogeneous functions into `τ`.  -/
Function.fromTypes_cons_equiv : {n : ℕ} →
  (α : Type u) →
    (p : Fin n → Type u) → (τ : Type u) → Function.FromTypes (Matrix.vecCons α p) τ ≃ (α → Function.FromTypes p τ)
-- Mathlib.Algebra.Group.Conj
/-- A `MonoidHom` maps conjugacy classes of one group to conjugacy classes of another.  -/
ConjClasses.map : {α : Type u} → {β : Type v} → [inst : Monoid α] → [inst_1 : Monoid β] → (α →* β) → ConjClasses α → ConjClasses β
-- Lean.Meta.WHNF
/-- Reduce kernel projection `Expr.proj ..` expression.  -/
Lean.Meta.reduceProj? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.restrict : ∀ {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε] {f : α → ε},
  MeasureTheory.HasFiniteIntegral f μ → ∀ {s : Set α}, MeasureTheory.HasFiniteIntegral f (μ.restrict s)
-- Mathlib.Algebra.GroupWithZero.WithZero
MulEquiv.withZero_apply_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Group α] [inst_1 : Group β] (e : α ≃* β) (a : WithZero α),
  (MulEquiv.withZero e) a = (WithZero.map' ↑e) a
-- Mathlib.Topology.UniformSpace.Cauchy
cauchySeq_iff : ∀ {α : Type u} [uniformSpace : UniformSpace α] {u : ℕ → α},
  CauchySeq u ↔ ∀ V ∈ uniformity α, ∃ N, ∀ k ≥ N, ∀ l ≥ N, (u k, u l) ∈ V
-- Lean.LabelAttribute
/-- Construct a new "label attribute",
which does nothing except keep track of the names of the declarations with that attribute.

Users will generally use the `register_label_attr` macro defined below.
 -/
Lean.registerLabelAttr : Lean.Name → String → autoParam Lean.Name Lean.registerLabelAttr._auto_1 → IO Lean.LabelExtension
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.le_mul_left : ∀ {a b : Cardinal.{u_1}}, b ≠ 0 → a ≤ b * a
-- Mathlib.Tactic.Simps.Basic
/-- Syntax for making a projection prefix.  -/
Lean.Parser.Command.simpsRule.prefix : Lean.ParserDescr
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_27 : HAdd Std.Time.Hour.Offset Std.Time.Minute.Offset Std.Time.Minute.Offset
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.isSeparated_maximalSeparatedSet : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A : Set X} {ε : NNReal},
  Metric.IsSeparated (↑ε) (Metric.maximalSeparatedSet ε A)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insertIfNew k v).minKey? = some (t.minKey?.elim k fun k' => if cmp k k' = Ordering.lt then k else k')
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Invariant.eq_1 : ∀ {α : Type u₁} (xs : List α) (β : Type u₂) (Pred : Type (max u₁ u₂)),
  Std.Internal.Do.Invariant xs β Pred = (xs.Cursor → β → Pred)
-- Mathlib.CategoryTheory.Galois.Topology
/-- If `G` is a fully faithful functor of categories finite types, this is the automorphism of
topological groups `Aut F ≃ Aut (F ⋙ G)`.  -/
CategoryTheory.PreGaloisCategory.autEquivAutWhiskerRight : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    (F : CategoryTheory.Functor C FintypeCat) →
      {G : CategoryTheory.Functor FintypeCat FintypeCat} →
        G.FullyFaithful → CategoryTheory.Aut F ≃ₜ* CategoryTheory.Aut (F.comp G)
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Power.denote.match_1.splitter : (motive : ℕ → Sort u_1) →
  (k : ℕ) → (Unit → motive 0) → (Unit → motive 1) → ((k : ℕ) → (k = 0 → False) → (k = 1 → False) → motive k) → motive k
-- Mathlib.LinearAlgebra.SModEq.Basic
Submodule.vadd_set_eq_vadd_set_iff : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {U : Submodule R M}
  {x y : M}, x +ᵥ ↑U = y +ᵥ ↑U ↔ x ≡ y [SMOD U]
-- Mathlib.Data.Fintype.EquivFin
Infinite.exists_notMem_finset : ∀ {α : Type u_1} [Infinite α] (s : Finset α), ∃ x, x ∉ s
-- Mathlib.Topology.Perfect
perfectSpace_iff_forall_not_isolated : ∀ {X : Type u_1} [inst : TopologicalSpace X], PerfectSpace X ↔ ∀ (x : X), (nhdsWithin x {x}ᶜ).NeBot
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The bundled derivative of a `C^{n+1}` function is `C^n`.  -/
contDiffOn_fderivWithin_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {m n : WithTop ℕ∞} {s : Set E}
  {f : E → F},
  ContDiffOn 𝕜 n f s →
    UniqueDiffOn 𝕜 s → m + 1 ≤ n → ContDiffOn 𝕜 m (fun p => (fderivWithin 𝕜 f s p.1) p.2) (s ×ˢ Set.univ)
-- Mathlib.Order.Filter.Map
Filter.comap_le_comap_iff : ∀ {α : Type u_1} {β : Type u_2} {f g : Filter β} {m : α → β},
  Set.range m ∈ f → (Filter.comap m f ≤ Filter.comap m g ↔ f ≤ g)
-- Init.Data.List.Nat.Prod
List.prod_pos_iff_forall_pos_nat : ∀ {l : List ℕ}, 0 < l.prod ↔ ∀ x ∈ l, 0 < x
-- Mathlib.Algebra.Quandle
/-- An involutory rack is one for which `Rack.oppositeRack R x` is an involution for every x.
 -/
Rack.IsInvolutory : (R : Type u_2) → [Rack R] → Prop
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Naturality of the left unitor, commutativity of `𝟙_ C ⊗ X ⟶ 𝟙_ C ⊗ Y ⟶ Y` and `𝟙_ C ⊗ X ⟶ X ⟶ Y`
 -/
CategoryTheory.MonoidalCategory.leftUnitor_naturality : ∀ {C : Type u} {𝒞 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.MonoidalCategory C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f)
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom f