mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Function.Defs
Function.uncurry_bicompl : ∀ {α : Type u_6} {β : Type u_7} {γ : Type u_8} {δ : Type u_9} {ε : Sort u_10} (f : γ → δ → ε) (g : α → γ) (h : β → δ),
  Function.uncurry (Function.bicompl f g h) = Function.uncurry f ∘ Prod.map g h
-- Mathlib.Algebra.Group.End
Equiv.Perm.sigmaCongrRight_one : ∀ {α : Type u_7} {β : α → Type u_8}, Equiv.Perm.sigmaCongrRight 1 = 1
-- Mathlib.Topology.Algebra.Algebra
continuousSMul_of_algebraMap : ∀ (R : Type u_1) (A : Type u) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : TopologicalSpace R] [inst_4 : TopologicalSpace A] [ContinuousMul A],
  Continuous ⇑(algebraMap R A) → ContinuousSMul R A
-- Mathlib.Topology.Gluing
TopCat.GlueData.ofOpenSubsets_toGlueData_U : ∀ {α : Type u} [inst : TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α)
  (a :
    { J := J, U := fun i => (TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U i),
        V := fun x j => (TopologicalSpace.Opens.map (U x).inclusion').obj (U j),
        t := fun i j => TopCat.ofHom { toFun := fun x => ⟨⟨↑↑x, ⋯⟩, ⋯⟩, continuous_toFun := ⋯ }, V_id := ⋯, t_id := ⋯,
        t_inter := ⋯, cocycle := ⋯ }.J),
  (TopCat.GlueData.ofOpenSubsets U).U a = (TopologicalSpace.Opens.toTopCat (TopCat.of α)).obj (U a)
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.GRing.toGSemiring : {ι : Type u_1} →
  {A : ι → Type u_2} →
    {inst : AddMonoid ι} → {inst_1 : (i : ι) → AddCommGroup (A i)} → [self : DirectSum.GRing A] → DirectSum.GSemiring A
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimApp.Result.alts : Lean.Elab.Tactic.ElimApp.Result → Array Lean.Elab.Tactic.ElimApp.Alt
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousSemilinearMapClass.toContinuousMapClass : ∀ {F : Type u_1} {R : outParam (Type u_2)} {S : outParam (Type u_3)} {inst : Semiring R} {inst_1 : Semiring S}
  {σ : outParam (R →+* S)} {M : outParam (Type u_4)} {inst_2 : TopologicalSpace M} {inst_3 : AddCommMonoid M}
  {M₂ : outParam (Type u_5)} {inst_4 : TopologicalSpace M₂} {inst_5 : AddCommMonoid M₂} {inst_6 : Module R M}
  {inst_7 : Module S M₂} {inst_8 : FunLike F M M₂} [self : ContinuousSemilinearMapClass F σ M M₂],
  ContinuousMapClass F M M₂
-- Std.Data.TreeMap.Lemmas
/-- Variant of `getElem_map` that holds without `LawfulEqCmp`.  -/
Std.TreeMap.getElem_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → γ} {k : α} {h' : k ∈ Std.TreeMap.map f t}, (Std.TreeMap.map f t)[k] = f (t.getKey k ⋯) t[k]
-- Mathlib.CategoryTheory.Action.Monoidal
Action.instMonoidalLinear : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [inst_1 : Monoid G]
  [inst_2 : CategoryTheory.MonoidalCategory V] [inst_3 : CategoryTheory.Preadditive V]
  [inst_4 : CategoryTheory.MonoidalPreadditive V] {R : Type u_3} [inst_5 : Semiring R]
  [inst_6 : CategoryTheory.Linear R V] [CategoryTheory.MonoidalLinear R V], CategoryTheory.MonoidalLinear R (Action V G)
-- Mathlib.CategoryTheory.Category.TwoP
pointedToTwoPFst_obj_toTwoPointing_toProd : ∀ (X : Pointed), (pointedToTwoPFst.obj X).toTwoPointing.toProd = (some X.point, none)
-- Mathlib.Order.Bounds.Image
mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β} {a : α} {b : β},
  (∀ (b : β), Monotone (Function.swap f b)) →
    (∀ (a : α), Antitone (f a)) → a ∈ lowerBounds s → b ∈ upperBounds t → f a b ∈ lowerBounds (Set.image2 f s t)
-- Mathlib.AlgebraicGeometry.AlgebraicCycle.Basic
AlgebraicGeometry.AlgebraicCycle.mapCoeff.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} {N : Type u_2} [inst : DecidableEq N] {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y)
  (wx : ↥X → N) (wy : ↥Y → N) (x : ↥X),
  AlgebraicGeometry.AlgebraicCycle.mapCoeff f wx wy x =
    if wx x = wy (f x) then AlgebraicGeometry.Scheme.Hom.residueDegree f x else 0
-- Init.Data.SInt.Lemmas
Int32.toInt32_toUInt32 : ∀ (x : Int32), x.toUInt32.toInt32 = x
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_lt_iff_lt_log : ∀ {x y z : ℝ}, 0 < x → 0 < y → (x ^ z < y ↔ z * Real.log x < Real.log y)
-- Mathlib.Topology.Algebra.Monoid
addHomOfTendsto_apply : ∀ {α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [inst : TopologicalSpace M₂] [inst_1 : T2Space M₂] [inst_2 : Add M₁]
  [inst_3 : Add M₂] [inst_4 : ContinuousAdd M₂] {F : Type u_8} [inst_5 : FunLike F M₁ M₂] [inst_6 : AddHomClass F M₁ M₂]
  {l : Filter α} (f : M₁ → M₂) (g : α → F) [inst_7 : l.NeBot] (h : Filter.Tendsto (fun a x => (g a) x) l (nhds f)),
  ⇑(addHomOfTendsto f g h) = f
-- Mathlib.Algebra.Polynomial.Laurent
Polynomial.toLaurent_X_pow : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), Polynomial.toLaurent (Polynomial.X ^ n) = LaurentPolynomial.T ↑n
-- Mathlib.Order.KrullDimension
Order.coheight_eq_krullDim_Ici : ∀ {α : Type u_3} [inst : Preorder α] (x : α), ↑(Order.coheight x) = Order.krullDim ↑(Set.Ici x)
-- Batteries.Recycling.RBTree.Basic
/-- True if `x` is an element of `t` "exactly", i.e. up to equality, not the `cmp` relation.  -/
RBTree.RBNode.EMem : {α : Type u_1} → α → RBTree.RBNode α → Prop
-- Mathlib.GroupTheory.GroupAction.Iwasawa
MulAction.IwasawaStructure.mk.sizeOf_spec : ∀ {M : Type u_1} [inst : Group M] {α : Type u_2} [inst_1 : MulAction M α] [inst_2 : SizeOf M] [inst_3 : SizeOf α]
  (T : α → Subgroup M) (is_comm : ∀ (x : α), IsMulCommutative ↥(T x))
  (is_conj : ∀ (g : M) (x : α), T (g • x) = MulAut.conj g • T x) (is_generator : iSup T = ⊤),
  sizeOf { T := T, is_comm := is_comm, is_conj := is_conj, is_generator := is_generator } = 1 + sizeOf is_generator
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.glue.congr_simp : ∀ {α : Type u} {β : α → Type v} (l l_1 : Std.DTreeMap.Internal.Impl α β) (e_l : l = l_1)
  (r r_1 : Std.DTreeMap.Internal.Impl α β) (e_r : r = r_1) (hl : l.Balanced) (hr : r.Balanced)
  (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size), l.glue r hl hr hlr = l_1.glue r_1 ⋯ ⋯ ⋯
-- Lean.Meta.WHNF
Lean.Meta.smartUnfolding : Lean.Option Bool
-- Lean.Meta.Tactic.Replace
/-- Replaces the type of the free variable `fvarId` with `typeNew`.

If `checkDefEq` is `true` then an error is thrown if `typeNew` is not definitionally
equal to the type of `fvarId`. Otherwise this function assumes `typeNew` and the type
of `fvarId` are definitionally equal.
 -/
Lean.MVarId.changeLocalDecl : Lean.MVarId → Lean.FVarId → Lean.Expr → optParam Bool true → Lean.MetaM Lean.MVarId
-- Mathlib.CategoryTheory.Limits.Constructions.EpiMono
CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan F],
  F.PreservesEpimorphisms
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
/-- If `c` is a cell of a rank function for a proper pairing `P`
of a subcomplex of a simplicial set, this is the index
in `Fin (c.dim + 2)` of the face of the type (I) simplex
given by the corresponding type (II) simplex.  -/
SSet.Subcomplex.Pairing.RankFunction.Cell.index : {X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} →
      {ι : Type v} →
        [inst : LinearOrder ι] → {f : P.RankFunction ι} → {i : ι} → (c : f.Cell i) → [P.IsProper] → Fin (c.dim + 2)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.ExtendTarget.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {newWidth : ℕ} (w : ℕ)
  (vec : aig.RefVec w) (w_1 : ℕ) (vec_1 : aig.RefVec w_1),
  ({ w := w, vec := vec } = { w := w_1, vec := vec_1 }) = (w = w_1 ∧ vec ≍ vec_1)
-- Mathlib.Topology.Order.Monotone
/-- An antitone function continuous at the indexed supremum over a nonempty `Sort` sends this
indexed supremum to the indexed infimum of the composition.  -/
Antitone.map_ciSup_of_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β]
  {ι : Sort u_3} [Nonempty ι] {f : α → β} {g : ι → α},
  ContinuousAt f (iSup g) →
    Antitone f →
      autoParam (BddAbove (Set.range g)) Antitone.map_ciSup_of_continuousAt._auto_1 → f (⨆ i, g i) = ⨅ i, f (g i)
-- Mathlib.RingTheory.OrderOfVanishing.Basic
Ring.ord.eq_1 : ∀ (R : Type u_1) [inst : Ring R] (x : R), Ring.ord R x = Module.length R (R ⧸ Ideal.span {x})
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffWithinAt_inter : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s t : Set M} {x : M}
  {n : WithTop ℕ∞}, t ∈ nhds x → (ContMDiffWithinAt I I' n f (s ∩ t) x ↔ ContMDiffWithinAt I I' n f s x)
-- Mathlib.RingTheory.Localization.Away.Basic
/-- For `s : S` with `S` being the localization of `R` away from `x`,
this is a choice of `(r, n) : R × ℕ` such that `s * algebraMap R S (x ^ n) = algebraMap R S r`.  -/
IsLocalization.Away.sec : {R : Type u_1} →
  [inst : CommSemiring R] →
    {S : Type u_2} →
      [inst_1 : CommSemiring S] → [inst_2 : Algebra R S] → (x : R) → [IsLocalization.Away x S] → S → R × ℕ
-- Mathlib.GroupTheory.CommutingProbability
commProb_function : ∀ {α : Type u_2} {β : Type u_3} [inst : Fintype α] [inst_1 : Mul β], commProb (α → β) = commProb β ^ Fintype.card α
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.instAbelianSheafAffineEtaleTopology : {S : AlgebraicGeometry.Scheme} →
  {A : Type u'} →
    [inst : CategoryTheory.Category.{u, u'} A] →
      {FA : A → A → Type u_1} →
        {CD : A → Type u} →
          [inst_1 : (X Y : A) → FunLike (FA X Y) (CD X) (CD Y)] →
            [inst_2 : CategoryTheory.ConcreteCategory A FA] →
              [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)] →
                [CategoryTheory.Limits.HasColimits A] →
                  [CategoryTheory.Limits.HasLimits A] →
                    [(CategoryTheory.forget A).ReflectsIsomorphisms] →
                      [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{u, u, u, u, u', u + 1}
                            (CategoryTheory.forget A)] →
                        [CategoryTheory.Abelian A] →
                          CategoryTheory.Abelian
                            (CategoryTheory.Sheaf (AlgebraicGeometry.Scheme.AffineEtale.topology S) A)
-- Mathlib.Topology.Algebra.Monoid
Filter.HasBasis.add_self : ∀ {ι : Type u_1} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddZeroClass M] [ContinuousAdd M] {p : ι → Prop}
  {s : ι → Set M}, (nhds 0).HasBasis p s → (nhds 0).HasBasis p fun i => s i + s i
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.comp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {E : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} E] →
                [inst_5 : CategoryTheory.MonoidalCategory E] →
                  (F : CategoryTheory.Functor C D) →
                    (G : CategoryTheory.Functor D E) → [F.OplaxMonoidal] → [G.OplaxMonoidal] → (F.comp G).OplaxMonoidal
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Param.fvarId : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Param pu → Lean.FVarId
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.opNNNorm_pi : ∀ {𝕜 : Type u} {E : Type wE} {ι : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : Fintype ι] {ι' : Type u_1} [inst_4 : Fintype ι'] {F : ι' → Type u_2}
  [inst_5 : (i' : ι') → SeminormedAddCommGroup (F i')] [inst_6 : (i' : ι') → NormedSpace 𝕜 (F i')]
  (f : (i' : ι') → E [⋀^ι]→L[𝕜] F i'), ‖ContinuousAlternatingMap.pi f‖₊ = ‖f‖₊
-- Mathlib.Probability.Moments.Basic
/-- Central moments are equal for almost-everywhere equal random variables.  -/
ProbabilityTheory.centralMoment_congr_ae : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {p : ℕ} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ},
  X =ᵐ[μ] Y → ProbabilityTheory.centralMoment X p μ = ProbabilityTheory.centralMoment Y p μ
-- Mathlib.RingTheory.DedekindDomain.Dvr
/-- A Dedekind domain is an integral domain that is Noetherian, and the
localization at every nonzero prime is a discrete valuation ring.

This is equivalent to `IsDedekindDomain`.
 -/
IsDedekindDomainDvr : (A : Type u_1) → [inst : CommRing A] → [IsDomain A] → Prop
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.FoldingRangeKind.region : Lean.Lsp.FoldingRangeKind
-- Mathlib.Algebra.Homology.DifferentialObject
HomologicalComplex.homologicalComplexToDGO_obj_obj : ∀ {β : Type u_1} [inst : AddCommGroup β] (b : β) (V : Type u_2) [inst_1 : CategoryTheory.Category.{v_1, u_2} V]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] (X : HomologicalComplex V (ComplexShape.up' b)) (i : β),
  ((HomologicalComplex.homologicalComplexToDGO b V).obj X).obj i = X.X i
-- Mathlib.Dynamics.PeriodicPts.Defs
AddAction.zsmul_mod_period_vadd : ∀ {α : Type v} {G : Type u} [inst : AddGroup G] [inst_1 : AddAction G α] (j : ℤ) {g : G} {a : α},
  (j % ↑(AddAction.period g a)) • g +ᵥ a = j • g +ᵥ a
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.Presieve.SecondObj.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C}
  (R : CategoryTheory.Presieve X) [inst_1 : R.HasPairwisePullbacks],
  CategoryTheory.Equalizer.Presieve.SecondObj P R =
    ∏ᶜ fun fg => P.obj (Opposite.op (CategoryTheory.Limits.pullback ↑fg.1.snd ↑fg.2.snd))
-- Mathlib.Algebra.Homology.QuasiIso
HomologicalComplex.quasiIsoAt_map_iff_of_preservesHomology : ∀ {ι : Type u_1} {c : ComplexShape ι} {C₁ : Type u_2} {C₂ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_2} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C₂] [inst_2 : CategoryTheory.Preadditive C₁]
  [inst_3 : CategoryTheory.Preadditive C₂] {K L : HomologicalComplex C₁ c} (φ : K ⟶ L)
  (F : CategoryTheory.Functor C₁ C₂) [inst_4 : F.Additive] [F.PreservesHomology] (i : ι) [inst_6 : K.HasHomology i]
  [inst_7 : L.HasHomology i] [inst_8 : ((F.mapHomologicalComplex c).obj K).HasHomology i]
  [inst_9 : ((F.mapHomologicalComplex c).obj L).HasHomology i] [F.ReflectsIsomorphisms],
  QuasiIsoAt ((F.mapHomologicalComplex c).map φ) i ↔ QuasiIsoAt φ i
-- Init.Data.UInt.Bitwise
UInt8.and_not_self : ∀ {a : UInt8}, a &&& ~~~a = 0
-- Mathlib.RingTheory.Valuation.RankOne
/-- The inclusion morphism from `Γ₀` to `ℝ≥0`.  -/
Valuation.RankLeOne.hom' : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    {inst : Ring R} →
      {inst_1 : LinearOrderedCommGroupWithZero Γ₀} →
        (v : Valuation R Γ₀) → [self : v.RankLeOne] → (MonoidWithZeroHom.ofClass v).ValueGroup₀ →*₀ NNReal
-- Aesop.Stats.File
Aesop.instToJsonStatsFileRecord.toJson : Aesop.StatsFileRecord → Lean.Json
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- Rotation by π is negation.  -/
Orientation.rotation_pi_apply : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x : V), (o.rotation ↑Real.pi) x = -x
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.δ_comp_δ_self'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.CosimplicialObject C) {n : ℕ}
  {i : Fin (n + 2)} {j : Fin (n + 3)},
  j = i.castSucc →
    ∀ {Z : C} (h : X.obj { len := n + 1 + 1 } ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.δ i) (CategoryTheory.CategoryStruct.comp (X.δ j) h) =
        CategoryTheory.CategoryStruct.comp (X.δ i) (CategoryTheory.CategoryStruct.comp (X.δ i.succ) h)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.uniqueHomFromTrivial.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Mon C),
  A.uniqueHomFromTrivial = { default := { hom := CategoryTheory.MonObj.one, isMonHom_hom := ⋯ }, uniq := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.diag_eq_zero : ∀ {α : Type u_1} {V : Type u_2} {A : Matrix V V α} [inst : Zero α] [inst_1 : One α], A.IsAdjMatrix → A.diag = 0
-- Init.Data.Array.Lemmas
Array.mem_flatMap_of_mem : ∀ {β : Type u_1} {α : Type u_2} {b : β} {xs : Array α} {f : α → Array β} {a : α},
  a ∈ xs → b ∈ f a → b ∈ Array.flatMap f xs
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.denote_toPoly : ∀ (ctx : Nat.Internal.Linear.Context) (e : Nat.Internal.Linear.Expr),
  Nat.Internal.Linear.Poly.denote ctx e.toPoly = Nat.Internal.Linear.Expr.denote ctx e
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.update_eq_single_add_erase : ∀ {ι : Type u} [inst : DecidableEq ι] {β : ι → Type u_1} [inst_1 : (i : ι) → AddZeroClass (β i)] (f : Π₀ (i : ι), β i)
  (i : ι) (b : β i), f.update i b = (fun₀ | i => b) + DFinsupp.erase i f
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.mk_div : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Div G] [inst_2 : ContinuousDiv G] (x y : G),
  SeparationQuotient.mk (x / y) = SeparationQuotient.mk x / SeparationQuotient.mk y
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
/-- When the index type `ι` contains a unique element, the category
`DescentDataAsCoalgebra` identifies to the category of coalgebras
over the comonad corresponding to the adjunction
`(F.map f.op.toLoc).adj`.  -/
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.coalgebraEquivalence : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F :
        CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
          (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)) →
      (ι : Type u_1) →
        [Unique ι] →
          {X S : C} →
            (f : X ⟶ S) →
              (F.DescentDataAsCoalgebra fun x => f) ≌
                (CategoryTheory.Adjunction.ofCat (F.map f.op.toLoc).adj).toComonad.Coalgebra
-- Mathlib.NumberTheory.LSeries.Linearity
LSeries_smul : ∀ (f : ℕ → ℂ) (c s : ℂ), LSeries (c • f) s = c * LSeries f s
-- Mathlib.Analysis.Calculus.BumpFunction.Normed
ContDiffBump.hasCompactSupport_normed : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  [inst_3 : MeasurableSpace E] {c : E} (f : ContDiffBump c) {μ : MeasureTheory.Measure E} [BorelSpace E]
  [FiniteDimensional ℝ E] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure], HasCompactSupport (f.normed μ)
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.isoWhiskerRight_trans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {G H K : CategoryTheory.Functor C D} (α : G ≅ H)
  (β : H ≅ K) (F : CategoryTheory.Functor D E),
  CategoryTheory.Functor.isoWhiskerRight (α ≪≫ β) F =
    CategoryTheory.Functor.isoWhiskerRight α F ≪≫ CategoryTheory.Functor.isoWhiskerRight β F
-- Mathlib.Logic.Equiv.Nat
/-- An equivalence between `Bool × ℕ` and `ℕ`, by mapping `(true, x)` to `2 * x + 1` and
`(false, x)` to `2 * x`.  -/
Equiv.boolProdNatEquivNat : Bool × ℕ ≃ ℕ
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.symm_dual_id : ∀ {α : Type u_2} [inst : CompleteLattice α],
  CompleteLatticeHom.dual.symm (CompleteLatticeHom.id αᵒᵈ) = CompleteLatticeHom.id α
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.restrictTotalDegree_le_restrictDegree : ∀ (σ : Type u) (R : Type v) [inst : CommSemiring R] (m : ℕ),
  MvPolynomial.restrictTotalDegree σ R m ≤ MvPolynomial.restrictDegree σ R m
-- Mathlib.Analysis.Normed.Group.Pointwise
ball_one_div_singleton : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x : E), Metric.ball 1 δ / {x} = Metric.ball x⁻¹ δ
-- Init.Data.Fin.Lemmas
Fin.add_one_le_iff : ∀ {n : ℕ} {k : Fin (n + 1)}, k + 1 ≤ k ↔ k = Fin.last n
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.yn_one : ∀ {a : ℕ} (a1 : 1 < a), Pell.yn a1 1 = 1
-- Mathlib.Order.Hom.CompleteLattice
/-- The type of complete lattice homomorphisms from `α` to `β`.  -/
CompleteLatticeHom : (α : Type u_8) → (β : Type u_9) → [CompleteLattice α] → [CompleteLattice β] → Type (max u_8 u_9)
-- Mathlib.Algebra.Ring.BooleanRing
ofBoolAlg_mul_ofBoolAlg_eq_left_iff : ∀ {α : Type u_1} [inst : BooleanRing α] {a b : AsBoolAlg α}, ofBoolAlg a * ofBoolAlg b = ofBoolAlg a ↔ a ≤ b
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.mapPreimage_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.GrothendieckTopology C}
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G]
  (F : CategoryTheory.Sheaf J A) {X Y Z : C} (f : G.obj X ⟶ G.obj Y) (g : G.obj Y ⟶ G.obj Z),
  CategoryTheory.Functor.IsDenseSubsite.mapPreimage K G F (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsDenseSubsite.mapPreimage K G F g)
      (CategoryTheory.Functor.IsDenseSubsite.mapPreimage K G F f)
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.eval₂Hom_eq_bind₂ : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (f : R →+* MvPolynomial σ S), MvPolynomial.eval₂Hom f MvPolynomial.X = MvPolynomial.bind₂ f
-- Init.GrindInstances.Ring.UInt
/-- Variant of `UInt64.ofNat_mod_size` replacing `2 ^ 64` with `18446744073709551616`. -/
UInt64.ofNat_mod_size' : ∀ {x : ℕ}, UInt64.ofNat (x % 18446744073709551616) = UInt64.ofNat x
-- Mathlib.Analysis.Normed.Group.Basic
dist_sum_sum_le_of_le : ∀ {ι : Type u_3} {E : Type u_5} [inst : SeminormedAddCommGroup E] (s : Finset ι) {f a : ι → E} {d : ι → ℝ},
  (∀ b ∈ s, dist (f b) (a b) ≤ d b) → dist (∑ b ∈ s, f b) (∑ b ∈ s, a b) ≤ ∑ b ∈ s, d b
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_ofNat_add : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] [inst_1 : AddCommMonoidWithOne G]
  [inst_2 : AddMonoidWithOne H] [AddConstMapClass F G H 1 1] (f : F) (n : ℕ) [inst_4 : n.AtLeastTwo] (x : G),
  f (OfNat.ofNat n + x) = f x + OfNat.ofNat n
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- For an open embedding `f : U ⟶ X` and a point `x : U`, we get an isomorphism between the stalk
of `X` at `f x` and the stalk of the restriction of `X` along `f` at `x`.  -/
AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso : {U : TopCat} →
  (X : AlgebraicGeometry.LocallyRingedSpace) →
    {f : U ⟶ X.toTopCat} →
      (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) →
        (x : ↑U) → (X.restrict h).presheaf.stalk x ≅ X.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom f) x)
-- Lean.Parser.Term
Lean.Parser.Term.depArrow.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.Bialgebra.Basic
/-- `comulAlgHom R A` is the comultiplication of the `R`-bialgebra `A`, as an `R`-algebra map.  -/
Bialgebra.comulAlgHom : (R : Type u) →
  (A : Type v) →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Bialgebra R A] → A →ₐ[R] TensorProduct R A A
-- Mathlib.Combinatorics.Quiver.Schreier
Quiver.SchreierGraph.ofVertex.inj : ∀ {V : Type u_1} {M : Type u_2} {inst : SMul M V} {S : Type u_3} {_ι : S → M} {toVertex toVertex_1 : V},
  { toVertex := toVertex } = { toVertex := toVertex_1 } → toVertex = toVertex_1