mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.RightExtension.coneAt_π_app : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} (E : L.RightExtension F) (Y : D)
  (g : CategoryTheory.StructuredArrow Y L),
  (E.coneAt Y).π.app g =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.CostructuredArrow.left E).map g.hom)
      ((CategoryTheory.CostructuredArrow.hom E).app g.right)
-- Init.Prelude
NatPow.mk : {α : Type u} → (α → ℕ → α) → NatPow α
-- Mathlib.Analysis.Meromorphic.FactorizedRational
/-- The order of the factorized rational function `(∏ᶠ u, fun z ↦ (z - u) ^ d u)` at `z` equals `d z`.
 -/
Function.FactorizedRational.meromorphicOrderAt_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {z : 𝕜} (d : 𝕜 → ℤ),
  Function.HasFiniteSupport d → meromorphicOrderAt (∏ᶠ (u : 𝕜), (fun x => x - u) ^ d u) z = ↑(d z)
-- Mathlib.Data.Nat.Digits.Lemmas
/-- The formula for the sum of the sum of the digits in base `b` over the natural integers `< b ^ l`.
 -/
Nat.sum_sum_digits_eq : ∀ {b : ℕ}, 1 < b → ∀ (l : ℕ), ∑ x ∈ Finset.range (b ^ l), (b.digits x).sum = l * b ^ (l - 1) * b.choose 2
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.coe_toAddSubgroup : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R), ↑s.toAddSubgroup = ↑s
-- Mathlib.LinearAlgebra.BilinearMap
/-- Composing a given linear map `M → N` with a linear map `N → P` as a linear map from
`Nₗ →ₗ[R] Pₗ` to `M →ₗ[R] Pₗ`.  -/
LinearMap.lcomp : {R : Type u_1} →
  (S : Type u_3) →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {M : Type u_5} →
          {M₂ : Type u_6} →
            (N : Type u_7) →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : AddCommMonoid N] →
                    [inst_5 : Module R M] →
                      [inst_6 : Module R M₂] →
                        [inst_7 : Module S N] →
                          [inst_8 : Module R N] →
                            [inst_9 : SMulCommClass R S N] → (M →ₗ[R] M₂) → (M₂ →ₗ[R] N) →ₗ[S] M →ₗ[R] N
-- Lean.Elab.Do.Basic
/-- Create a `ReturnCont` returning the result using `pure`.  -/
Lean.Elab.Do.ReturnCont.mkPure : Lean.Expr → Lean.Elab.TermElabM Lean.Elab.Do.ReturnCont
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.orderIsoRpow_apply : ∀ (y : ℝ) (hy : 0 < y) (x : ENNReal), (ENNReal.orderIsoRpow y hy) x = x ^ y
-- Mathlib.Computability.Language
Language.nil_mem_kstar : ∀ {α : Type u_1} (l : Language α), [] ∈ KStar.kstar l
-- Mathlib.Computability.EpsilonNFA
εNFA.IsPath.below.nil : ∀ {α : Type u} {σ : Type v} {M : εNFA α σ} {motive : (a a_1 : σ) → (a_2 : List (Option α)) → M.IsPath a a_1 a_2 → Prop}
  (s : σ), εNFA.IsPath.below ⋯
-- Mathlib.Algebra.Group.Center
Set.prod_addCentralizer_subset_addCentralizer_prod : ∀ {M : Type u_1} [inst : Add M] {N : Type u_2} [inst_1 : Add N] (S : Set M) (T : Set N),
  S.addCentralizer ×ˢ T.addCentralizer ⊆ (S ×ˢ T).addCentralizer
-- Mathlib.Topology.Sober
QuasiSober.of_subset : ∀ {α : Type u_1} [inst : TopologicalSpace α] {V W : Set α} [QuasiSober ↑W],
  IsClosed (Subtype.val ⁻¹' V) → V ⊆ W → QuasiSober ↑V
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.coe_toBasis_repr_apply : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E) (i : ι),
  (b.toBasis.repr x) i = (b.repr x).ofLp i
-- Mathlib.Algebra.Polynomial.Basic
/-- See also `Polynomial.sum_add`.  -/
Polynomial.sum_add' : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : AddCommMonoid S] (p : Polynomial R) (f g : ℕ → R → S),
  p.sum (f + g) = p.sum f + p.sum g
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse_obj_left_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Over.forget c).comp F) G),
  ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse F G c).obj Y).left.hom = Y.hom
-- Mathlib.RingTheory.Lasker
/-- The first uniqueness theorem for primary decomposition, Theorem 4.5 in Atiyah-Macdonald:
In any minimal primary decomposition `I = ⨅ i, q_i`, the ideals `radical (q_i.colon M)` are exactly
the associated primes of `I`.  -/
Submodule.IsMinimalPrimaryDecomposition.image_radical_eq_associated_primes : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {t : Finset (Submodule R M)},
  N.IsMinimalPrimaryDecomposition t → (fun J => (J.colon Set.univ).radical) '' ↑t = N.associatedPrimes
-- Mathlib.Algebra.Order.Monovary
antivary_inv₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : Semifield β] [inst_4 : LinearOrder β] [IsStrictOrderedRing β] {f : ι → α} {g : ι → β},
  StrongLT 0 f → StrongLT 0 g → (Antivary f⁻¹ g⁻¹ ↔ Antivary f g)
-- Mathlib.RingTheory.Bialgebra.Basic
Bialgebra.counit_mul : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A] (a b : A),
  CoalgebraStruct.counit (a * b) = CoalgebraStruct.counit a * CoalgebraStruct.counit b
-- Mathlib.Data.Nat.GCD.Basic
Nat.pow_sub_one_mod_pow_sub_one : ∀ (a b c : ℕ), (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.RightHomotopyClass.mk_eq_mk_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : HomotopicalAlgebra.ModelCategory C]
  [HomotopicalAlgebra.IsFibrant Y] (f g : X ⟶ Y),
  HomotopicalAlgebra.RightHomotopyClass.mk f = HomotopicalAlgebra.RightHomotopyClass.mk g ↔
    HomotopicalAlgebra.RightHomotopyRel f g
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.rootSpaceWeightSpaceProduct.eq_1 : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : LieRing.IsNilpotent ↥H] (M : Type u_3) [inst_4 : AddCommGroup M]
  [inst_5 : Module R M] [inst_6 : LieRingModule L M] [inst_7 : LieModule R L M] (χ₁ χ₂ χ₃ : ↥H → R) (hχ : χ₁ + χ₂ = χ₃),
  LieAlgebra.rootSpaceWeightSpaceProduct R L H M χ₁ χ₂ χ₃ hχ =
    (TensorProduct.LieModule.liftLie R ↥H ↥(LieAlgebra.rootSpace H χ₁) ↥(LieModule.genWeightSpace M χ₂)
        ↥(LieModule.genWeightSpace M χ₃))
      (let __LinearMap := LieAlgebra.rootSpaceWeightSpaceProductAux R L H M hχ;
      { toLinearMap := __LinearMap, map_lie' := ⋯ })
-- Mathlib.Algebra.Order.Nonneg.Field
Nonneg.val_unitsEquivPos_symm_apply_coe : ∀ (R : Type u_2) [inst : DivisionSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : PosMulReflectLT R] (r : { r // 0 < r }), ↑↑((Nonneg.unitsEquivPos R).symm r) = ↑r
-- Mathlib.RingTheory.Ideal.Maps
RingHom.liftOfRightInverseAux_comp_apply : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Ring A] [inst_1 : Ring B] [inst_2 : Ring C] (f : A →+* B)
  (f_inv : B → A) (hf : Function.RightInverse f_inv ⇑f) (g : A →+* C) (hg : RingHom.ker f ≤ RingHom.ker g) (a : A),
  (f.liftOfRightInverseAux f_inv hf g hg) (f a) = g a
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.π_comp_cokernelIsoOfEq_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f g : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasCokernel f] [inst_3 : CategoryTheory.Limits.HasCokernel g]
  (h : f = g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π g)
      (CategoryTheory.Limits.cokernelIsoOfEq h).inv =
    CategoryTheory.Limits.cokernel.π f
-- Mathlib.FieldTheory.Perfect
RingHom.map_frobeniusEquiv_symm : ∀ {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] (p : ℕ) [inst_2 : ExpChar R p]
  [inst_3 : PerfectRing R p] [inst_4 : ExpChar S p] [inst_5 : PerfectRing S p] (f : R →+* S) (x : R),
  f ((frobeniusEquiv R p).symm x) = (frobeniusEquiv S p).symm (f x)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- A category with a zero object has zero morphisms.

It is rarely a good idea to use this. Many categories that have a zero object have zero
morphisms for some other reason, for example from additivity. Library code that uses
`zeroMorphismsOfZeroObject` will then be incompatible with these categories because
the `HasZeroMorphisms` instances will not be definitionally equal. For this reason library
code should generally ask for an instance of `HasZeroMorphisms` separately, even if it already
asks for an instance of `HasZeroObject`.  -/
CategoryTheory.Limits.HasZeroObject.zeroMorphismsOfZeroObject : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroObject C] → CategoryTheory.Limits.HasZeroMorphisms C
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersion.isImmersionOfComplement_complement : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] {H : Type u_7}
  [inst_5 : TopologicalSpace H] {G : Type u_9} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {N : Type u_13} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  (h : Manifold.IsImmersion I J n f), Manifold.IsImmersionOfComplement h.complement I J n f
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.localRingHom_id : ∀ {R : Type u_1} [inst : CommSemiring R] (I : Ideal R) [hI : I.IsPrime],
  Localization.localRingHom I I (RingHom.id R) ⋯ = RingHom.id (Localization.AtPrime I)
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.le_def : ∀ {X : Type u_1} {R : Type u_3} [inst : Zero X] [inst_1 : Zero R] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace R] [inst_4 : PartialOrder R] (f g : ContinuousMapZero X R), f ≤ g ↔ ∀ (x : X), f x ≤ g x
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasColimit.isoOfNatIso_inv_desc_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasColimit G] (t : CategoryTheory.Limits.Cocone F) (w : F ≅ G) {Z : C} (h : t.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasColimit.isoOfNatIso w).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.desc F t) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.desc G ((CategoryTheory.Limits.Cocone.precompose w.inv).obj t)) h
-- Mathlib.Util.Superscript
Mathlib.Tactic.Superscript.Mapping.mk.sizeOf_spec : ∀ (toNormal toSpecial : Std.HashMap Char Char),
  sizeOf { toNormal := toNormal, toSpecial := toSpecial } = 1 + sizeOf toNormal + sizeOf toSpecial
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.homologyMap_eq : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_3}
  {c : ComplexShape ι} {K L : HomologicalComplex C c} {f g : K ⟶ L} (ho : Homotopy f g) (i : ι)
  [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i],
  HomologicalComplex.homologyMap f i = HomologicalComplex.homologyMap g i
-- Mathlib.Data.Set.Finite.Lattice
Set.iUnion_pi_of_monotone : ∀ {ι : Type u_1} {ι' : Type u_2} [inst : LinearOrder ι'] [Nonempty ι'] {α : ι → Type u_3} {I : Set ι}
  {s : (i : ι) → ι' → Set (α i)},
  I.Finite → (∀ i ∈ I, Monotone (s i)) → (⋃ j, I.pi fun i => s i j) = I.pi fun i => ⋃ j, s i j
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
CategoryTheory.LocallyDiscrete.homSmallCategory : {C : Type u} →
  [inst : CategoryTheory.CategoryStruct.{v, u} C] →
    (a b : CategoryTheory.LocallyDiscrete C) → CategoryTheory.SmallCategory (a ⟶ b)
-- Mathlib.Algebra.Module.ZLattice.Basic
/-- Let `e : E → F` a linear map, the map that sends a `L : Submodule ℤ E` to the
`Submodule ℤ F` that is the pullback of `L` by `e`. If `IsZLattice L` and `e` is a continuous
linear equiv, then it is a `IsZLattice` of `E`, see `instIsZLatticeComap`.  -/
ZLattice.comap : (K : Type u_1) →
  [inst : NormedField K] →
    {E : Type u_2} →
      {F : Type u_3} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace K E] →
            [inst_3 : NormedAddCommGroup F] → [inst_4 : NormedSpace K F] → Submodule ℤ E → (F →ₗ[K] E) → Submodule ℤ F
-- Mathlib.Analysis.Convex.KreinMilman
/-- **Krein-Milman lemma**: In an LCTVS, any nonempty compact set has an extreme point.  -/
IsCompact.extremePoints_nonempty : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [T2Space E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] {s : Set E},
  IsCompact s → s.Nonempty → (Set.extremePoints ℝ s).Nonempty
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pushout.isIso_codiagonal_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f f],
  CategoryTheory.IsIso (CategoryTheory.Limits.pushout.codiagonal f) ↔ CategoryTheory.Epi f
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.eq_of_le_of_measure_univ_eq : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ],
  μ ≤ ν → μ Set.univ = ν Set.univ → μ = ν
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.centralizer_toSubsemigroup : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] (s : Set R),
  (NonUnitalSubsemiring.centralizer s).toSubsemigroup = Subsemigroup.centralizer s
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.smul : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {U : Submodule R M}
  {x y : M}, x ≡ y [SMOD U] → ∀ (c : R), c • x ≡ c • y [SMOD U]
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- **Alias** of `AlgebraicGeometry.StructureSheaf.algebraMap_self_map`. -/
AlgebraicGeometry.StructureSheaf.toOpen_res : ∀ (R : Type u) [inst : CommRing R] (U V : (TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))ᵒᵖ)
  (i : V ⟶ U),
  CategoryTheory.CategoryStruct.comp
      (CommRingCat.ofHom (algebraMap R ((AlgebraicGeometry.structureSheafInType R R).obj.obj V)))
      ((AlgebraicGeometry.Spec.structureSheaf R).obj.map i) =
    CommRingCat.ofHom (algebraMap R ((AlgebraicGeometry.structureSheafInType R R).obj.obj U))
-- Mathlib.Analysis.SpecialFunctions.Artanh
/-- `artanh` is defined using a logarithm, `artanh x = log √((1 + x) / (1 - x))`.  -/
Real.artanh : ℝ → ℝ
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.structuredArrowDownwards_map : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) (X₂ : C₂)
  {X Y : CategoryTheory.StructuredArrow X₂ T} (f : X ⟶ Y),
  (w.structuredArrowDownwards X₂).map f =
    (CategoryTheory.StructuredArrow.pre (R.obj X₂) L B).map
      ((CategoryTheory.Comma.mapRight (CategoryTheory.Functor.fromPUnit (R.obj X₂)) w).map
        (CategoryTheory.StructuredArrow.homMk (CategoryTheory.StructuredArrow.Hom.right f) ⋯))
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.IsWide.wide : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {S : CategoryTheory.Subgroupoid C},
  S.IsWide → ∀ (c : C), CategoryTheory.CategoryStruct.id c ∈ S.arrows c c
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.State.readBody.inj : ∀ {dir : Std.Http.Protocol.H1.Direction} {a a_1 : Std.Http.Protocol.H1.Reader.BodyState},
  Std.Http.Protocol.H1.Reader.State.readBody a = Std.Http.Protocol.H1.Reader.State.readBody a_1 → a = a_1
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Comonad.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (toFunctor : CategoryTheory.Functor C C) →
      (ε : toFunctor ⟶ CategoryTheory.Functor.id C) →
        (δ : toFunctor ⟶ toFunctor.comp toFunctor) →
          autoParam
              (∀ (X : C),
                CategoryTheory.CategoryStruct.comp (δ.app X) (toFunctor.map (δ.app X)) =
                  CategoryTheory.CategoryStruct.comp (δ.app X) (δ.app (toFunctor.obj X)))
              CategoryTheory.Comonad.coassoc._autoParam →
            autoParam
                (∀ (X : C),
                  CategoryTheory.CategoryStruct.comp (δ.app X) (ε.app (toFunctor.obj X)) =
                    CategoryTheory.CategoryStruct.id (toFunctor.obj X))
                CategoryTheory.Comonad.left_counit._autoParam →
              autoParam
                  (∀ (X : C),
                    CategoryTheory.CategoryStruct.comp (δ.app X) (toFunctor.map (ε.app X)) =
                      CategoryTheory.CategoryStruct.id (toFunctor.obj X))
                  CategoryTheory.Comonad.right_counit._autoParam →
                CategoryTheory.Comonad C
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.addVal_pow : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] (a : R) (n : ℕ),
  (IsDiscreteValuationRing.addVal R) (a ^ n) = n • (IsDiscreteValuationRing.addVal R) a
-- Mathlib.Topology.Order.Basic
tendstoIooClassNhds : ∀ {α : Type u} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] (a : α),
  Filter.TendstoIxxClass Set.Ioo (nhds a) (nhds a)
-- Init.Data.UInt.Lemmas
UInt8.toUInt16_add : ∀ (a b : UInt8), (a + b).toUInt16 = (a.toUInt16 + b.toUInt16) % 256
-- Lean.Meta.Sym.AlphaShareBuilder
/-- Helper function for lifting a `AlphaShareBuilderM` action to `GrindM`
 -/
Lean.Meta.Sym.Internal.liftBuilderM : {α : Type} → Lean.Meta.Sym.Internal.AlphaShareBuilderM α → Lean.Meta.Sym.SymM α
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- A constructor for natural transformations between functors from `WalkingReflexivePair`.  -/
CategoryTheory.Limits.reflexivePair.mkNatTrans : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C} →
      (e₀ :
          F.obj CategoryTheory.Limits.WalkingReflexivePair.zero ⟶
            G.obj CategoryTheory.Limits.WalkingReflexivePair.zero) →
        (e₁ :
            F.obj CategoryTheory.Limits.WalkingReflexivePair.one ⟶
              G.obj CategoryTheory.Limits.WalkingReflexivePair.one) →
          autoParam
              (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) e₀ =
                CategoryTheory.CategoryStruct.comp e₁ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left))
              _auto_144✝ →
            autoParam
                (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right) e₀ =
                  CategoryTheory.CategoryStruct.comp e₁ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right))
                _auto_146✝ →
              autoParam
                  (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion)
                      e₁ =
                    CategoryTheory.CategoryStruct.comp e₀
                      (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion))
                  _auto_148✝ →
                (F ⟶ G)
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.instHasInitialLeftExtensionOfHasLeftKanExtension : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  [CategoryTheory.Bicategory.HasLeftKanExtension f g],
  CategoryTheory.Limits.HasInitial (CategoryTheory.Bicategory.LeftExtension f g)
-- Mathlib.RingTheory.DedekindDomain.SInteger
Set.unit_eq : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R))
  (K : Type v) [inst_2 : Field K] [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K],
  S.unit K = ⨅ v, ⨅ (_ : v ∉ S), (IsDedekindDomain.HeightOneSpectrum.valuation K v).valuationSubring.unitGroup
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Atom₁.mk.inj : ∀ {e : Lean.Expr} {src tgt : Mathlib.Tactic.BicategoryLike.Obj} {e_1 : Lean.Expr}
  {src_1 tgt_1 : Mathlib.Tactic.BicategoryLike.Obj},
  { e := e, src := src, tgt := tgt } = { e := e_1, src := src_1, tgt := tgt_1 } → e = e_1 ∧ src = src_1 ∧ tgt = tgt_1
-- Init.Data.SInt.Basic
/-- Decides whether one word-sized signed integer is strictly less than another. Usually accessed via the
`DecidableLT ISize` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if ((-7) : ISize) < 7 then "yes" else "no") = "yes"`
 * `(if (5 : ISize) < 5 then "yes" else "no") = "no"`
 * `show ¬((7 : ISize) < 7) by decide`
 -/
ISize.decLt : (a b : ISize) → Decidable (a < b)
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.Hom.id_hom : ∀ {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] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] (F : CategoryTheory.SingleFunctors C D A) (x : A),
  (CategoryTheory.SingleFunctors.Hom.id F).hom x = CategoryTheory.CategoryStruct.id (F.functor x)
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.image_coe_Ioc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, WithTop.some '' Set.Ioc a b = Set.Ioc ↑a ↑b
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.pow_card_pow : ∀ {K : Type u_1} [inst : GroupWithZero K] [inst_1 : Fintype K] (n : ℕ) (a : K), a ^ Fintype.card K ^ n = a
-- Init.Data.Int.LemmasAux
Int.ofNat_add_one_out : ∀ (n : ℕ), ↑n + 1 = ↑n.succ
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_multiset_sum_le : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] (m : Multiset E), ‖m.sum‖₊ ≤ (Multiset.map (fun x => ‖x‖₊) m).sum
-- Init.Control.StateCps
StateCpsT.instMonad : {σ : Type u} → {m : Type u → Type v} → Monad (StateCpsT σ m)
-- Lean.Util.NumObjs
Lean.Expr.NumObjs.visit : Lean.Expr → Lean.Expr.NumObjs.M Unit
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.HandlerTrie.brecOn_2.go : {motive_1 : Lean.Elab.ConfigEval.HandlerTrie✝ → Sort u} →
  {motive_2 : Array (String × Lean.Elab.ConfigEval.HandlerTrie✝) → Sort u} →
    {motive_3 : List (String × Lean.Elab.ConfigEval.HandlerTrie✝) → Sort u} →
      {motive_4 : String × Lean.Elab.ConfigEval.HandlerTrie✝ → Sort u} →
        (t : List (String × Lean.Elab.ConfigEval.HandlerTrie✝)) →
          ((t : Lean.Elab.ConfigEval.HandlerTrie✝) → Lean.Elab.ConfigEval.HandlerTrie.below✝ t → motive_1 t) →
            ((t : Array (String × Lean.Elab.ConfigEval.HandlerTrie✝)) →
                Lean.Elab.ConfigEval.HandlerTrie.below_1✝ t → motive_2 t) →
              ((t : List (String × Lean.Elab.ConfigEval.HandlerTrie✝)) →
                  Lean.Elab.ConfigEval.HandlerTrie.below_2✝ t → motive_3 t) →
                ((t : String × Lean.Elab.ConfigEval.HandlerTrie✝) →
                    Lean.Elab.ConfigEval.HandlerTrie.below_3✝ t → motive_4 t) →
                  motive_3 t ×' Lean.Elab.ConfigEval.HandlerTrie.below_2✝ t
-- Init.Grind.Attr
/-- Like `@[lia!]`, but also prints the pattern(s) selected by `lia` as info messages.  -/
Lean.Parser.Attr.lia!? : Lean.ParserDescr