mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Category.TopCat.Opens
/-- An inducing map `f : X ⟶ Y` induces a functor `Opens X ⥤ Opens Y`.  -/
Topology.IsInducing.functor : {X Y : TopCat} →
  {f : X ⟶ Y} →
    Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f) →
      CategoryTheory.Functor (TopologicalSpace.Opens ↑X) (TopologicalSpace.Opens ↑Y)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_toArray_iff_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α] {k : α}
  {v : β}, m.WF → ((k, v) ∈ m.toArray ↔ m[k]? = some v)
-- Init.Data.Repr
instReprULift : {α : Type u_1} → [Repr α] → Repr (ULift.{v, u_1} α)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_le_size_alter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF → ∀ {k : α} {f : Option (β k) → Option (β k)}, t.size - 1 ≤ (Std.DTreeMap.Internal.Impl.alter! k f t).size
-- Init.Data.Rat.Basic
Rat.instAdd : Add ℚ
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
CategoryTheory.Limits.inr_comp_pushoutObjIso_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Limits.HasPushouts C] (f : F ⟶ G) (g : F ⟶ H) (d : D)
  {Z : C} (h : CategoryTheory.Limits.pushout (f.app d) (g.app d) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.pushout.inr f g).app d)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutObjIso f g d).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (f.app d) (g.app d)) h
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.partition_fst : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → Bool}, (Std.TreeMap.Raw.partition f t).1.WF
-- Mathlib.Algebra.Ring.Rat
Rat.commGroupWithZero : CommGroupWithZero ℚ
-- Lean.Parser.Term
/-- Indicates that an argument to a function marked `@[extern]` is borrowed.

Being borrowed only affects the ABI and runtime behavior of the function when compiled or interpreted. From the perspective of Lean's type system, this annotation has no effect. It similarly has no effect on functions not marked `@[extern]`.

When a function argument is borrowed, the function does not consume the value. This means that the function will not decrement the value's reference count or deallocate it, and the caller is responsible for doing so.

Please see https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=ffi-borrowing for a complete description.
 -/
Lean.Parser.Term.borrowed : Lean.Parser.Parser
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.smul : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {R : Type u_8}
  [inst_1 : NormedAddCommGroup R] [inst_2 : SMulZeroClass R E] [IsBoundedSMul R E] {f : ℝ → E},
  IntervalIntegrable f μ a b → ∀ (r : R), IntervalIntegrable (r • f) μ a b
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
/-- Any field is integral closed.  -/
Field.instIsIntegrallyClosed : ∀ (K : Type u_1) [inst : Field K], IsIntegrallyClosed K
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.SMulMemClass.coe_subtype : ∀ {R : Type u} {M : Type v} [inst : AddMonoid R] [inst_1 : AddAction R M] {A : Type u_1} [inst_2 : SetLike A M]
  [hA : VAddMemClass A R M] (S' : A), ⇑(SubAddAction.SMulMemClass.subtype S') = Subtype.val
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.IsReduced.linearIndependent : ∀ {ι : 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) {i j : ι}
  [P.IsReduced], i ≠ j → P.root i ≠ -P.root j → LinearIndependent R ![P.root i, P.root j]
-- Mathlib.GroupTheory.MonoidLocalization.Order
AddLocalization.instLinearAddOrderOfIsOrderedAddCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedCancelAddMonoid α]
  {s : AddSubmonoid α},
  AddLocalization.instLinearAddOrderOfIsOrderedAddCancelMonoid =
    { toPartialOrder := AddLocalization.partialOrder, min := fun a b => if a ≤ b then a else b,
      max := fun a b => if a ≤ b then b else a, compare := fun a b => compareOfLessAndEq a b, le_total := ⋯,
      toDecidableLE := AddLocalization.decidableLE, toDecidableEq := AddLocalization.decidableEq,
      toDecidableLT := AddLocalization.decidableLT, min_def := ⋯, max_def := ⋯, compare_eq_compareOfLessAndEq := ⋯ }
-- Mathlib.Logic.Equiv.Prod
Equiv.prodComm_apply : ∀ {α : Type u_9} {β : Type u_10} (x : α × β), (Equiv.prodComm α β) x = x.swap
-- Mathlib.AlgebraicGeometry.Cover.Over
/-- Bundle an `S`-scheme with `P` into an object of `P.Over ⊤ S`.  -/
AlgebraicGeometry.Scheme.asOverProp : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  (X S : AlgebraicGeometry.Scheme) → [inst : X.Over S] → P (X ↘ S) → P.Over ⊤ S
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.RealizeValueResult.res? : Lean.Meta.RealizeValueResult✝ → Except Lean.Exception Dynamic
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_toNonUnitalRingHom : ∀ {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (f : R ≃+* S), ⇑↑f = ⇑f
-- Mathlib.Data.Finset.Sups
/-- `s \\ t` is the finset of elements of the form `a \ b` where `a ∈ s`, `b ∈ t`.  -/
FinsetFamily.«term_\\_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Finset.hasSum_compl_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalAddGroup α]
  {f : β → α} {a : α} (s : Finset β), HasSum (fun x => f ↑x) a ↔ HasSum f (a + ∑ i ∈ s, f i)
-- Mathlib.Tactic.Linter.TextBased.UnicodeLinter
/-- Unicode symbols in mathlib that should always be followed by the text variant selector.  -/
Mathlib.Linter.TextBased.UnicodeLinter.nonEmojis : Array Char
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- The auxiliary sequence for a normalised EDS `W : ℤ → R`, with initial values
`W(0) = 0`, `W(1) = 1`, `W(2) = 1`, `W(3) = c`, and `W(4) = d` and extra parameter `b`.

This extends `preNormEDS'` by defining its values at negative integers.  -/
preNormEDS : {R : Type u_1} → [CommRing R] → R → R → R → ℤ → R
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
/-- Pull-out property of the conditional expectation.  -/
MeasureTheory.condExp_bilin_of_stronglyMeasurable_left : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_2} {F : Type u_3} {G : Type u_4}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] [CompleteSpace G] (B : F →L[ℝ] E →L[ℝ] G) [CompleteSpace E]
  {f : Ω → F} {g : Ω → E},
  MeasureTheory.StronglyMeasurable f →
    MeasureTheory.Integrable (fun ω => (B (f ω)) (g ω)) μ →
      MeasureTheory.Integrable g μ → μ[fun ω => (B (f ω)) (g ω) | m] =ᵐ[μ] fun ω => (B (f ω)) (μ[g | m] ω)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_indicator : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet s → ∀ (f : α → ENNReal), ∫⁻ (a : α) in t, s.indicator f a ∂μ = ∫⁻ (a : α) in s ∩ t, f a ∂μ
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.Bicone.diagram.inj : ∀ {J : Type u₁} {val val_1 : J}, CategoryTheory.Bicone.diagram val = CategoryTheory.Bicone.diagram val_1 → val = val_1
-- Mathlib.FieldTheory.Finiteness
/-- In a Noetherian module over a division ring,
`Basis.ofVectorSpace` is indexed by a finite type.  -/
IsNoetherian.instFintypeElemOfVectorSpaceIndex : {K : Type u} →
  {V : Type v} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] → [IsNoetherian K V] → Fintype ↑(Module.Basis.ofVectorSpaceIndex K V)
-- Mathlib.Algebra.Regular.Basic
/-- If a sum is add-regular, so is its right summand.  -/
IsAddRegular.of_add_right : ∀ {R : Type u_1} [inst : AddCommSemigroup R] {a b : R}, IsAddRegular (a + b) → IsAddRegular b
-- Std.Sync.RecursiveMutex
Std.RecursiveMutex.mutex : {α : Type} → Std.RecursiveMutex α → Std.BaseRecursiveMutex
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.image_symm_eq_preimage : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S)
  (s : Set S), ⇑e.symm '' s = ⇑e ⁻¹' s
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
Bundle.Trivialization.contMDiffOn : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8}
  [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)]
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_11 : (x : B) → TopologicalSpace (E x)] [inst_12 : FiberBundle F E] [inst_13 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle n F E IB] (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e],
  ContMDiffOn (IB.prod (modelWithCornersSelf 𝕜 F)) (IB.prod (modelWithCornersSelf 𝕜 F)) n (↑e) e.source
-- Init.Data.List.Perm
List.Perm.congr_left : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Perm l₂ → ∀ (l₃ : List α), l₁.Perm l₃ ↔ l₂.Perm l₃
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
/-- The `2`-truncated nerve functor is fully faithful.  -/
CategoryTheory.nerve.fullyFaithfulNerveFunctor₂ : CategoryTheory.Nerve.nerveFunctor₂.FullyFaithful
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RciSlice : (α : Type u_1) → Type u_2 → [Ord α] → Type (max u_2 u_1)
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.map_inf : ∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] (L M : BooleanSubalgebra α)
  (f : BoundedLatticeHom α β),
  Function.Injective ⇑f → BooleanSubalgebra.map f (L ⊓ M) = BooleanSubalgebra.map f L ⊓ BooleanSubalgebra.map f M
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instAddCommSemigroup : {R : Type u_3} → {A : Type u_4} → [AddCommSemigroup R] → [AddCommSemigroup A] → AddCommSemigroup (Unitization R A)
-- Lean.Elab.DefView
/-- State after elaboration.  -/
Lean.Elab.BodyProcessedSnapshot.state : Lean.Elab.BodyProcessedSnapshot → Lean.Elab.Term.SavedState
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.DominatedFinMeasAdditive.sub_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} {β : Type u_7} [inst : SeminormedAddCommGroup β] {T T' : Set α → β} {C C' : ℝ}
  (μ ν : MeasureTheory.Measure α),
  MeasureTheory.DominatedFinMeasAdditive μ T C →
    MeasureTheory.DominatedFinMeasAdditive ν T' C' → MeasureTheory.DominatedFinMeasAdditive (μ + ν) (T - T') (max C C')
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
/-- structure 2-morphism for composition of 1-morphism  -/
CategoryTheory.StrictlyUnitaryLaxFunctorCore.mapComp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (self : CategoryTheory.StrictlyUnitaryLaxFunctorCore B C) →
          {a b c : B} →
            (f : a ⟶ b) →
              (g : b ⟶ c) →
                CategoryTheory.CategoryStruct.comp (self.map f) (self.map g) ⟶
                  self.map (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- The inf of an indexed family of orthogonal subspaces equals the
subspace orthogonal to the sup.  -/
ClosedSubmodule.iInf_orthogonal : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_7} (K : ι → ClosedSubmodule 𝕜 E), ⨅ i, (K i)ᗮ = (iSup K)ᗮ
-- Aesop.Tree.TreeM
Aesop.getRootGoal : Aesop.TreeM Aesop.GoalRef
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.PInfty_comp_QInfty : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C},
  CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty AlgebraicTopology.DoldKan.QInfty = 0
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
/-- Define a left action of `C` on `D` from a left action of `Cᵒᵖ` on `Dᵒᵖ` via
the formula `c ⊙ₗ d = unop ((op c) ⊙ₗ (op d))`.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftActionOfOppositeLeftAction : (C : Type u_1) →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.MonoidalCategory C] →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [CategoryTheory.MonoidalCategory.MonoidalLeftAction Cᵒᵖ Dᵒᵖ] →
            CategoryTheory.MonoidalCategory.MonoidalLeftAction C D
-- Mathlib.SetTheory.Ordinal.Basic
/-- The order type of a well order is an ordinal.  -/
Ordinal.type : {α : Type u} → (r : α → α → Prop) → [wo : IsWellOrder α r] → Ordinal.{u}
-- Init.Grind.Ordered.Field
Lean.Grind.Field.IsOrdered.mul_lt_mul_iff_of_neg_right : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a b c : R}, c < 0 → (a * c < b * c ↔ b < a)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_ofList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k : α}, k ∈ Std.DHashMap.Raw.ofList l ↔ (List.map Sigma.fst l).contains k = true
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation_ι_app_hom : ∀ {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.HasColimitsOfShape J C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (j : J) (k : K),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.colimit.ι F j).app k)
      (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F k).hom =
    CategoryTheory.Limits.colimit.ι (F.comp ((CategoryTheory.evaluation K C).obj k)) j
-- Mathlib.Algebra.Star.Subalgebra
StarAlgebra.self_mem_adjoin_singleton : ∀ (R : Type u_2) {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (x : A), x ∈ StarAlgebra.adjoin R {x}
-- Mathlib.Data.List.Sublists
List.sublistsAux_eq_array_foldl : ∀ {α : Type u}, List.sublistsAux = fun a r => (Array.foldl (fun r l => (r.push l).push (a :: l)) #[] r.toArray).toList
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
EulerSine.antideriv_cos_comp_const_mul : ∀ {z : ℂ}, z ≠ 0 → ∀ (x : ℝ), HasDerivAt (fun y => Complex.sin (2 * z * ↑y) / (2 * z)) (Complex.cos (2 * z * ↑x)) x
-- Lean.Meta.Tactic.Grind.EMatchAction
_private.Lean.Meta.Tactic.Grind.EMatchAction.0.Lean.Meta.Grind.Action.CollectState.mk.sizeOf_spec : ∀ (visited : Std.HashSet Lean.Meta.Sym.ExprPtr)
  (collectedThms : Std.HashSet (Lean.Meta.Grind.Origin × Lean.Meta.Grind.EMatchTheoremKind))
  (thms : Array Lean.Meta.Grind.EMatchTheorem),
  sizeOf { visited := visited, collectedThms := collectedThms, thms := thms } =
    1 + sizeOf visited + sizeOf collectedThms + sizeOf thms
-- Mathlib.Order.CompleteBooleanAlgebra
Order.Coframe.toHNot : {α : Type u_1} → [self : Order.Coframe α] → HNot α
-- Init.Core
/-- The disjoint union of types `α` and `β`, ordinarily written `α ⊕ β`.

An element of `α ⊕ β` is either an `a : α` wrapped in `Sum.inl` or a `b : β` wrapped in `Sum.inr`.
`α ⊕ β` is not equivalent to the set-theoretic union of `α` and `β` because its values include an
indication of which of the two types was chosen. The union of a singleton set with itself contains
one element, while `Unit ⊕ Unit` contains distinct values `inl ()` and `inr ()`.
 -/
«term_⊕_» : Lean.TrailingParserDescr
-- Init.Dynamic
_private.Init.Dynamic.0.Dynamic.get?Impl : (α : Type u_1) → Dynamic → [TypeName α] → Option α
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.mem_fixedSubmodule_transvection_iff : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {f : Module.Dual R V}
  {v : V} {hfv : f v = 0} {x : V}, x ∈ (↑(LinearEquiv.transvection hfv)).fixedSubmodule ↔ f x • v = 0
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.localization_map : ∀ {R : Type u_4} {A : Type u_5} {Rₘ : Type u_6} {Sₘ : Type u_7} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : CommRing Rₘ] [inst_3 : CommRing Sₘ] (M : Submonoid R) [inst_4 : Algebra R A] [inst_5 : Algebra R Sₘ]
  [inst_6 : Algebra A Sₘ] [inst_7 : Algebra R Rₘ] [inst_8 : Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ]
  [IsScalarTower R A Sₘ] [IsLocalization M Rₘ] [IsLocalization (Submonoid.map (algebraMap R A) M) Sₘ]
  [Algebra.FormallySmooth R A], Algebra.FormallySmooth Rₘ Sₘ
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.sum_C : ∀ {R : Type u} {σ : Type u_1} {a : R} [inst : CommSemiring R] {A : Type u_2} [inst_1 : AddCommMonoid A]
  {b : (σ →₀ ℕ) → R → A}, b 0 0 = 0 → (MvPolynomial.C a).coeff.sum b = b 0 a
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.not_connected_bot : ∀ {V : Type u} [Nontrivial V], ¬⊥.Connected
-- Std.Internal.UV.System
Std.Internal.UV.System.UnameInfo.version : Std.Internal.UV.System.UnameInfo → String
-- Mathlib.CategoryTheory.Sites.Point.Category
CategoryTheory.GrothendieckTopology.Point.id_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point),
  (CategoryTheory.CategoryStruct.id Φ).hom = CategoryTheory.CategoryStruct.id Φ.fiber
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
/-- The counit 2-morphism of the comonad.  -/
CategoryTheory.Bicategory.«termε[_]» : Lean.ParserDescr
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.comp_neg : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_8} {N₂ : Type u_12} {N₃ : Type u_13} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommGroup N₂]
  [inst_5 : AddCommGroup N₃] [inst_6 : Module R₁ M] [inst_7 : Module R₂ N₂] [inst_8 : Module R₃ N₃] {σ₁₂ : R₁ →+* R₂}
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] N₂) (g : N₂ →ₛₗ[σ₂₃] N₃),
  g ∘ₛₗ (-f) = -g ∘ₛₗ f
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.smul_ae : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] (c : G),
  c • MeasureTheory.ae μ = MeasureTheory.ae μ
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv_apply_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z)
  (g : Y ⟶ Z)
  (pb :
    (i : Function.Pullback f.f g.f) →
      CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯))
        (g.φ (↑i).2))
  (hpb : (i : Function.Pullback f.f g.f) → CategoryTheory.Limits.IsLimit (pb i))
  (T : CategoryTheory.Limits.FormalCoproduct C)
  (m : T ⟶ (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).pt),
  ↑((CategoryTheory.Limits.FormalCoproduct.homPullbackEquiv f g pb hpb T) m) =
    (CategoryTheory.CategoryStruct.comp m (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).fst,
      CategoryTheory.CategoryStruct.comp m (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).snd)
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- A graph embedding is an embedding `f` such that for vertices `v w : V`,
`G'.Adj (f v) (f w) ↔ G.Adj v w`. Its image is an induced subgraph of G'.

The notation `G ↪g G'` represents the type of graph embeddings.  -/
SimpleGraph.«term_↪g_» : Lean.TrailingParserDescr
-- Mathlib.Data.ZMod.QuotientGroup
MulAction.minimalPeriod_eq_card : ∀ {α : Type u_3} {β : Type u_4} [inst : Group α] (a : α) [inst_1 : MulAction α β] (b : β)
  [inst_2 : Fintype ↑(MulAction.orbit (↥(Subgroup.zpowers a)) b)],
  Function.minimalPeriod (fun x => a • x) b = Fintype.card ↑(MulAction.orbit (↥(Subgroup.zpowers a)) b)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- We construct explicitly the data that specify the coproduct of a given family of formal
coproducts.  -/
CategoryTheory.Limits.FormalCoproduct.cofan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (𝒜 : Type w) → (f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C) → CategoryTheory.Limits.Cofan f
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.derives_nonterminal : ∀ {T : Type u_1} {g : ContextFreeGrammar T} {t : g.NT},
  (∀ r ∈ g.rules, r.input ≠ t) →
    ∀ (s : List (Symbol T g.NT)), s ≠ [Symbol.nonterminal t] → ¬g.Derives [Symbol.nonterminal t] s
-- Mathlib.Algebra.Order.Kleene
IdemSemiring.toIsOrderedAddMonoid : ∀ {α : Type u_1} [inst : IdemSemiring α], IsOrderedAddMonoid α
-- Init.Data.SInt.Lemmas
Int32.lt_or_lt_of_ne : ∀ {a b : Int32}, a ≠ b → a < b ∨ b < a
-- Lean.Elab.Binders
/-- Auxiliary datatype for elaborating binders.  -/
Lean.Elab.Term.BinderView : Type
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.coe_ofBijective : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R B] (f : A →ₐc[R] B) (hf : Function.Bijective ⇑f),
  ⇑(BialgEquiv.ofBijective f hf) = ⇑f
-- Mathlib.MeasureTheory.Group.Arithmetic
measurableVAdd_opposite_of_add : ∀ {M : Type u_2} [inst : Add M] [inst_1 : MeasurableSpace M] [MeasurableAdd M], MeasurableVAdd Mᵃᵒᵖ M
-- Mathlib.Tactic.Algebra.Basic
/-- `ExProd BaseType sα e` stores the structure of a normalized monomial expression `e`.
A monomial here is a product of powers of `ExBase` expressions, terminated by a (nonzero) constant
coefficient. The data of the constant coefficient is stored in the `BaseType`.  -/
Mathlib.Tactic.Algebra.ExProd : {u v : Lean.Level} →
  {R : Q(Type u)} →
    {A : Q(Type v)} → {sR : Q(CommSemiring «$R»)} → {sA : Q(CommSemiring «$A»)} → Q(Algebra «$R» «$A») → Q(«$A») → Type
-- Init.Data.Range.Polymorphic.UInt
UInt64.instLawfulUpwardEnumerableLE : Std.PRange.LawfulUpwardEnumerableLE UInt64
-- Init.Data.SInt.Basic
/-- Converts `true` to `1` and `false` to `0`.
 -/
Bool.toInt32 : Bool → Int32
-- Lean.Elab.Do.Basic
Lean.Elab.Do.getReturnCont : Lean.Elab.Do.DoElabM Lean.Elab.Do.ReturnCont
-- Init.Data.Nat.Coprime
Nat.Coprime.gcd_mul_right_cancel_right : ∀ {k m : ℕ} (n : ℕ), k.Coprime m → m.gcd (n * k) = m.gcd n
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.OverClass.asOverHom_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (S : C) [inst_1 : CategoryTheory.OverClass X S]
  [inst_2 : CategoryTheory.OverClass Y S] [inst_3 : CategoryTheory.OverClass Z S] (f : X ⟶ Y) (g : Y ⟶ Z)
  [inst_4 : CategoryTheory.HomIsOver f S] [inst_5 : CategoryTheory.HomIsOver g S] {Z_1 : CategoryTheory.Over S}
  (h : CategoryTheory.OverClass.asOver Z S ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.OverClass.asOverHom S (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.OverClass.asOverHom S f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.OverClass.asOverHom S g) h)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.mkMonoidHom.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : MulOneClass M] [inst_2 : ContinuousMul M],
  SeparationQuotient.mkMonoidHom = { toFun := SeparationQuotient.mk, map_one' := ⋯, map_mul' := ⋯ }