mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.ENNReal.Inv
/-- Left multiplication by a nonzero finite `a` as an order isomorphism.  -/
ENNReal.mulLeftOrderIso : (a : ENNReal) → IsUnit a → ENNReal ≃o ENNReal
-- Mathlib.Algebra.Group.Defs
MulOne.toMul : {M : Type u_2} → [self : MulOne M] → Mul M
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.FinalizeContext.replaceIndFVars : Lean.Elab.Command.FinalizeContext✝ → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Condensed.Discrete.Colimit
Condensed.instFinalOppositeDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceCostructuredArrowFintypeCatProfiniteOpToProfiniteOpPtAsLimitConeFunctorOp : ∀ {S : Profinite}, (Profinite.Extend.functorOp S.asLimitCone).Final
-- Mathlib.Algebra.Squarefree.Basic
Prime.squarefree : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [IsCancelMulZero R] {x : R}, Prime x → Squarefree x
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Sentence.Realize.eq_1 : ∀ {L : FirstOrder.Language} (M : Type w) [inst : L.Structure M] (φ : L.Sentence),
  M ⊨ φ = FirstOrder.Language.Formula.Realize φ default
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.isCompact_basicOpen : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens},
  IsCompact ↑U → ∀ (f : ↑(X.presheaf.obj (Opposite.op U))), IsCompact ↑(X.basicOpen f)
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- `val_v(I) = 0` for all but finitely many maximal ideals of `R`.  -/
FractionalIdeal.finite_factors : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (I : FractionalIdeal (nonZeroDivisors R) K),
  ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite, FractionalIdeal.count K v I = 0
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- The inverse `AffineIsometryEquiv`.  -/
AffineIsometryEquiv.symm : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_5} →
      {P : Type u_10} →
        {P₂ : Type u_11} →
          [inst : NormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup V] →
              [inst_2 : NormedSpace 𝕜 V] →
                [inst_3 : PseudoMetricSpace P] →
                  [inst_4 : NormedAddTorsor V P] →
                    [inst_5 : SeminormedAddCommGroup V₂] →
                      [inst_6 : NormedSpace 𝕜 V₂] →
                        [inst_7 : PseudoMetricSpace P₂] → [inst_8 : NormedAddTorsor V₂ P₂] → (P ≃ᵃⁱ[𝕜] P₂) → P₂ ≃ᵃⁱ[𝕜] P
-- Mathlib.Algebra.Lie.Weights.Cartan
/-- Given a root `α` relative to a Cartan subalgebra `H`, this is the span of all products of
an element of the `α` root space and an element of the `-α` root space. Informally it is often
denoted `⁅H(α), H(-α)⁆`.

If the Killing form is non-degenerate and the coefficients are a perfect field, this space is
one-dimensional. See `LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton` and
`LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton'`.

Note that the name "coroot space" is not standard as this space does not seem to have a name in the
informal literature.  -/
LieAlgebra.corootSpace : {R : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          {H : LieSubalgebra R L} →
            [LieRing.IsNilpotent ↥H] → [H.IsCartanSubalgebra] → [IsNoetherian R L] → (↥H → R) → LieIdeal R ↥H
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
CategoryTheory.Limits.weakEqualizer.condition : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasWeakEqualizer f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakEqualizer.ι f g) f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakEqualizer.ι f g) g
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_sub_Ioi : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => a - x) ⁻¹' Set.Ioi b = Set.Iio (a - b)
-- Mathlib.NumberTheory.NumberField.FractionalIdeal
/-- A `ℤ`-basis of a fractional ideal.  -/
NumberField.fractionalIdealBasis : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      (I : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K) →
        Module.Basis (Module.Free.ChooseBasisIndex ℤ ↥↑I) ℤ ↥↑I
-- Mathlib.Geometry.Manifold.Submersion
isOpen_isSubmersionAtOfComplement : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N},
  IsOpen {x | Manifold.IsSubmersionAtOfComplement F I J n f x}
-- Lean.Server.Rpc.Basic
_private.Lean.Server.Rpc.Basic.0.Lean.Server.WithRpcRef.mk'.inj : ∀ {α : Type u} {val : α} {id : USize} {val_1 : α} {id_1 : USize},
  { val := val, id := id } = { val := val_1, id := id_1 } → val = val_1 ∧ id = id_1
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- Auxiliary lemma for `biproduct.uniqueUpToIso`.  -/
CategoryTheory.Limits.biproduct.conePointUniqueUpToIso_inv : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  {b : CategoryTheory.Limits.Bicone f} (hb : b.IsBilimit),
  (hb.isLimit.conePointUniqueUpToIso (CategoryTheory.Limits.biproduct.isLimit f)).inv =
    CategoryTheory.Limits.biproduct.desc b.ι
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α},
        Std.DHashMap.Internal.Raw₀.Const.get! (m₁.diff m₂) k =
          if m₂.contains k = true then default else Std.DHashMap.Internal.Raw₀.Const.get! m₁ k
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], IsIntegralClosure (CyclotomicRing p ℤ ℚ) ℤ (CyclotomicField p ℚ)
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- Dual to `Monad.HasCoequalizerOfIsSplitPair`.  -/
CategoryTheory.Comonad.HasEqualizerOfIsCosplitPair : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] → CategoryTheory.Functor C D → Prop
-- Init.Data.SInt.Lemmas
Int16.toInt64_mod : ∀ (a b : Int16), (a % b).toInt64 = a.toInt64 % b.toInt64
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.re_div : ∀ {K : Type u_1} [inst : Field K] {a b : K} (w z : QuadraticAlgebra K a b),
  (w / z).re =
    w.re * ((QuadraticAlgebra.norm z)⁻¹ * (z.re + b * z.im)) + -(a * w.im * ((QuadraticAlgebra.norm z)⁻¹ * z.im))
-- Init.Data.Float.Model.Unpacked.Pack.Basic
/-- Unpacks the given float according to the given specification.

The resulting float may be assumed to be correctly rounded for the given specification.
 -/
Float.Model.UnpackedFloat.unpack : (spec : Float.Model.Format) → BitVec spec.numBits → Float.Model.UnpackedFloat
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The left map in the oplax right unitality square.
 -/
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.leftMapᵣ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          (F : CategoryTheory.Functor C D) → F ⟶ F.comp (CategoryTheory.MonoidalCategory.tensorUnitRight D)
-- Mathlib.Data.Finsupp.SMul
Finsupp.faithfulSMul : ∀ {α : Type u_1} {M : Type u_3} {R : Type u_6} [Nonempty α] [inst : Zero M] [inst_1 : SMulZeroClass R M]
  [FaithfulSMul R M], FaithfulSMul R (α →₀ M)
-- Lean.Meta.Basic
Lean.Meta.Cache.inferType : Lean.Meta.Cache → Lean.Meta.InferTypeCache
-- Mathlib.Tactic.DefEqTransformations
/-- Given an expression that's either a native projection or a registered projection
function, gives (1) the name of the structure type, (2) the index of the projection, and
(3) the object being projected.  -/
Mathlib.Tactic.getProjectedExpr : Lean.Expr → Lean.MetaM (Option (Lean.Name × ℕ × Lean.Expr))
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- **Alias** of the forward direction of `hasMFDerivWithinAt_insert`. -/
HasMFDerivWithinAt.of_insert : ∀ {𝕜 : 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)} {y : M}, HasMFDerivAt[insert y s] f x f' → HasMFDerivAt[s] f x f'
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- The linear span of the monomials `mFourier n` is dense in `C(UnitAddTorus d, ℂ)`.  -/
UnitAddTorus.span_mFourier_closure_eq_top : ∀ {d : Type u_1} [inst : Fintype d], (Submodule.span ℂ (Set.range UnitAddTorus.mFourier)).topologicalClosure = ⊤
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_insertMany_list : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (∀ a ∈ m, (List.map Prod.fst l).contains a = false) → (m.insertMany l).size = m.size + l.length
-- Mathlib.LinearAlgebra.TensorProduct.Prod
TensorProduct.prodRight_tmul : ∀ (R : Type u_1) (S : Type u_2) (M₁ : Type u_3) (M₂ : Type u_4) (M₃ : Type u_5) [inst : CommSemiring R]
  [inst_1 : Semiring S] [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid M₃]
  [inst_5 : Algebra R S] [inst_6 : Module R M₁] [inst_7 : Module S M₁] [inst_8 : IsScalarTower R S M₁]
  [inst_9 : Module R M₂] [inst_10 : Module R M₃] (m₁ : M₁) (m : M₂ × M₃),
  (TensorProduct.prodRight R S M₁ M₂ M₃) (m₁ ⊗ₜ[R] m) = (m₁ ⊗ₜ[R] m.1, m₁ ⊗ₜ[R] m.2)
-- Init.Data.Sum.Lemmas
Sum.eq_left_getLeft_of_isLeft : ∀ {α : Type u_1} {β : Type u_2} {x : α ⊕ β} (h : x.isLeft = true), x = Sum.inl (x.getLeft h)
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.fixed_eq_iInter_fixedBy : ∀ (M : Type u_1) (α : Type u_3) [inst : AddMonoid M] [inst_1 : AddAction M α],
  AddAction.fixedPoints M α = ⋂ m, AddAction.fixedBy α m
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If `s` is a limit binary fan over `X` and `Y`, then every pair of morphisms `f : W ⟶ X` and
`g : W ⟶ Y` induces a morphism `l : W ⟶ s.pt` satisfying `l ≫ s.fst = f` and `l ≫ s.snd = g`.
 -/
CategoryTheory.Limits.BinaryFan.IsLimit.lift' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y : C} →
      {s : CategoryTheory.Limits.BinaryFan X Y} →
        CategoryTheory.Limits.IsLimit s →
          (f : W ⟶ X) →
            (g : W ⟶ Y) →
              { l // CategoryTheory.CategoryStruct.comp l s.fst = f ∧ CategoryTheory.CategoryStruct.comp l s.snd = g }
-- Init.Data.UInt.Lemmas
USize.ofNatLT_toNat : ∀ (n : USize), USize.ofNatLT n.toNat ⋯ = n
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instIsTorsionFree : ∀ {R : Type u_1} {S : Type u_2} {a b : R} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Module S R]
  [Module.IsTorsionFree S R], Module.IsTorsionFree S (QuadraticAlgebra R a b)
-- Lean.Exception
/-- Throw an error exception for the given kernel exception.
 -/
Lean.throwKernelException : {m : Type → Type} → {α : Type} → [Monad m] → [Lean.MonadError m] → [Lean.MonadOptions m] → Lean.Kernel.Exception → m α
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.inv_preimage : ∀ {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y) (U : X.Opens),
  (TopologicalSpace.Opens.map e.inv.base).obj U = (AlgebraicGeometry.Scheme.Hom.opensFunctor e.hom).obj U
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk_prodMk₀ : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : ι → Type u_8}
  {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ)) →
      ∀ (i j k l : ι),
        i ≠ k →
          i ≠ l →
            j ≠ k → j ≠ l → ProbabilityTheory.Kernel.IndepFun (fun a => (f i a, f j a)) (fun a => (f k a, f l a)) κ μ
-- Mathlib.RingTheory.Polynomial.IrreducibleRing
/-- A polynomial over an irreducible ring `R` is irreducible if it is monic and irreducible after
mapping into an integral domain `S` (https://math.stackexchange.com/a/4843432/235999).
A generalization to `Polynomial.Monic.irreducible_of_irreducible_map`.  -/
Polynomial.Monic.irreducible_of_irreducible_map_of_isPrime_nilradical : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [(nilradical R).IsPrime] [inst_2 : CommRing S] [IsDomain S]
  (φ : R →+* S) (f : Polynomial R), f.Monic → Irreducible (Polynomial.map φ f) → Irreducible f
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.lTensor_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] (f₁ : E →L[𝕜] F) (f₂ : H →L[𝕜] E),
  ContinuousLinearMap.lTensor G (f₁ ∘SL f₂) = ContinuousLinearMap.lTensor G f₁ ∘SL ContinuousLinearMap.lTensor G f₂
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Algebra.algebraMap_intTrace_fractionRing : ∀ {A : Type u_1} {B : Type u_6} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain A]
  [inst_4 : IsIntegrallyClosed A] [inst_5 : IsDomain B] [inst_6 : IsIntegrallyClosed B] [inst_7 : Module.Finite A B]
  [inst_8 : Module.IsTorsionFree A B] (x : B),
  (algebraMap A (FractionRing A)) ((Algebra.intTrace A B) x) =
    (Algebra.trace (FractionRing A) (FractionRing B)) ((algebraMap B (FractionRing B)) x)
-- Mathlib.Logic.Function.Basic
Function.Surjective.piMap : ∀ {ι : Sort u_1} {α : ι → Sort u_2} {β : ι → Sort u_3} {f : (i : ι) → α i → β i},
  (∀ (i : ι), Function.Surjective (f i)) → Function.Surjective (Pi.map f)
-- Lean.Util.PPExt
Lean.FormatWithInfos.infos : Lean.FormatWithInfos → Lean.PrettyPrinter.InfoPerPos
-- Mathlib.Algebra.Module.Equiv.Defs
SemilinearEquivClass.mk : ∀ {F : Type u_14} {R : outParam (Type u_15)} {S : outParam (Type u_16)} [inst : Semiring R] [inst_1 : Semiring S]
  {σ : outParam (R →+* S)} {σ' : outParam (S →+* R)} [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ]
  {M : outParam (Type u_17)} {M₂ : outParam (Type u_18)} [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M] [inst_7 : Module S M₂] [inst_8 : EquivLike F M M₂] [toAddEquivClass : AddEquivClass F M M₂],
  (∀ (f : F) (r : R) (x : M), f (r • x) = σ r • f x) → SemilinearEquivClass F σ M M₂
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.TensorBimod.whiskerLeft_π_actLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T)
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R.X
        (CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight Q.X)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X S.X Q.X).hom
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q.actLeft))))
      (Bimod.TensorBimod.actLeft P Q) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R.X P.X Q.X).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actLeft Q.X)
        (CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight Q.X)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X S.X Q.X).hom
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q.actLeft))))
-- Mathlib.CategoryTheory.Linear.Yoneda
CategoryTheory.faithful_linearCoyoneda : ∀ (R : Type w) [inst : Ring R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C],
  (CategoryTheory.linearCoyoneda R C).Faithful
-- Mathlib.Algebra.GroupWithZero.Units.Basic
div_mul_div_cancel₀' : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] {a : G₀}, a ≠ 0 → ∀ (b c : G₀), a / b * (c / a) = c / b
-- Mathlib.Order.Filter.Lift
Filter.lift_top : ∀ {α : Type u_1} {β : Type u_2} (g : Set α → Filter β), ⊤.lift g = g Set.univ
-- Lean.Meta.PProdN
/-- Packs multiple type-forming lambda expressions taking the same parameters using `PProd`.

The parameter `type` is the common type of the these expressions

For example
```
packLambdas (Nat → Sort u) #[(fun (n : Nat) => Nat), (fun (n : Nat) => Fin n -> Fin n )]
```
will return
```
fun (n : Nat) => (Nat ×' (Fin n → Fin n))
```

It is the identity if `es.size = 1`.

It returns a dummy motive `(xs : ) → PUnit` or `(xs : … ) → True` if no expressions are given.
(this is the reason we need the expected type in the `type` parameter).

 -/
Lean.Meta.PProdN.packLambdas : Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Order.CompleteLattice.Basic
biInf_mono : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {f : ι → α} {p q : ι → Prop},
  (∀ (i : ι), p i → q i) → ⨅ i, ⨅ (_ : q i), f i ≤ ⨅ i, ⨅ (_ : p i), f i
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.ext_iff_isBase : ∀ {α : Type u_1} {M₁ M₂ : Matroid α}, M₁ = M₂ ↔ M₁.E = M₂.E ∧ ∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.foldlM_eq_foldlM_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m] {f : δ → α → m δ} {init : δ},
  Std.ExtTreeSet.foldlM f init t = List.foldlM f init t.toList
-- Lean.Data.Lsp.Workspace
Lean.Lsp.instToJsonDidChangeWatchedFilesParams : Lean.ToJson Lean.Lsp.DidChangeWatchedFilesParams
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β] [inst_4 : SizeOf α] [inst_5 : SizeOf β] (toRingHom : α →+* β)
  (monotone' : Monotone (↑↑toRingHom).toFun),
  sizeOf { toRingHom := toRingHom, monotone' := monotone' } = 1 + sizeOf toRingHom
-- Mathlib.FieldTheory.SeparableDegree
Polynomial.natSepDegree_C_mul_X_sub_C_pow : ∀ {F : Type u} [inst : Field F] {x y : F} {n : ℕ},
  x ≠ 0 → (Polynomial.C x * (Polynomial.X - Polynomial.C y) ^ n).natSepDegree = if n = 0 then 0 else 1
-- Init.Grind.Config
/-- A `grind` configuration that only uses `linarith`.
 -/
Lean.Grind.LinarithConfig : Type
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trCont.match_1.eq_1 : ∀ (motive : Turing.ToPartrec.Cont → Sort u_1) (h_1 : Unit → motive Turing.ToPartrec.Cont.halt)
  (h_2 :
    (c : Turing.ToPartrec.Code) →
      (a : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₁ c a k))
  (h_3 : (a : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₂ a k))
  (h_4 : (c : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.comp c k))
  (h_5 : (c : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.fix c k)),
  (match Turing.ToPartrec.Cont.halt with
    | Turing.ToPartrec.Cont.halt => h_1 ()
    | Turing.ToPartrec.Cont.cons₁ c a k => h_2 c a k
    | Turing.ToPartrec.Cont.cons₂ a k => h_3 a k
    | Turing.ToPartrec.Cont.comp c k => h_4 c k
    | Turing.ToPartrec.Cont.fix c k => h_5 c k) =
    h_1 ()
-- Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
/-- The isomorphism given by the very definition of `singleFunctors C`.  -/
HomotopyCategory.singleFunctorsPostcompQuotientIso : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        HomotopyCategory.singleFunctors C ≅
          (CochainComplex.singleFunctors C).postcomp (HomotopyCategory.quotient C (ComplexShape.up ℤ))
-- Mathlib.CategoryTheory.EssentialImage
CategoryTheory.Functor.toEssImageCompι_inv_app : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C), F.toEssImageCompι.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] [inst_2 : Inhabited α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (t.insertMany l).getKey! k = t.getKey! k
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.fieldEquivOfAlgEquiv_trans : ∀ {A : Type u_8} {B : Type u_9} {C : Type u_10} {D : Type u_11} [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : CommRing C] [inst_3 : CommRing D] [inst_4 : Algebra A B] [inst_5 : Algebra A C] [inst_6 : Algebra A D]
  (FA : Type u_12) (FB : Type u_13) (FC : Type u_14) (FD : Type u_15) [inst_7 : Field FA] [inst_8 : Field FB]
  [inst_9 : Field FC] [inst_10 : Field FD] [inst_11 : Algebra A FA] [inst_12 : Algebra B FB] [inst_13 : Algebra C FC]
  [inst_14 : Algebra D FD] [inst_15 : IsFractionRing A FA] [inst_16 : IsFractionRing B FB]
  [inst_17 : IsFractionRing C FC] [inst_18 : IsFractionRing D FD] [inst_19 : Algebra A FB]
  [inst_20 : IsScalarTower A B FB] [inst_21 : Algebra A FC] [inst_22 : IsScalarTower A C FC] [inst_23 : Algebra A FD]
  [inst_24 : IsScalarTower A D FD] [inst_25 : Algebra FA FB] [inst_26 : IsScalarTower A FA FB] [inst_27 : Algebra FA FC]
  [inst_28 : IsScalarTower A FA FC] [inst_29 : Algebra FA FD] [inst_30 : IsScalarTower A FA FD] (f : B ≃ₐ[A] C)
  (g : C ≃ₐ[A] D),
  IsFractionRing.fieldEquivOfAlgEquiv FA FB FD (f.trans g) =
    (IsFractionRing.fieldEquivOfAlgEquiv FA FB FC f).trans (IsFractionRing.fieldEquivOfAlgEquiv FA FC FD g)
-- Mathlib.Tactic.Bound.Attribute
/-- Map a theorem decl to a score (0 means `norm apply`, `0 <` means `safe apply`)  -/
Mathlib.Tactic.Bound.declPriority : Lean.Name → Lean.MetaM ℕ
-- Lean.Exception
Lean.MonadError.mk : {m : Type → Type} →
  [toMonadExceptOf : MonadExceptOf Lean.Exception m] →
    [toMonadRef : Lean.MonadRef m] → [toAddErrorMessageContext : Lean.AddErrorMessageContext m] → Lean.MonadError m
-- Init.Data.UInt.Bitwise
USize.shiftLeft_or : ∀ {a b c : USize}, (a ||| b) <<< c = a <<< c ||| b <<< c
-- Mathlib.RingTheory.WittVector.Basic
WittVector.mapFun.nsmul : ∀ {p : ℕ} {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Fact (Nat.Prime p)]
  (f : R →+* S) (n : ℕ) (x : WittVector p R), WittVector.mapFun (⇑f) (n • x) = n • WittVector.mapFun (⇑f) x