mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Definability
_private.Mathlib.ModelTheory.Definability.0.Set.DefinableFun.comp.match_1_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (i : α) (h_1 : Unit → motive none) (h_2 : (i : α) → motive (some i)),
  (match some i with
    | none => h_1 ()
    | some i => h_2 i) =
    h_2 i
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.modifier : Lean.Lsp.SemanticTokenType
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.parentD_findAux_lt : ∀ {i : ℕ} {self : Batteries.UnionFind} {x : Fin self.size},
  i < self.size → Batteries.UnionFind.parentD (self.findAux x).s i < self.size
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.image2_sdiv : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] {s t : Set β}, Set.image2 (fun x1 x2 => x1 /ₛ x2) s t = s /ₛ t
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.expandFinValuePattern : Lean.Meta.Match.Problem → Lean.MetaM Lean.Meta.Match.Problem
-- Mathlib.Algebra.Order.Floor.Extended
ENat.preimage_toENNReal_Ico : ∀ (a b : ENNReal), ENat.toENNReal ⁻¹' Set.Ico a b = Set.Ico ⌈a⌉ₑ ⌈b⌉ₑ
-- Aesop.Script.SpecificTactics
_private.Aesop.Script.SpecificTactics.0.Aesop.renameInaccessibleFVarsS' : Array Lean.MVarId → Aesop.ScriptM (Array Lean.MVarId)
-- Mathlib.Analysis.LocallyConvex.AbsConvex
balanced_absConvexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] {s : Set E}, Balanced 𝕜 ((absConvexHull 𝕜) s)
-- Mathlib.Algebra.Order.Monoid.NatCast
/-- **Alias** of `zero_lt_three`.

---

See `zero_lt_three'` for a version with the type explicit.  -/
three_pos : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [ZeroLEOneClass α] [NeZero 1] [AddLeftMono α],
  0 < 3
-- Mathlib.GroupTheory.OrderOfElement
/-- `IsOfFinOrder` is a predicate on an element `x` of a monoid to be of finite order, i.e. there
exists `n ≥ 1` such that `x ^ n = 1`.  -/
IsOfFinOrder : {G : Type u_1} → [Monoid G] → G → Prop
-- Mathlib.GroupTheory.CommutingProbability
commProb_def : ∀ (M : Type u_1) [inst : Mul M], commProb M = ↑(Nat.card { p // Commute p.1 p.2 }) / ↑(Nat.card M) ^ 2
-- Mathlib.Order.Interval.Set.SuccPred
Set.insert_Ico_right_eq_Ico_succ : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α} [NoMaxOrder α],
  a ≤ b → insert b (Set.Ico a b) = Set.Ico a (Order.succ b)
-- Mathlib.Order.Interval.Set.Pi
Set.image_mulSingle_uIcc_right : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Lattice (α i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → One (α i)] (i : ι) (b : α i), Pi.mulSingle i '' Set.uIcc 1 b = Set.uIcc 1 (Pi.mulSingle i b)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- If `G` is an additive group object, then `Hom(-, G)` is a presheaf of additive groups.  -/
CategoryTheory.yonedaAddGrpObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (G : C) → [CategoryTheory.AddGrpObj G] → CategoryTheory.Functor Cᵒᵖ AddGrpCat
-- Mathlib.Topology.Gluing
TopCat.GlueData.f_open : ∀ (self : TopCat.GlueData) (i j : self.J), Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (self.f i j))
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
/-- Given a free groupoid and an arborescence of its generating quiver, the vertex
group at the root is freely generated by loops coming from generating arrows
in the complement of the tree.  -/
IsFreeGroupoid.SpanningTree.endIsFree : ∀ {G : Type u} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G]
  (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G)))
  [inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)],
  IsFreeGroup (CategoryTheory.End (IsFreeGroupoid.SpanningTree.root'✝ T))
-- Lean.CoreM
Lean.DeclNameGenerator.mkChild : Lean.DeclNameGenerator → Lean.DeclNameGenerator × Lean.DeclNameGenerator
-- Mathlib.Analysis.Analytic.Basic
/-- If a function admits a power series expansion within a set at `x`, then it is the uniform limit
of the partial sums of this power series on strict subdisks of the disk of convergence, i.e., `f y`
is the uniform limit of `p.partialSum n (y - x)` there.  -/
HasFPowerSeriesWithinOnBall.tendstoUniformlyOn' : ∀ {𝕜 : 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] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} {r' : NNReal},
  HasFPowerSeriesWithinOnBall f p s x r →
    ↑r' < r → TendstoUniformlyOn (fun n y => p.partialSum n (y - x)) f Filter.atTop (insert x s ∩ Metric.ball x ↑r')
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
HasMFDerivWithinAt.continuousWithinAt : ∀ {𝕜 : 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'} {x : M} {s : Set M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)}, HasMFDerivAt[s] f x f' → ContinuousWithinAt f s x
-- Std.Internal.Parsec.ByteArray
/-- Run a `Parser` on a `ByteArray`, returns either the result or an error string with offset.
 -/
Std.Internal.Parsec.ByteArray.Parser.run : {α : Type} → Std.Internal.Parsec.ByteArray.Parser α → ByteArray → Except String α
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} {N₁ N₂ : M.Submodule}, (∀ (X : Cᵒᵖ), N₁.obj X = N₂.obj X) → N₁ = N₂
-- Mathlib.Data.Finsupp.PointwiseSMul
/-- **Alias** of `Finset.VAddAntidiagonal`. -/
Finsupp.vaddAntidiagonal : {G : Type u_1} →
  {P : Type u_2} →
    [inst : VAdd G P] → {s : Set G} → {t : Set P} → (a : P) → (s.vaddAntidiagonal t a).Finite → Finset (G × P)
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (f : BoundedOrderHom α β), (BoundedOrderHom.id β).comp f = f
-- Init.Data.List.Find
List.findFinIdx?_cons : ∀ {α : Type u_1} {p : α → Bool} {x : α} {xs : List α},
  List.findFinIdx? p (x :: xs) = if p x = true then some 0 else Option.map Fin.succ (List.findFinIdx? p xs)
-- Lean.DocString.Types
Lean.Doc.Block.para.inj : ∀ {i : Type u} {b : Type v} {contents contents_1 : Array (Lean.Doc.Inline i)},
  Lean.Doc.Block.para contents = Lean.Doc.Block.para contents_1 → contents = contents_1
-- Mathlib.Order.Interval.Finset.Gaps
Finset.intervalGapsWithin.snd.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] (F : Finset (α × α)) {k : ℕ} (h : F.card = k) (b : α) (i : Fin (k + 1)),
  Finset.intervalGapsWithin.snd F h b i = if hi : i = Fin.last k then b else ((F.orderEmbOfFin h) (i.castPred hi)).1
-- Init.Data.UInt.BasicAux
/-- Converts a natural number to `USize`, returning the largest representable value if the number is too
large.

Returns `USize.size - 1`, which is  `2^64 - 1` or `2^32 - 1` depending on the platform, for natural
numbers greater than or equal to `USize.size`.
 -/
USize.ofNatTruncate : ℕ → USize
-- Mathlib.Topology.Separation.Basic
/-- **Alias** of the reverse direction of `continuousWithinAt_insert`. -/
ContinuousWithinAt.insert' : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T1Space X] {x y : X}
  {s : Set X} {f : X → Y}, ContinuousWithinAt f s x → ContinuousWithinAt f (insert y s) x
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.IsMonotone.mk : ∀ {α : Type u_1} {β : Type u_2} {cmpα : α → α → Ordering} {cmpβ : β → β → Ordering} {f : α → β},
  (∀ {x y : α}, RBTree.RBNode.cmpLT cmpα x y → RBTree.RBNode.cmpLT cmpβ (f x) (f y)) →
    RBTree.RBNode.IsMonotone cmpα cmpβ f
-- Init.Data.Option.Monadic
Option.mapM_guard : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Applicative m] {x : α} {p : α → Bool} {f : α → m β},
  Option.mapM f (Option.guard p x) = if p x = true then some <$> f x else pure none
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
NonUnitalSubalgebra.le_topologicalClosure : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : TopologicalSpace A] [inst_2 : NonUnitalSemiring A]
  [inst_3 : Module R A] [inst_4 : ContinuousConstSMul R A] [inst_5 : IsSemitopologicalSemiring A]
  (s : NonUnitalSubalgebra R A), s ≤ s.topologicalClosure
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ (f : ↑(X.presheaf.obj (Opposite.op U))), IsLocalization.Away f ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))
-- Mathlib.RingTheory.Ideal.Quotient.Operations
AlgHom.liftOfSurjective.congr_simp : ∀ {R : Type u_5} {A : Type u_6} {B : Type u_7} {C : Type u_8} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : CommRing B] [inst_3 : CommRing C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  (f f_1 : A →ₐ[R] B) (e_f : f = f_1) (hf : Function.Surjective ⇑f) (g g_1 : A →ₐ[R] C) (e_g : g = g_1)
  (H : RingHom.ker f.toRingHom ≤ RingHom.ker g.toRingHom), f.liftOfSurjective hf g H = f_1.liftOfSurjective ⋯ g_1 ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKeyD_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k fallback : α},
  (List.map Prod.fst l).contains k = false → (Std.DTreeMap.Raw.Const.ofList l cmp).getKeyD k fallback = fallback
-- Mathlib.Topology.Algebra.Group.Basic
ContinuousWithinAt.fun_zsmul : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G]
  [inst_3 : TopologicalSpace α] {f : α → G} {x : α} {s : Set α},
  ContinuousWithinAt f s x → ∀ (z : ℤ), ContinuousWithinAt (fun i => z • f i) s x
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.mul_mem_smul_finset_iff : ∀ {α : Type u_2} [inst : Group α] [inst_1 : DecidableEq α] (a : α) {b : α} {s : Finset α}, a * b ∈ a • s ↔ b ∈ s
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsFoelner.tendsto_nhds_mean : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : Group G]
  [inst_2 : MulAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X},
  IsFoelner G μ (↑u) F →
    ∀ (s : Set X), Filter.Tendsto (fun i => μ (s ∩ F i) / μ (F i)) (↑u) (nhds (IsFoelner.mean μ u F s))
-- Mathlib.Algebra.Lie.BaseChange
LieAlgebra.RestrictScalars.lieAlgebra : (R : Type u_1) →
  (A : Type u_2) →
    (L : Type u_3) →
      [h : LieRing L] →
        [inst : CommRing A] →
          [LieAlgebra A L] → [inst_2 : CommRing R] → [Algebra R A] → LieAlgebra R (RestrictScalars R A L)
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.lift_unique' : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] (F : MonoidAlgebra R M →ₐ[R] A), F = (MonoidAlgebra.lift R A M) ((↑F).comp (MonoidAlgebra.of R M))
-- Mathlib.Algebra.Lie.Quotient
LieSubmodule.Quotient.map_mk'_eq_bot_le : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N N' : LieSubmodule R L M) [inst_5 : LieAlgebra R L]
  [inst_6 : LieModule R L M], LieSubmodule.map (LieSubmodule.Quotient.mk' N) N' = ⊥ ↔ N' ≤ N
-- Init.Omega.Constraint
/-- The impossible constraint, unsatisfiable.  -/
Lean.Omega.Constraint.impossible : Lean.Omega.Constraint
-- Std.Internal.Do.WP.Basic
/-- `Except ε`'s `WP` interpretation: `Prop` assertions and a single exception postcondition.  -/
Std.Internal.Do.Except.wpInst : {ε : Type u_1} → {α : Type u} → Std.Internal.Do.WP (Except ε α) α Prop EPost⟨ε → Prop⟩
-- Mathlib.Data.SProd
/-- Notation type class for the set product `×ˢ`.  -/
SProd : Type u → Type v → outParam (Type w) → Type (max (max u v) w)
-- Mathlib.Analysis.RCLike.Basic
RCLike.re_eq_self_of_le : ∀ {K : Type u_1} [inst : RCLike K] {a : K}, ‖a‖ ≤ RCLike.re a → ↑(RCLike.re a) = a
-- Batteries.Data.Array.Scan
Array.scanr_ne_empty : ∀ {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → β} {as : Array α}, Array.scanr f init as ≠ #[]
-- Mathlib.Logic.OpClass
isSymmOp_of_isCommutative : ∀ (α : Sort u) (op : α → α → α) [Std.Commutative op], IsSymmOp op
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- The map `Dⱼᵢ⁻¹ U ⟶ Dᵢ` from the restricted diagram to the original diagram.  -/
AlgebraicGeometry.opensDiagramι : {I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme) →
      (i : I) → (U : (D.obj i).Opens) → AlgebraicGeometry.opensDiagram D i U ⟶ (CategoryTheory.Over.forget i).comp D
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffOn.image_comp_contDiff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E} {g : F → G} {f : E → F},
  ContDiffOn 𝕜 n g (f '' s) → ContDiff 𝕜 n f → ContDiffOn 𝕜 n (g ∘ f) s
-- Mathlib.LinearAlgebra.Quotient.Defs
/-- Two `LinearMap`s from a quotient module are equal if their compositions with
`submodule.mkQ` are equal.

See note [partially-applied ext lemmas].  -/
Submodule.linearMap_qext : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {R₂ : Type u_3} {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  ⦃f g : M ⧸ p →ₛₗ[τ₁₂] M₂⦄, f ∘ₛₗ p.mkQ = g ∘ₛₗ p.mkQ → f = g
-- Mathlib.Order.Hom.WithTopBot
SupHom.withTop_toFun : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] (f : SupHom α β) (a : WithTop α),
  f.withTop a = WithTop.map (⇑f) a
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.one : {R : Type u} → [inst : Ring R] → (I : Ideal R) → One (R ⧸ I)
-- Mathlib.Data.Multiset.MapFold
Multiset.zero_eq_map : ∀ {α : Type u_1} {β : Type v} {s : Multiset α} {f : α → β}, 0 = Multiset.map f s ↔ s = 0
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
/-- The characteristic function of a convolution of measures
is the product of the respective characteristic functions.  -/
MeasureTheory.charFunDual_conv : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {mE : MeasurableSpace E} [BorelSpace E]
  [SecondCountableTopology E] {μ ν : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν] (L : StrongDual ℝ E),
  MeasureTheory.charFunDual (μ.conv ν) L = MeasureTheory.charFunDual μ L * MeasureTheory.charFunDual ν L
-- Mathlib.Analysis.Normed.Group.Continuity
Filter.Tendsto.norm : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedAddGroup E] {a : E} {l : Filter α} {f : α → E},
  Filter.Tendsto f l (nhds a) → Filter.Tendsto (fun x => ‖f x‖) l (nhds ‖a‖)
-- Init.MethodSpecsSimp
OrOp.or_hOr : ∀ {α : Type u_1} [inst : OrOp α], OrOp.or = HOr.hOr
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxRightLinear.μᵣ_naturality_right : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'} [self : F.LaxRightLinear C] (d : D) {c c' : C}
  (f : c ⟶ c'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight (F.obj d) f)
      (CategoryTheory.Functor.LaxRightLinear.μᵣ F d c') =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxRightLinear.μᵣ F d c)
      (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f))
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.copy_eq : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (f : α → β) (hf : ↑e = f) (g : β → α) (hg : ↑e.symm = g)
  (s : Set α) (hs : e.source = s) (t : Set β) (ht : e.target = t), e.copy f hf g hg s hs t ht = e
-- Mathlib.RingTheory.DedekindDomain.SelmerGroup
/-- The multiplicative `v`-adic valuation on `Kˣ` modulo `n`-th powers.  -/
IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroMod : {R : Type u} →
  [inst : CommRing R] →
    [IsDedekindDomain R] →
      {K : Type v} →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [IsFractionRing R K] →
              IsDedekindDomain.HeightOneSpectrum R → (n : ℕ) → Kˣ ⧸ (powMonoidHom n).range →* Multiplicative (ZMod n)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.card_neighborSet_eq_degree : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)],
  Fintype.card ↑(G.neighborSet v) = G.degree v
-- Mathlib.RingTheory.LocalRing.Length
/-- If `B/A` is an extension of local rings, and if `M` is a `B`-module, then
`ℓ_A(M) = ℓ_B(M) * [κ(B) : κ(A)]`.  -/
IsLocalRing.length_restrictScalars : ∀ (A : Type u_1) (B : Type u_2) (M : Type u_3) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : IsLocalRing A]
  [inst_3 : IsLocalRing B] [inst_4 : Algebra A B] [inst_5 : IsLocalHom (algebraMap A B)] [inst_6 : AddCommGroup M]
  [inst_7 : Module A M] [inst_8 : Module B M] [IsScalarTower A B M],
  Module.length A M = Module.length B M * Module.length (IsLocalRing.ResidueField A) (IsLocalRing.ResidueField B)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.auxbound1 : ∀ (z : UpperHalfPlane) {c : ℝ} (d : ℝ), 1 ≤ c ^ 2 → EisensteinSeries.r z ≤ ‖↑c * ↑z + ↑d‖
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.term.injEq : ∀ (i i_1 : Lean.Term), (Aesop.Frontend.Feature.term i = Aesop.Frontend.Feature.term i_1) = (i = i_1)
-- Mathlib.Order.Heyting.Hom
BoundedLatticeHomClass.toBiheytingHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : BooleanAlgebra α]
  [inst_2 : BooleanAlgebra β] [BoundedLatticeHomClass F α β], BiheytingHomClass F α β
-- Mathlib.CategoryTheory.Enriched.Opposite
/-- The functor going from the opposite of the underlying category of the enriched category `C`
to the underlying category of the enriched category `Cᵒᵖ`.  -/
CategoryTheory.forgetEnrichmentOppositeEquivalence.inverse : (V : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      [inst_2 : CategoryTheory.BraidedCategory V] →
        (C : Type u) →
          [inst_3 : CategoryTheory.EnrichedCategory V C] →
            CategoryTheory.Functor (CategoryTheory.ForgetEnrichment V C)ᵒᵖ (CategoryTheory.ForgetEnrichment V Cᵒᵖ)
-- Init.Data.Repr
instReprAtomUSize : ReprAtom USize
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSet_precomp_of_bijective : ∀ {Ω : Type u_1} {ι : Type u_2} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : ι → Set Ω} {ι' : Type u_6}
  {g : ι' → ι}, Function.Bijective g → (ProbabilityTheory.iIndepSet (s ∘ g) μ ↔ ProbabilityTheory.iIndepSet s μ)
-- Mathlib.Topology.Algebra.Monoid
Filter.Tendsto.nsmul : ∀ {α : Type u_2} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [ContinuousAdd M] {l : Filter α}
  {f : α → M} {x : M}, Filter.Tendsto f l (nhds x) → ∀ (n : ℕ), Filter.Tendsto (fun x => n • f x) l (nhds (n • x))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.insertIfNew k v).minKey? = some (t.minKey?.elim k fun k' => if cmp k k' = Ordering.lt then k else k')
-- Mathlib.Algebra.BigOperators.Expect
/-- Reorder an average.

The difference with `Finset.expect_bij` is that the bijection is specified with an inverse, rather
than as a surjective injection.

The difference with `Finset.expect_nbij'` is that the bijection and its inverse are allowed to use
membership of the domains of the averages, rather than being non-dependent functions.  -/
Finset.expect_bij' : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] {s : Finset ι}
  {f : ι → M} {t : Finset κ} {g : κ → M} (i : (a : ι) → a ∈ s → κ) (j : (a : κ) → a ∈ t → ι)
  (hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t) (hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s),
  (∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a) →
    (∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a) →
      (∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)) → (s.expect fun i => f i) = t.expect fun i => g i
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.aleph_add_aleph : ∀ (o₁ o₂ : Ordinal.{u_1}), Cardinal.aleph o₁ + Cardinal.aleph o₂ = Cardinal.aleph (max o₁ o₂)
-- Mathlib.GroupTheory.Exponent
/-- **Alias** of the reverse direction of `Monoid.exponent_ne_zero`. -/
Monoid.ExponentExists.exponent_ne_zero : ∀ {G : Type u} [inst : Monoid G], Monoid.ExponentExists G → Monoid.exponent G ≠ 0
-- Mathlib.Data.Fintype.BigOperators
/-- This lemma is specifically designed to be used backwards, whence the specialisation to `Fin n`
as the indexing type doesn't matter in practice. The more general forward direction lemma here is
`Fintype.card_piFinset`.  -/
Fintype.card_piFinset_const : ∀ {α : Type u_7} (s : Finset α) (n : ℕ), (Fintype.piFinset fun x => s).card = s.card ^ n
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.instMonoid : {d : ℤ} → Monoid (ℤ√d)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.arrowCongr_symm : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₁' : Type uA₁'} {A₂' : Type uA₂'} [inst : CommSemiring R]
  [inst_1 : Semiring A₁] [inst_2 : Semiring A₂] [inst_3 : Semiring A₁'] [inst_4 : Semiring A₂'] [inst_5 : Algebra R A₁]
  [inst_6 : Algebra R A₂] [inst_7 : Algebra R A₁'] [inst_8 : Algebra R A₂'] (e₁ : A₁ ≃ₐ[R] A₁') (e₂ : A₂ ≃ₐ[R] A₂'),
  (e₁.arrowCongr e₂).symm = e₁.symm.arrowCongr e₂.symm
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPullback_arrows : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} (R : CategoryTheory.Sieve (F.obj X)),
  (CategoryTheory.Sieve.functorPullback F R).arrows = CategoryTheory.Presieve.functorPullback F R.arrows
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- When the first map `S.f` is zero, this is the homology data on `S` given
by the chosen `kernel S.g`  -/
CategoryTheory.ShortComplex.HomologyData.ofHasKernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → S.f = 0 → [CategoryTheory.Limits.HasKernel S.g] → S.HomologyData