mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Attributes
Lean.getBuiltinAttributeImpl : Lean.Name → IO Lean.AttributeImpl
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
WeierstrassCurve.ofJ_1728_of_three_eq_zero : ∀ {F : Type u_2} [inst : Field F] [inst_1 : DecidableEq F],
  3 = 0 → WeierstrassCurve.ofJ 1728 = WeierstrassCurve.ofJ1728 F
-- Mathlib.Topology.Category.Profinite.EffectiveEpi
Profinite.instPreregular : CategoryTheory.Preregular Profinite
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.exists_mem_carrier_add_eq_zero : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (x y : ConjRootClass K L),
  (∃ a ∈ x.carrier, ∃ b ∈ y.carrier, a + b = 0) ↔ x = -y
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
/-- If `f : X ⟶ Y` and `g : Y ⟶ Z` are composable morphisms,
then the kernel of `φ f g : X ⊞ Y ⟶ Y ⊞ Z` identifies
to `kernel (f ≫ g)`.  -/
CategoryTheory.kernelCokernelCompSequence.isLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y Z : C} →
        (f : X ⟶ Y) →
          (g : Y ⟶ Z) →
            CategoryTheory.Limits.IsLimit
              (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.kernelCokernelCompSequence.ι f g) ⋯)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instInfSet : {R : Type u} → {M : Type v} → [inst : VAdd R M] → InfSet (SubAddAction R M)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.coeff_preΨ₄_ne_zero : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), 2 ≠ 0 → W.preΨ₄.coeff 6 ≠ 0
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The L-series of the von Mangoldt function `Λ` equals the negative logarithmic derivative
of the Riemann zeta function on its domain of convergence `re s > 1`.  -/
ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div : ∀ {s : ℂ}, 1 < s.re → LSeries (fun n => ↑(ArithmeticFunction.vonMangoldt n)) s = -deriv riemannZeta s / riemannZeta s
-- Lean.Data.Lsp.Client
Lean.Lsp.Registration : Type
-- Mathlib.Geometry.Convex.Cone.Basic
/-- **Alias** of `ConvexCone.IsReproducing.span_eq_top`. -/
ConvexCone.isGenerating_iff_isReproducing : ∀ {R : Type u_7} {M : Type u_8} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {C : ConvexCone R M}, C.IsReproducing → Submodule.span R ↑C = ⊤
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_add_left : ∀ {a b c : ℤ}, a ∣ c → (a ∣ b + c ↔ a ∣ b)
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.I.symm_zero : (CategoryTheory.ConcreteCategory.hom TopCat.I.symm) 0 = 1
-- Mathlib.Topology.Ultrafilter
Ultrafilter.clusterPt_iff : ∀ {X : Type u} {x : X} [inst : TopologicalSpace X] {f : Ultrafilter X}, ClusterPt x ↑f ↔ ↑f ≤ nhds x
-- Batteries.Lean.Expr
/-- Auxiliary definition for `withApp'`.  -/
Lean.Expr.withApp'.go : {α : Sort u_1} → (Lean.Expr → Array Lean.Expr → α) → Lean.Expr → Array Lean.Expr → ℕ → α
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mem_mul : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α} {a : α}, a ∈ s * t ↔ ∃ x ∈ s, ∃ y ∈ t, x * y = a
-- Init.Data.List.ToArray
List.prod.eq_1 : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α], List.prod = List.foldr (fun x1 x2 => x1 * x2) 1
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.π.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  CategoryTheory.kernelCokernelCompSequence.π f g =
    CategoryTheory.Limits.biprod.desc
      (CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.cokernel.π (CategoryTheory.CategoryStruct.comp f g)))
      (CategoryTheory.Limits.cokernel.π (CategoryTheory.CategoryStruct.comp f g))
-- Mathlib.Data.Num.Bitwise
NzsNum.bit.inj : ∀ {a : Bool} {a_1 : NzsNum} {a_2 : Bool} {a_3 : NzsNum}, NzsNum.bit a a_1 = NzsNum.bit a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.instInhabited.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S],
  OreLocalization.instInhabited = { default := 1 }
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicAt.smul` -/
MeromorphicAt.fun_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_4} [inst_3 : NormedRing R] [inst_4 : Module R E] [IsBoundedSMul R E] {x : 𝕜}
  [inst_6 : NormedAlgebra 𝕜 R] [IsScalarTower 𝕜 R E] {f : 𝕜 → R} {g : 𝕜 → E},
  MeromorphicAt f x → MeromorphicAt g x → MeromorphicAt (fun i => f i • g i) x
-- Init.Data.List.Lemmas
List.intercalate.eq_1 : ∀ {α : Type u} (sep : List α) (xs : List (List α)), sep.intercalate xs = (List.intersperse sep xs).flatten
-- Mathlib.Order.Atoms
OrderDual.instIsAtomic : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderTop α] [IsCoatomic α], IsAtomic αᵒᵈ
-- Init.Data.Int.Basic
Int.instNatPow : NatPow ℤ
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ring.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr) (lhs : Lean.Meta.Grind.Arith.Linear.LinExpr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ring c lhs) = 1 + sizeOf c + sizeOf lhs
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.prod_Hom : ∀ (C : Type u₁) [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] (D : Type u₂)
  [inst_1 : CategoryTheory.CategoryStruct.{v₂, u₂} D] (X Y : C × D), (X ⟶ Y) = ((X.1 ⟶ Y.1) × (X.2 ⟶ Y.2))
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.eval.match_1.eq_2 : ∀ (motive : Lean.Data.AC.Expr → Sort u_1) (l r : Lean.Data.AC.Expr)
  (h_1 : (idx : ℕ) → motive (Lean.Data.AC.Expr.var idx)) (h_2 : (l r : Lean.Data.AC.Expr) → motive (l.op r)),
  (match l.op r with
    | Lean.Data.AC.Expr.var idx => h_1 idx
    | l.op r => h_2 l r) =
    h_2 l r
-- Batteries.Data.List.Matcher
/-- Knuth-Morris-Pratt matcher type

This type is used to keep data for running the Knuth-Morris-Pratt (KMP) list matching algorithm.
KMP is a linear time algorithm to locate all contiguous sublists of a list that match a given
pattern. Generating the algorithm data is also linear in the length of the pattern but the data can
be re-used to match the same pattern over multiple lists.

The KMP data for a pattern can be generated using `Matcher.ofList`. Then `Matcher.find?` and
`Matcher.findAll` can be used to run the algorithm on an input list.
```
def m := Matcher.ofList [0,1,1,0]

#eval Option.isSome <| m.find? [2,1,1,0,1,1,2] -- false
#eval Option.isSome <| m.find? [0,0,1,1,0,0] -- true

#eval Array.size <| m.findAll [0,1,1,0,1,1,0] -- 2
#eval Array.size <| m.findAll [0,1,1,0,1,1,0,1,1,0] -- 3
```
 -/
List.Matcher : Type u_1 → Type u_1
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.preservesZeroMorphisms_π₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C],
  CategoryTheory.ShortComplex.π₃.PreservesZeroMorphisms
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.zero_lt_getElem!_toList_roc_iff : ∀ {m n i : ℕ}, 0 < (m<...=n).toList[i]! ↔ i < n - m
-- Lean.Meta.Tactic.Cases
_private.Lean.Meta.Tactic.Cases.0.Lean.Meta.Cases.inductionCasesOn : Lean.MVarId →
  Lean.FVarId →
    Array Lean.Meta.AltVarNames →
      Lean.Meta.Cases.Context →
        optParam Bool false → optParam (Option (Array Lean.Name)) none → Lean.MetaM (Array Lean.Meta.CasesSubgoal)
-- Init.Data.List.MinMaxIdx
List.getElem_get_minIdxOn? : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β}
  {xs : List α} (h : (List.minIdxOn? f xs).isSome = true), xs[(List.minIdxOn? f xs).get h] = List.minOn f xs ⋯
-- Mathlib.RingTheory.DedekindDomain.Different
aeval_derivative_mem_differentIdeal : ∀ (A : Type u_1) (K : Type u_2) (L : Type u) {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [inst_11 : IsDomain A] [IsFractionRing A K]
  [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsIntegrallyClosed A]
  [inst_17 : IsDedekindDomain B] [inst_18 : Module.IsTorsionFree A B] (x : B),
  K[(algebraMap B L) x] = ⊤ → (Polynomial.aeval x) (Polynomial.derivative (minpoly A x)) ∈ differentIdeal A B
-- Mathlib.Topology.Connected.PathConnected
/-- The path component of `x` in a product space is the product of the path components of its
coordinates.  -/
pathComponent_pi : ∀ {ι : Type u_3} {Z : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (Z i)] (x : (i : ι) → Z i),
  pathComponent x = Set.univ.pi fun i => pathComponent (x i)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
/-- `F` is triangulated if and only if `F.op` is triangulated.
 -/
CategoryTheory.Functor.op_isTriangulated_iff : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Limits.HasZeroObject C] [inst_6 : CategoryTheory.Preadditive C]
  [inst_7 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_8 : CategoryTheory.Pretriangulated C]
  [inst_9 : CategoryTheory.Limits.HasZeroObject D] [inst_10 : CategoryTheory.Preadditive D]
  [inst_11 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_12 : CategoryTheory.Pretriangulated D],
  F.op.IsTriangulated ↔ F.IsTriangulated
-- Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
AddMonoidAlgebra.smul_apply_addAction : ∀ {G : Type u_1} {P : Type u_2} {R : Type u_3} {V : Type u_4} [inst : AddGroup G] [inst_1 : AddAction G P]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid V] [inst_4 : SMulWithZero R V] (f : AddMonoidAlgebra R G) (x : P → V)
  (p : P), (f • x) p = ∑ i ∈ f.coeff.support, f.coeff i • x (-i +ᵥ p)
-- Mathlib.Computability.Ackermann
ack_two : ∀ (n : ℕ), ack 2 n = 2 * n + 3
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.preLeft_obj_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (F : CategoryTheory.Functor C A) (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma (F.comp L) R),
  ((CategoryTheory.Comma.preLeft F L R).obj X).right = X.right
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedLinearMap.mk : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] {f : E → F},
  IsLinearMap 𝕜 f → (∃ M, 0 < M ∧ ∀ (x : E), ‖f x‖ ≤ M * ‖x‖) → IsBoundedLinearMap 𝕜 f
-- Lean.Data.Lsp.Basic
Lean.Lsp.ProgressParams.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (token : Lean.Lsp.ProgressToken) (value : α),
  sizeOf { token := token, value := value } = 1 + sizeOf token + sizeOf value
-- Mathlib.CategoryTheory.Comma.Over.StrictInitial
CategoryTheory.MorphismProperty.overEquivOfIsInitial_functor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.MorphismProperty C)
  [inst_1 : P.ContainsIdentities] [inst_2 : Q.IsMultiplicative] [inst_3 : Q.RespectsIso]
  [inst_4 : CategoryTheory.Limits.HasStrictInitialObjects C] (X : C) (h : CategoryTheory.Limits.IsInitial X),
  (CategoryTheory.MorphismProperty.overEquivOfIsInitial.{w, v_1, u_1} P Q X h).functor =
    CategoryTheory.Functor.star (P.Over Q X)
-- Mathlib.Data.Set.MulAntidiagonal
Set.mulAntidiagonal_mono_left : ∀ {α : Type u_1} [inst : Mul α] {s₁ s₂ t : Set α} {a : α}, s₁ ⊆ s₂ → s₁.mulAntidiagonal t a ⊆ s₂.mulAntidiagonal t a
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.MorphismProperty.CostructuredArrow.hasPullbacks : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {A : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A] {L : CategoryTheory.Functor A T} (X : T) [P.IsStableUnderComposition]
  [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P] [CategoryTheory.Limits.HasPullbacks A]
  [CategoryTheory.Limits.HasPullbacks T]
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan L],
  CategoryTheory.Limits.HasPullbacks (P.CostructuredArrow ⊤ L X)
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
MvQPF.Cofix.dest_corec' : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u}
  (g : β → F (α ::: (MvQPF.Cofix F α ⊕ β))) (x : β),
  (MvQPF.Cofix.corec' g x).dest = MvFunctor.map (TypeVec.id ::: Sum.elim id (MvQPF.Cofix.corec' g)) (g x)
-- Mathlib.Algebra.EuclideanDomain.Defs
/-- An additional constraint on `r`.  -/
EuclideanDomain.mul_left_not_lt : ∀ {R : Type u} [self : EuclideanDomain R] (a : R) {b : R}, b ≠ 0 → ¬EuclideanDomain.r (a * b) a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_eq_of_mem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  m.WF → ∀ {k fallback : α}, k ∈ m → m.getKeyD k fallback = k
-- Mathlib.GroupTheory.Coset.Basic
/-- If `s ≤ t`, then there is a map `α ⧸ s → α ⧸ t`.  -/
Subgroup.quotientMapOfLE : {α : Type u_1} → [inst : Group α] → {s t : Subgroup α} → s ≤ t → α ⧸ s → α ⧸ t
-- Mathlib.Topology.ApproximateUnit
/-- A unital magma with a topology and bornology has the trivial approximate unit `pure 1`.  -/
Filter.IsApproximateUnit.pure_one : ∀ (α : Type u_1) [inst : TopologicalSpace α] [inst_1 : MulOneClass α], (pure 1).IsApproximateUnit
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.toENat_lt_natCast : ∀ {c : Cardinal.{u}} {n : ℕ}, Cardinal.toENat c < ↑n ↔ c < ↑n
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.rightUnitor_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] (P : C),
  (CategoryTheory.Limits.coprod.rightUnitor P).inv = CategoryTheory.Limits.coprod.inl
-- Mathlib.Analysis.Calculus.DSlope
differentiableAt_dslope_of_ne : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {a b : 𝕜}, b ≠ a → (DifferentiableAt 𝕜 (dslope f a) b ↔ DifferentiableAt 𝕜 f b)
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.currying_functor_obj_obj : ∀ {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]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : C × D),
  (CategoryTheory.Functor.currying.functor.obj F).obj X = (F.obj X.1).obj X.2
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.card_le_mul_card_image_of_maps_to : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β},
  (∀ a ∈ s, f a ∈ t) → ∀ (n : ℕ), (∀ b ∈ t, {a ∈ s | f a = b}.card ≤ n) → s.card ≤ n * t.card
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.mk_lt_mk_of_comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X A₁ A₂ : C} {i₁ : A₁ ⟶ X} {i₂ : A₂ ⟶ X}
  [inst_1 : CategoryTheory.Mono i₁] [inst_2 : CategoryTheory.Mono i₂] (f : A₁ ⟶ A₂),
  CategoryTheory.CategoryStruct.comp f i₂ = i₁ →
    ¬CategoryTheory.IsIso f → CategoryTheory.Subobject.mk i₁ < CategoryTheory.Subobject.mk i₂
-- Mathlib.Algebra.Group.Equiv.Opposite
AddHom.unop.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : Add M] [inst_1 : Add N], AddHom.unop = AddHom.op.symm
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.EvalTacticFailure.exception : Lean.Elab.Tactic.Grind.EvalTacticFailure → Lean.Exception
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- If `f` is a multiplicative Freiman isomorphism from `A` to `B`, then `f.invFunOn A` is
a multiplicative Freiman isomorphism from `B` to `A`.  -/
IsMulFreimanIso.invFunOn : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {B : Set β} {f : α → β}
  {n : ℕ}, IsMulFreimanIso n A B f → IsMulFreimanIso n B A (Function.invFunOn f A)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.lintegral_coe_eq_integral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → NNReal),
  MeasureTheory.Integrable (fun x => ↑(f x)) μ → ∫⁻ (a : α), ↑(f a) ∂μ = ENNReal.ofReal (∫ (a : α), ↑(f a) ∂μ)
-- Mathlib.Data.PNat.Prime
PNat.lcm_coe : ∀ (n m : ℕ+), ↑(n.lcm m) = (↑n).lcm ↑m
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.IsFiltered.sequentialFunctor_final_aux : ∀ (J : Type u_2) [inst : Countable J] [inst_1 : Preorder J] [inst_2 : CategoryTheory.IsFiltered J] (j : J),
  ∃ n, j ≤ CategoryTheory.Limits.IsFiltered.sequentialFunctor_obj J n
-- Mathlib.CategoryTheory.Filtered.Final
Monotone.final_functor_iff : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : Preorder J₁] [inst_1 : Preorder J₂] [IsDirectedOrder J₁] {f : J₁ → J₂}
  (hf : Monotone f), hf.functor.Final ↔ ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁
-- Init.Data.String.Iterator
/-- Replaces the current character in the string.

Does nothing if the iterator is at the end of the string. If both the replacement character and the
replaced character are 7-bit ASCII characters and the string is not shared, then it is updated
in-place and not copied.
 -/
String.Legacy.Iterator.setCurr : String.Legacy.Iterator → Char → String.Legacy.Iterator
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.Hom.le_iff_le : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] {J₁ J₂ : CategoryTheory.CardinalDirectedPoset κ} (f : J₁ ⟶ J₂)
  (x₁ x₂ : ↑J₁.obj), (CategoryTheory.ConcreteCategory.hom f) x₁ ≤ (CategoryTheory.ConcreteCategory.hom f) x₂ ↔ x₁ ≤ x₂
-- Init.Data.UInt.Basic
UInt16.modn : UInt16 → ℕ → UInt16
-- Init.Data.Int.Order
Int.le_of_add_le_add_left : ∀ {a b c : ℤ}, a + b ≤ a + c → b ≤ c
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
CochainComplex.isStrictlyGE_mappingCone : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (f : K ⟶ L) (n₁ n₂ n : ℤ)
  [K.IsStrictlyGE n₁] [L.IsStrictlyGE n₂],
  autoParam (n < n₁) CochainComplex.isStrictlyGE_mappingCone._auto_1 →
    autoParam (n ≤ n₂) CochainComplex.isStrictlyGE_mappingCone._auto_3 → (CochainComplex.mappingCone f).IsStrictlyGE n
-- Lean.Util.Trace
Lean.instExceptToTraceResultOption : {α ε : Type} → Lean.ExceptToTraceResult ε (Option α)
-- Mathlib.RingTheory.SimpleModule.Basic
_private.Mathlib.RingTheory.SimpleModule.Basic.0.LinearMap.isSemisimpleModule_of_surjective : {R : Type u_2} →
  {S : Type u_3} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {M' : Type u_6} →
          [inst_2 : AddCommGroup M'] →
            [inst_3 : Module R M'] →
              {N' : Type u_7} →
                [inst_4 : AddCommGroup N'] →
                  [inst_5 : Module S N'] →
                    {σ : R →+* S} →
                      (l : M' →ₛₗ[σ] N') →
                        Function.Surjective ⇑l → [IsSemisimpleModule R M'] → ProofWanted (IsSemisimpleModule S N')
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary
spectrum_subset_unitary_of_mem_unitary : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra ℂ A]
  [ContinuousFunctionalCalculus ℂ A IsStarNormal] {u : A}, u ∈ unitary A → spectrum ℂ u ⊆ ↑(unitary ℂ)
-- Mathlib.Probability.Distributions.Poisson.Basic
/-- The pmf of the Poisson distribution depending on its rate, as a PMF.  -/
ProbabilityTheory.poissonPMF : NNReal → PMF ℕ
-- Mathlib.CategoryTheory.GradedObject
/-- The canonical morphism of `J`-graded objects `X.mapObj p ⟶ Y.mapObj p` induced by
a morphism `X ⟶ Y` of `I`-graded objects and a map `p : I → J`.  -/
CategoryTheory.GradedObject.mapMap : {I : Type u_1} →
  {J : Type u_2} →
    {C : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_4} C] →
        {X Y : CategoryTheory.GradedObject I C} →
          (X ⟶ Y) → (p : I → J) → [inst_1 : X.HasMap p] → [inst_2 : Y.HasMap p] → X.mapObj p ⟶ Y.mapObj p
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- A zero morphism `0 : X ⟶ Y` is an isomorphism if and only if
`X` and `Y` are isomorphic to the zero object.
 -/
CategoryTheory.Limits.isIsoZeroEquivIsoZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] → (X Y : C) → CategoryTheory.IsIso 0 ≃ (X ≅ 0) × (Y ≅ 0)
-- Std.Time.Internal.Bounded
/-- A `Bounded` integer where the relation used is the less-than relation, so it includes all
integers that `lo < val < hi`.
 -/
Std.Time.Internal.Bounded.LT : ℤ → ℤ → Type
-- Init.Data.Fin.Iterate
/-- Applies an index-dependent function `f` to all of the values in `[i:n]`, starting at `i` with an
initial accumulator `a`.

Concretely, `Fin.hIterateFrom P f i a` is equal to
```lean
  a |> f i |> f (i + 1) |> ... |> f (n - 1)
```

Theorems about `Fin.hIterateFrom` can be proven using the general theorem `Fin.hIterateFrom_elim` or
other more specialized theorems.

`Fin.hIterate` is a variant that always starts at `0`.
 -/
Fin.hIterateFrom : (P : ℕ → Sort u_1) → {n : ℕ} → ((i : Fin n) → P ↑i → P (↑i + 1)) → (i : ℕ) → i ≤ n → P i → P n
-- Mathlib.RingTheory.WittVector.IsPoly
WittVector.IsPoly₂.mk' : ∀ {p : ℕ} {f : ⦃R : Type u_2⦄ → [CommRing R] → WittVector p R → WittVector p R → WittVector p R},
  (∃ φ,
      ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : WittVector p R),
        (f x y).coeff = fun n => WittVector.peval (φ n) ![x.coeff, y.coeff]) →
    WittVector.IsPoly₂ p f
-- Mathlib.CategoryTheory.Shift.Localization
CategoryTheory.Functor.commShiftOfLocalization.iso_hom_app_assoc : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W] {A : Type w} [inst_4 : AddMonoid A]
  [inst_5 : CategoryTheory.HasShift C A] (F : CategoryTheory.Functor C E) (F' : CategoryTheory.Functor D E)
  [inst_6 : CategoryTheory.Localization.Lifting L W F F'] [inst_7 : CategoryTheory.HasShift D A]
  [inst_8 : CategoryTheory.HasShift E A] [inst_9 : L.CommShift A] [inst_10 : F.CommShift A] (a : A) (X : C) {Z : E}
  (h : (CategoryTheory.shiftFunctor E a).obj (F'.obj (L.obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftOfLocalization.iso L W F F' a).hom.app (L.obj X))
      h =
    CategoryTheory.CategoryStruct.comp (F'.map ((CategoryTheory.Functor.commShiftIso L a).inv.app X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Localization.Lifting.iso L W F F').hom.app ((CategoryTheory.shiftFunctor C a).obj X))
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).hom.app X)
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.shiftFunctor E a).map ((CategoryTheory.Localization.Lifting.iso L W F F').inv.app X)) h)))
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_hom_app_τ₃_app : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X : CategoryTheory.ShortComplex (CategoryTheory.Functor J C)) (X_1 : J),
  ((CategoryTheory.ShortComplex.FunctorEquivalence.unitIso J C).hom.app X).τ₃.app X_1 =
    CategoryTheory.CategoryStruct.id (X.X₃.obj X_1)
-- Batteries.Data.String.Legacy
/-- Implementation of `String.Legacy.map`.  -/
String.Legacy.mapAux : (Char → Char) → String.Pos.Raw → String → String
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.instIsMonoidalClosedModuleCatIsFG : ∀ (K : Type u) [inst : Field K], (ModuleCat.isFG K).IsMonoidalClosed