mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.coe_symm_toHomeomorph : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂), ⇑e.toHomeomorph.symm = ⇑e.symm
-- Mathlib.Data.Vector3
Vector3.cons_fz : ∀ {α : Type u_1} {n : ℕ} (a : α) (v : Vector3 α n), Vector3.cons a v Fin2.fz = a
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.det_adjugate : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α),
  A.adjugate.det = A.det ^ (Fintype.card n - 1)
-- Init.Data.Nat.Basic
Nat.lt_of_add_right_lt : ∀ {n m k : ℕ}, n + k < m → n < m
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.ofIso_Ω₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (𝒞 : CategoryTheory.Subobject.Classifier C) {Ω₀ Ω : C}
  (eΩ : 𝒞.Ω ≅ Ω) (eΩ₀ : 𝒞.Ω₀ ≅ Ω₀) (from' : (C_1 : C) → C_1 ⟶ Ω₀) (t : Ω₀ ⟶ Ω)
  (ht :
    autoParam (t = CategoryTheory.CategoryStruct.comp eΩ₀.inv (CategoryTheory.CategoryStruct.comp 𝒞.truth eΩ.hom))
      CategoryTheory.Subobject.Classifier.ofIso._auto_1),
  (𝒞.ofIso eΩ eΩ₀ from' t ht).Ω₀ = Ω₀
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `E / F` is a separable field extension of exponential characteristic `q`, then
`F⟮a⟯ = F⟮a ^ q⟯` for any `a : E`.  -/
IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_of_isSeparable' : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsSeparable F E] (a : E)
  (q : ℕ) [ExpChar F q], F⟮a⟯ = F⟮a ^ q⟯
-- Mathlib.Algebra.Lie.SerreConstruction
Matrix.instInhabitedToLieAlgebra : (R : Type u_1) →
  {B : Type u_2} →
    [inst : CommRing R] → (CM : Matrix B B ℤ) → [inst_1 : DecidableEq B] → Inhabited (Matrix.ToLieAlgebra R CM)
-- Mathlib.CategoryTheory.Monoidal.Ring
/-- The property that a morphism between ring objects is a ring morphism.  -/
CategoryTheory.IsRingHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {R₁ R₂ : C} →
        [CategoryTheory.AddMonObj R₁] →
          [CategoryTheory.AddMonObj R₂] → [CategoryTheory.MonObj R₁] → [CategoryTheory.MonObj R₂] → (R₁ ⟶ R₂) → Prop
-- Mathlib.NumberTheory.ModularForms.Basic
ModularFormClass.bdd_at_infty : ∀ {k : ℤ} {F : Type u_1} {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : FunLike F UpperHalfPlane ℂ] (f : F)
  [ModularFormClass F Γ k] [Fact (IsCusp OnePoint.infty Γ)], UpperHalfPlane.IsBoundedAtImInfty ⇑f
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.isDenseInducing_pureCauchy : ∀ {α : Type u} [inst : UniformSpace α], IsDenseInducing CauchyFilter.pureCauchy
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_apply : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) (x : ↑S.moduleCatLeftHomologyData.K),
  (CategoryTheory.ConcreteCategory.hom S.homologyπ) ((CategoryTheory.ConcreteCategory.hom S.moduleCatCyclesIso.inv) x) =
    (CategoryTheory.ConcreteCategory.hom S.moduleCatHomologyIso.inv)
      ((CategoryTheory.ConcreteCategory.hom S.moduleCatLeftHomologyData.π) x)
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.HomotopyCategory.congr_arrowMk_homMk : ∀ {V : SSet.Truncated 2} {x₀ x₁ : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })}
  (e : SSet.Truncated.Edge x₀ x₁)
  {y₀ y₁ : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })}
  (e' : SSet.Truncated.Edge y₀ y₁),
  e.edge = e'.edge →
    CategoryTheory.Arrow.mk (SSet.Truncated.HomotopyCategory.homMk e) =
      CategoryTheory.Arrow.mk (SSet.Truncated.HomotopyCategory.homMk e')
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_fin_two_of : ∀ {R : Type u_6} [inst : AddCommMonoid R] (a b c d : R), !![a, b; c, d].trace = a + d
-- Init.Data.List.Basic
List.zipWith.eq_2 : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (x : List α) (x_1 : List β),
  (∀ (x_2 : α) (xs : List α) (y : β) (ys : List β), x = x_2 :: xs → x_1 = y :: ys → False) → List.zipWith f x x_1 = []
-- Init.Data.Order.Opposite
Std.OppositeOrderInstances.instIsLinearOrderOpposite : ∀ {α : Type u_1} {i : LE α} [Std.IsLinearOrder α], Std.IsLinearOrder α
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableWithinAt_iff_of_mem_maximalAtlas : ∀ {𝕜 : 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 : Set M}
  {e : OpenPartialHomeomorph M H} {e' : OpenPartialHomeomorph M' H'} {x : M},
  e ∈ IsManifold.maximalAtlas I 1 M →
    e' ∈ IsManifold.maximalAtlas I' 1 M' →
      x ∈ e.source →
        f x ∈ e'.source →
          (MDiffAt[s] f x ↔
            ContinuousWithinAt f s x ∧
              DifferentiableWithinAt 𝕜 (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm)
                (↑(e.extend I).symm ⁻¹' s ∩ Set.range ↑I) (↑(e.extend I) x))
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator.mk.injEq : ∀ (curr top curr_1 top_1 : ℕ),
  ({ curr := curr, top := top } = { curr := curr_1, top := top_1 }) = (curr = curr_1 ∧ top = top_1)
-- Lean.Data.Lsp.Internal
/-- Definition site and usage sites of a reference. Obtained from `Lean.Server.RefInfo`.  -/
Lean.Lsp.RefInfo : Type
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.inv_comp_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (α : X ≅ Y) {f : X ⟶ Z} {g : Y ⟶ Z},
  CategoryTheory.CategoryStruct.comp α.inv f = g ↔ f = CategoryTheory.CategoryStruct.comp α.hom g
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mop.sizeOf_spec : ∀ {C : Type u₁} [inst : SizeOf C] (unmop : C), sizeOf { unmop := unmop } = 1 + sizeOf unmop
-- Mathlib.Algebra.PEmptyInstances
SemigroupPEmpty : Semigroup PEmpty.{u + 1}
-- Mathlib.Order.Defs.LinearOrder
/-- The underlying linearly ordered type.  -/
LinOrd.carrier : LinOrd → Type u_2
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.abs_eval_T_real_le_one_iff : ∀ {n : ℤ}, n ≠ 0 → ∀ (x : ℝ), |x| ≤ 1 ↔ |Polynomial.eval x (Polynomial.Chebyshev.T ℝ n)| ≤ 1
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.id_comp : ∀ {B : Type u} [inst : Quiver B] {a b : B} {f g : CategoryTheory.FreeBicategory.Hom a b}
  (η : CategoryTheory.FreeBicategory.Hom₂ f g),
  CategoryTheory.FreeBicategory.Rel ((CategoryTheory.FreeBicategory.Hom₂.id f).vcomp η) η
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.Embedding.toEmbedding_toPartialEquiv : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Embedding M N), FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop ⋯ = f
-- Mathlib.CategoryTheory.DinatTrans
/-- Pre-composition with a natural transformation.  -/
CategoryTheory.DinatTrans.precompNatTrans : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G H : CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C D)} →
          CategoryTheory.DinatTrans G H → (F ⟶ G) → CategoryTheory.DinatTrans F H
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k a : α}
  {fallback : β a} {v : β k},
  (m.insert k v).getD a fallback = if h : (k == a) = true then cast ⋯ v else m.getD a fallback
-- Mathlib.CategoryTheory.Filtered.Final
/-- The forgetful functor of the under category on any filtered or empty category is final.  -/
CategoryTheory.Under.final_forget : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.IsFilteredOrEmpty C] (c : C),
  (CategoryTheory.Under.forget c).Final
-- Mathlib.Order.Bounds.Image
bddAbove_range_pi : ∀ {α : Type u} {ι : Sort x} {π : α → Type u_1} [inst : (a : α) → Preorder (π a)] {F : ι → (a : α) → π a},
  BddAbove (Set.range F) ↔ ∀ (a : α), BddAbove (Set.range fun i => F i a)
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
CategoryTheory.StrongMonoCategory.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (∀ {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f], CategoryTheory.StrongMono f) → CategoryTheory.StrongMonoCategory C
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.Solvers.mergeTerms.toPendingDiseqs : Lean.Meta.Grind.SolverTerms → Lean.Meta.Grind.ParentSet → Lean.Meta.Grind.PendingSolverPropagationsData✝
-- Mathlib.Topology.Order.IntermediateValue
intermediate_value_Ioo : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α}, a ≤ b → ∀ {f : α → δ}, ContinuousOn f (Set.Icc a b) → Set.Ioo (f a) (f b) ⊆ f '' Set.Ioo a b
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instAddSemigroupQuotient : {R : Type u_1} → [inst : AddSemigroup R] → [inst_1 : Mul R] → (c : RingCon R) → AddSemigroup c.Quotient
-- Init.Data.Option.Lemmas
Option.or_of_isSome : ∀ {α : Type u_1} {o o' : Option α}, o.isSome = true → o.or o' = o
-- Init.Data.SInt.Lemmas
Int64.pow_zero : ∀ (x : Int64), x ^ 0 = 1
-- Mathlib.LinearAlgebra.Ray
Module.Ray.neg_units_smul : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (u : Rˣ) (v : Module.Ray R M), -u • v = -(u • v)
-- Mathlib.MeasureTheory.Integral.SetToL1
/-- Extend `Set α → E →L[ℝ] F` to `(α →₁[μ] E) →L[ℝ] F`.  -/
MeasureTheory.L1.setToL1 : {α : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              {m : MeasurableSpace α} →
                {μ : MeasureTheory.Measure α} →
                  [CompleteSpace F] →
                    {T : Set α → E →L[ℝ] F} →
                      {C : ℝ} → MeasureTheory.DominatedFinMeasAdditive μ T C → ↥(MeasureTheory.Lp E 1 μ) →L[ℝ] F
-- Mathlib.Analysis.Normed.Module.Basic
norm_intCast_eq_abs_mul_norm_one : ∀ (α : Type u_6) [inst : SeminormedRing α] [NormSMulClass ℤ α] (n : ℤ), ‖↑n‖ = ↑|n| * ‖1‖
-- Lean.Server.ServerTask
Lean.Server.ServerTask.get : {α : Type u_1} → Lean.Server.ServerTask α → α
-- Mathlib.RepresentationTheory.Character
/-- The character is multiplicative under the tensor product.  -/
Representation.char_tensor : ∀ {G : Type u_1} {k : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Field k]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [FiniteDimensional k V] [inst_5 : AddCommGroup W]
  [inst_6 : Module k W] [FiniteDimensional k W] (ρ : Representation k G V) (σ : Representation k G W),
  (ρ.tprod σ).character = ρ.character * σ.character
-- Mathlib.RingTheory.Lasker
Submodule.IsMinimalPrimaryDecomposition.mk : ∀ {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)},
  t.inf id = N →
    (∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary) →
      (↑t).Pairwise (Function.onFun (fun x1 x2 => x1 ≠ x2) fun J => (J.colon Set.univ).radical) →
        (∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J) → N.IsMinimalPrimaryDecomposition t
-- Lean.Data.PersistentArray
Lean.instInhabitedPersistentArrayNode.default : {α : Type u} → Lean.PersistentArrayNode α
-- Mathlib.Algebra.WithConv
WithConv.symm_linearEquiv_apply : ∀ {R : Type u_1} {A : Type u_2} [inst : AddCommMonoid A] [inst_1 : Semiring R] [inst_2 : Module R A] (a : A),
  (WithConv.linearEquiv R A).symm a = WithConv.toConv a
-- Init.Data.UInt.Lemmas
UInt16.toUInt16_toUSize : ∀ (n : UInt16), n.toUSize.toUInt16 = n
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.descFunLift.eq_4 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat)
  (s : CategoryTheory.Limits.Cocone F) (x_1 : CommRingCat.Colimits.Prequotient F),
  CommRingCat.Colimits.descFunLift F s x_1.neg = -CommRingCat.Colimits.descFunLift F s x_1
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafCommRing.ι_forgetStalk_inv_assoc : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (R : Type u)
  [inst_9 : TopologicalSpace R] [inst_10 : ChartedSpace H R] [inst_11 : CommRing R] [inst_12 : ContMDiffRing I (↑⊤) R]
  (x : ↑(TopCat.of M)) (U : (TopologicalSpace.OpenNhds x)ᵒᵖ) {Z : Type u}
  (h : ↑((smoothSheafCommRing IM I M R).presheaf.stalk x) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheaf IM I M R).presheaf)
        U)
      (CategoryTheory.CategoryStruct.comp (smoothSheafCommRing.forgetStalk IM I M R x).inv h) =
    CategoryTheory.CategoryStruct.comp
      (TypeCat.ofHom
        ⇑(CommRingCat.Hom.hom
            (CategoryTheory.Limits.colimit.ι
              ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf) U)))
      h
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- `leftMulMatrix b x` is the matrix corresponding to the linear map `fun y ↦ x * y`.

`leftMulMatrix_eq_repr_mul` gives a formula for the entries of `leftMulMatrix`.

This definition is useful for doing (more) explicit computations with `LinearMap.mulLeft`,
such as the trace form or norm map for algebras.
 -/
Algebra.leftMulMatrix : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] →
        [inst_2 : Algebra R S] →
          {m : Type u_3} → [inst_3 : Fintype m] → [inst_4 : DecidableEq m] → Module.Basis m R S → S →ₐ[R] Matrix m m R
-- Mathlib.Topology.Algebra.Module.Star
starL'.congr_simp : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid A]
  [inst_3 : StarAddMonoid A] [inst_4 : Module R A] [inst_5 : StarModule R A] [inst_6 : TopologicalSpace A]
  [inst_7 : ContinuousStar A] [inst_8 : TrivialStar R], starL' R = starL' R
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquivClass.instNonUnitalStarRingHomClass : ∀ {F : Type u_1} {A : Type u_2} {B : Type u_3} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B] [inst_4 : EquivLike F A B]
  [inst_5 : StarRingEquivClass F A B], NonUnitalStarRingHomClass F A B
-- Init.Data.Option.Lemmas
Option.default_eq_none : ∀ {α : Type u_1}, default = none
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.homCategory.ext : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {m n : η ⟶ θ}, (∀ (b : B), m.as.app b = n.as.app b) → m = n
-- Batteries.Util.ProofWanted
_private.Batteries.Util.ProofWanted.0.WantedRefKind.proofWanted.sizeOf_spec : sizeOf WantedRefKind.proofWanted✝ = 1
-- Mathlib.Order.Filter.Cocardinal
Filter.hasBasis_cocardinal : ∀ {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular},
  (Filter.cocardinal α hreg).HasBasis (fun s => Cardinal.mk ↑s < c) compl
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
/-- Given a morphism of presheaves of rings `φ : S ⟶ F.op ⋙ R`, where `F : C ⥤ D`,
`S : Cᵒᵖ ⥤ RingCat`, `R : Dᵒᵖ ⥤ RingCat` and `X : C`, the (partial) left adjoint
functor of `pushforward φ` is defined on the object `(free S).obj (yoneda.obj X)`:
this object shall be mapped to `(free R).obj (yoneda.obj (F.obj X))`.  -/
PresheafOfModules.pushforwardCompCoyonedaFreeYonedaCorepresentableBy : {C D : Type u} →
  [inst : CategoryTheory.SmallCategory C] →
    [inst_1 : CategoryTheory.SmallCategory D] →
      {F : CategoryTheory.Functor C D} →
        {R : CategoryTheory.Functor Dᵒᵖ RingCat} →
          {S : CategoryTheory.Functor Cᵒᵖ RingCat} →
            (φ : S ⟶ F.op.comp R) →
              (X : C) →
                ((PresheafOfModules.pushforward φ).comp
                      (CategoryTheory.coyoneda.obj
                        (Opposite.op ((PresheafOfModules.free S).obj (CategoryTheory.yoneda.obj X))))).CorepresentableBy
                  ((PresheafOfModules.free R).obj (CategoryTheory.yoneda.obj (F.obj X)))
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.measure_spanningSets_lt_top : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ] (i : ℕ),
  μ (MeasureTheory.spanningSets μ i) < ⊤
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.Adjunction.comp_unit : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b c : B} {f₁ : a ⟶ b} {g₁ : b ⟶ a} {f₂ : b ⟶ c} {g₂ : c ⟶ b}
  (adj₁ : CategoryTheory.Bicategory.Adjunction f₁ g₁) (adj₂ : CategoryTheory.Bicategory.Adjunction f₂ g₂),
  (adj₁.comp adj₂).unit = adj₁.compUnit adj₂
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.liminf_mul_le : ∀ {ι : Type u_4} {f : Filter ι} {u v : ι → ENNReal},
  Filter.limsup u f ≠ 0 ∨ Filter.liminf v f ≠ ⊤ →
    Filter.limsup u f ≠ ⊤ ∨ Filter.liminf v f ≠ 0 → Filter.liminf (u * v) f ≤ Filter.limsup u f * Filter.liminf v f
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.iteratedDeriv_derivWeierstrassPExcept_self : ∀ (L : PeriodPair) (l : ℂ) {n : ℕ},
  iteratedDeriv n (L.derivWeierstrassPExcept l) l = ↑(n + 2).factorial * L.sumInvPow l (n + 3)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_keysArray : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.LawfulEqOrd α]
  [Std.TransOrd α] {k : α}, t.WF → (k ∈ t.keysArray ↔ k ∈ t)
-- Mathlib.CategoryTheory.FinCategory.AsType
CategoryTheory.FinCategory.objAsTypeToAsType_obj : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : CategoryTheory.SmallCategory α] [inst_2 : CategoryTheory.FinCategory α]
  (a : CategoryTheory.FinCategory.ObjAsType α), (CategoryTheory.FinCategory.objAsTypeToAsType α).obj a = id a
-- Mathlib.Tactic.Convert
/-- `convert e`, where the term `e` is inferred to have type `t`, replaces the main goal `⊢ t'` with new
goals for proving the equality `t' = t` using congruence. The goals are created like `congr!` would.
Like `refine e`, any holes (`?_` or `?x`) in `e` that are not solved by unification are converted
into new goals, using the hole's name, if any, as the goal case name.
Like `congr!`, `convert` introduces variables while applying congruence rules. These can be
pattern-matched, like `rintro` would, using the `with` keyword.

See also `convert_to t`, where `t` specifies the expected type, instead of a proof term of type `t`.
In other words, `convert_to t` works like `convert (?_ : t)`. Both tactics use the same options.

* `convert! e` uses default transparency, rather than reducible, when solving side goals, and
  it tries to apply congruence even if the two expressions do not have the same head constant.
* `convert ← e` creates equality goals in the opposite direction (with the goal type on the right).
* `convert e using n`, where `n` is a numeral, controls the depth with which congruence is
  applied. For example, if the main goal is `⊢ Prime (n + n + 1)` and `e : Prime (2 * n + 1)`, then
  `convert e using 2` results in one goal, `⊢ n + n = 2 * n`, and `convert e using 3` (or more)
  results in two (impossible) goals `⊢ HAdd.hAdd = HMul.hMul` and `⊢ n = 2`.
  By default, the depth is unlimited.
* `convert e with x ⟨y₁, y₂⟩ (z₁ | z₂)` names or pattern-matches the variables introduced by
  congruence rules, like `rintro x ⟨y₁, y₂⟩ (z₁ | z₂)` would.
* `convert (config := cfg) e` uses the configuration options in `cfg` to control the congruence
  rules (see `Congr!.Config`).

Examples:

```lean
example {n : ℕ} (e : Prime (2 * n + 1)) :
    Prime (n + n + 1) := by
  convert e
  -- One goal: ⊢ n + n = 2 * n
  ring

-- `convert` can fail where `exact` succeeds.
def p (n : ℕ) := True
example (h : p 0) : p 1 := by
  fail_if_success
    convert h -- fails, left-over goal 1 = 0
    done
  exact h -- succeeds

-- `convert with` names introduced variables.
example (p q : Nat → Prop) (h : ∀ ε > 0, p ε) :
    ∀ ε > 0, q ε := by
  convert h with ε hε
  -- Goal now looks like:
  -- hε : ε > 0
  -- ⊢ q ε ↔ p ε
  sorry
```
 -/
Mathlib.Tactic.convert : Lean.ParserDescr
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.insert : {α : Type u} →
  {β : α → Type v} →
    [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → (a : α) → β a → Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.RingTheory.Ideal.Operations
Ideal.IsPrime.notMem_of_isCoprime_of_mem : ∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R} [I.IsPrime] {x y : R}, IsCoprime x y → x ∈ I → y ∉ I
-- Mathlib.Computability.TuringMachine.Config
/-- If we are not done (in `Cfg.halt` state), then we must be still stuck on a continuation, so
this main loop calls `stepRet` with the new continuation. The overall `step` function transitions
from one `Cfg` to another, only halting at the `Cfg.halt` state.  -/
Turing.ToPartrec.step : Turing.ToPartrec.Cfg → Option Turing.ToPartrec.Cfg
-- Mathlib.CategoryTheory.Groupoid.Grpd.Basic
/-- Converts identity in the category of groupoids to the functor identity  -/
CategoryTheory.Grpd.id_eq_id : ∀ {C : CategoryTheory.Grpd}, CategoryTheory.CategoryStruct.id C = CategoryTheory.Functor.id ↑C
-- Mathlib.Algebra.Free
AddMagma.FreeAddSemigroup.lift_comp_of : ∀ {α : Type u} [inst : Add α] {β : Type v} [inst_1 : AddSemigroup β] (f : α →ₙ+ β),
  (AddMagma.FreeAddSemigroup.lift f).comp AddMagma.FreeAddSemigroup.of = f
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
/-- The monoidal coherence theorem.  -/
CategoryTheory.FreeMonoidalCategory.subsingleton_hom : ∀ {C : Type u}, Quiver.IsThin (CategoryTheory.FreeMonoidalCategory C)
-- Lean.ScopedEnvExtension
/-- Modifies `delimitsLocal` flag to `false` on the top `depth` entries of the state stack,
to turn off delimiting of local entries across multiple implicit scope levels
(e.g. those introduced by compound `namespace A.B.C` expansions).
 -/
Lean.ScopedEnvExtension.setDelimitsLocal : {α β σ : Type} → Lean.ScopedEnvExtension α β σ → Lean.Environment → ℕ → Lean.Environment
-- Lean.Parser.Command
Lean.Parser.Command.printAxioms.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
/-- The algebra version of `AddMonoidAlgebra.addMonoidAlgebraEquivDirectSum`.  -/
addMonoidAlgebraAlgEquivDirectSum : {ι : Type u_1} →
  {R : Type u_2} →
    {A : Type u_4} →
      [inst : DecidableEq ι] →
        [inst_1 : AddMonoid ι] →
          [inst_2 : CommSemiring R] →
            [inst_3 : Semiring A] →
              [inst_4 : Algebra R A] → [(m : A) → Decidable (m ≠ 0)] → AddMonoidAlgebra A ι ≃ₐ[R] DirectSum ι fun x => A