mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Linear.LinearFunctor
CategoryTheory.Functor.fullSubcategoryInclusionLinear : ∀ (R : Type u_1) [inst : Semiring R] {C : Type u_4} [inst_1 : CategoryTheory.Category.{v_3, u_4} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] (Z : CategoryTheory.ObjectProperty C),
  CategoryTheory.Functor.Linear R Z.ι
-- Lean.Data.JsonRpc
Lean.JsonRpc.instToJsonMessageDirection.toJson : Lean.JsonRpc.MessageDirection → Lean.Json
-- Mathlib.AlgebraicTopology.CechNerve
/-- The Čech nerve construction, as a functor from `Arrow C`.  -/
CategoryTheory.SimplicialObject.cechNerve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [∀ (n : ℕ) (f : CategoryTheory.Arrow C),
          CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] →
      CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.SimplicialObject C)
-- Mathlib.Order.Filter.ZeroAndBoundedAtFilter
Filter.BoundedAtFilter.prod : ∀ {α : Type u_2} {β : Type u_3} {ι : Type} (s : Finset ι) [inst : SeminormedCommRing β] {l : Filter α} {f : ι → α → β},
  (∀ i ∈ s, l.BoundedAtFilter (f i)) → l.BoundedAtFilter (∏ i ∈ s, f i)
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.support_nonempty_iff : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {x : HahnSeries Γ R},
  x.support.Nonempty ↔ x ≠ 0
-- Mathlib.Topology.EMetricSpace.Defs
/-- **Alias** of `Metric.pos_of_mem_eball`. -/
EMetric.pos_of_mem_ball : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {ε : ENNReal}, y ∈ Metric.eball x ε → 0 < ε
-- Lean.DocString.Types
Lean.Doc.MathMode.display.sizeOf_spec : sizeOf Lean.Doc.MathMode.display = 1
-- Mathlib.Order.Interval.Set.SurjOn
surjOn_Ici_of_monotone_surjective : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PartialOrder β] {f : α → β},
  Monotone f → Function.Surjective f → ∀ (a : α), Set.SurjOn f (Set.Ici a) (Set.Ici (f a))
-- Init.Data.Vector.Attach
Vector.reverse_pmap : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {P : α → Prop} {f : (a : α) → P a → β} {xs : Vector α n} (H : ∀ a ∈ xs, P a),
  (Vector.pmap f xs H).reverse = Vector.pmap f xs.reverse ⋯
-- Mathlib.Order.Filter.Basic
Filter.EventuallyLE.inter : ∀ {α : Type u} {s t s' t' : Set α} {l : Filter α}, s ≤ᶠ[l] t → s' ≤ᶠ[l] t' → s ∩ s' ≤ᶠ[l] t ∩ t'
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
/-- Given a box `J ∈ π.biUnion πi`, returns the box `J' ∈ π` such that `J ∈ πi J'`.
For `J ∉ π.biUnion πi`, returns `I`.  -/
BoxIntegral.Prepartition.biUnionIndex : {ι : Type u_1} →
  {I : BoxIntegral.Box ι} →
    BoxIntegral.Prepartition I →
      ((J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) → BoxIntegral.Box ι → BoxIntegral.Box ι
-- Mathlib.Topology.UniformSpace.UniformEmbedding
CompleteSpace.sum : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] [CompleteSpace α] [CompleteSpace β],
  CompleteSpace (α ⊕ β)
-- Mathlib.Algebra.Polynomial.Degree.Support
Polynomial.le_natDegree_of_mem_supp : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, ∀ a ∈ p.support, a ≤ p.natDegree
-- Lean.Parser.Attr
Lean.Parser.Attr.recursor : Lean.Parser.Parser
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addSemigroup : {I : Type u} → {f : I → Type v₁} → [(i : I) → AddSemigroup (f i)] → AddSemigroup ((i : I) → f i)
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.instSMul_1 : {S : Type u_2} →
  [inst : Semiring S] →
    [inst_1 : PartialOrder S] →
      {R : Type u_3} →
        {T : Type u_4} → [inst_2 : Semiring R] → (v : AbsoluteValue R S) → [SMul T R] → SMul T (WithAbs v)
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.instNatCast : {q : ℕ} → NatCast (LucasLehmer.X q)
-- Lean.Elab.InfoTree.Types
Lean.Elab.instInhabitedTermInfo.default : Lean.Elab.TermInfo
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.insertMany_list : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : t₁.WF)
  (h₂ : t₂.WF), t₁.Equiv t₂ → ∀ {l : List ((a : α) × β a)}, (↑(t₁.insertMany l ⋯)).Equiv ↑(t₂.insertMany l ⋯)
-- Mathlib.Algebra.Category.HopfAlgCat.Monoidal
HopfAlgCat.instMonoidalCategory : (R : Type u) → [inst : CommRing R] → CategoryTheory.MonoidalCategory (HopfAlgCat R)
-- Mathlib.RingTheory.MvPowerSeries.GaussNorm
MvPowerSeries.gaussNorm_mul_eq_mul : ∀ {R : Type u_1} {σ : Type u_2} (v : R → ℝ) (c : σ → ℝ) [inst : Ring R] [inst_1 : DecidableEq σ]
  (f g : MvPowerSeries σ R),
  MvPowerSeries.HasGaussNorm v c f →
    MvPowerSeries.HasGaussNorm v c g →
      MvPowerSeries.HasGaussNorm v c (f * g) →
        (∀ (a : R), v a ≥ 0) →
          v 0 = 0 →
            IsNonarchimedean v →
              (∀ (a b : R), v (a * b) = v a * v b) →
                (∀ (a : R), v (-a) = v a) →
                  (∀ (x : R), v x = 0 → x = 0) →
                    (∀ (i : σ), 0 < c i) →
                      (∃ i j,
                          MvPowerSeries.AchievesGaussNorm v c f i ∧
                            MvPowerSeries.AchievesGaussNorm v c g j ∧
                              ∀ p ∈ Finset.HasAntidiagonal.antidiagonal (i + j),
                                p ≠ (i, j) →
                                  v ((MvPowerSeries.coeff p.1) f * (MvPowerSeries.coeff p.2) g) <
                                    v ((MvPowerSeries.coeff i) f) * v ((MvPowerSeries.coeff j) g)) →
                        MvPowerSeries.gaussNorm v c (f * g) =
                          MvPowerSeries.gaussNorm v c f * MvPowerSeries.gaussNorm v c g
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- A function `f : G → A` satisfies the 1-cocycle condition if
`f(gh) = g • f(h) + f(g)` for all `g, h : G`.  -/
groupCohomology.IsCocycle₁ : {G : Type u_1} → {A : Type u_2} → [Mul G] → [AddCommGroup A] → [SMul G A] → (G → A) → Prop
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.instIteratorLoop.loop : {α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [inst_1 : LE α] →
      [DecidableLE α] →
        [Std.PRange.LawfulUpwardEnumerable α] →
          [Std.PRange.LawfulUpwardEnumerableLE α] →
            {n : Type u → Type w} →
              [Monad n] →
                (γ : Type u) →
                  (Pl : α → γ → ForInStep γ → Prop) →
                    (LargeEnough : α → Prop) →
                      (∀ (a b : α), a ≤ b → LargeEnough a → LargeEnough b) →
                        (upperBound : α) →
                          γ →
                            (next : α) →
                              LargeEnough next →
                                ((out : α) → LargeEnough out → out ≤ upperBound → (c : γ) → n (Subtype (Pl out c))) →
                                  n γ
-- Mathlib.Analysis.Calculus.FDeriv.Basic
fderivWithin_zero_of_notMem_closure : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s : Set E}, x ∉ closure s → fderivWithin 𝕜 f s x = 0
-- Mathlib.Data.Set.Restrict
Set.MapsTo.restrict.congr_simp : ∀ {α : Type u} {β : Type v} (f f_1 : α → β) (e_f : f = f_1) (s : Set α) (t : Set β) (h : Set.MapsTo f s t) (a a_1 : ↑s),
  a = a_1 → Set.MapsTo.restrict f s t h a = Set.MapsTo.restrict f_1 s t ⋯ a_1
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.constVSub_apply : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁] [inst_5 : TopologicalSpace V₁]
  [inst_6 : IsTopologicalAddTorsor P₁] (p x : P₁), (ContinuousAffineEquiv.constVSub k p) x = p -ᵥ x
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.isClosed_iff' : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace X],
  Topology.IsInducing f → ∀ {s : Set X}, IsClosed s ↔ ∀ (x : X), f x ∈ closure (f '' s) → x ∈ s
-- Mathlib.Algebra.Category.Ring.Limits
/-- The category of rings has all limits.  -/
SemiRingCat.hasLimitsOfSize : ∀ [UnivLE.{v, u}], CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} SemiRingCat
-- Mathlib.LinearAlgebra.Projectivization.Subspace
/-- The span of the entire projective space is the top of the lattice of subspaces.  -/
Projectivization.Subspace.span_univ : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  Projectivization.Subspace.span Set.univ = ⊤
-- Lean.DocString.Syntax
/-- Boolean flag, turned off  -/
Lean.Doc.Syntax.flag_off : Lean.ParserDescr
-- Mathlib.NumberTheory.MulChar.Lemmas
/-- There is always a character on `F` of order `#F-1` with values in a ring that has
a primitive `(#F-1)`th root of unity.  -/
MulChar.exists_mulChar_orderOf_eq_card_units : ∀ (F : Type u_1) [inst : Field F] [inst_1 : Fintype F] {R : Type u_2} [inst_2 : CommRing R] [inst_3 : DecidableEq F]
  {ζ : R}, IsPrimitiveRoot ζ (Fintype.card Fˣ) → ∃ χ, orderOf χ = Fintype.card Fˣ
-- Init.Data.String.Basic
String.Slice.sliceTo_append_sliceFrom : ∀ {s : String.Slice} {pos : s.Pos}, (s.sliceTo pos).copy ++ (s.sliceFrom pos).copy = s.copy
-- Mathlib.Order.CompleteBooleanAlgebra
CompletelyDistribLattice.toCompleteDistribLattice : {α : Type u} → [CompletelyDistribLattice α] → CompleteDistribLattice α
-- Mathlib.Algebra.Order.Interval.Basic
Interval.length_sub_le : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedAddMonoid α] (s t : Interval α),
  (s - t).length ≤ s.length + t.length
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.instHasDistribNeg : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] →
      {R : Type v} →
        [inst_2 : CommRing R] → [Fact (Even (Fintype.card n))] → HasDistribNeg (Matrix.SpecialLinearGroup n R)
-- Mathlib.Algebra.Module.Presentation.Cokernel
Module.Presentation.nonempty_cokernelData : ∀ {A : Type u} [inst : Ring A] {M₁ : Type v₁} {M₂ : Type v₂} [inst_1 : AddCommGroup M₁] [inst_2 : Module A M₁]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module A M₂] (pres₂ : Module.Presentation A M₂) (f : M₁ →ₗ[A] M₂) {ι : Type w₁}
  (g₁ : ι → M₁), Nonempty (pres₂.CokernelData f g₁)
-- Lean.Elab.Arg
Lean.Elab.Term.NamedArg.name : Lean.Elab.Term.NamedArg → Lean.Name
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.instIsCentralVAdd : ∀ {R : Type u_1} {M : Type u_3} {X : Type u_4} [inst : AddMonoid M] {S : AddSubmonoid M}
  [inst_1 : AddOreLocalization.AddOreSet S] [inst_2 : AddAction M X] [inst_3 : VAdd R X] [inst_4 : VAdd R M]
  [inst_5 : VAddAssocClass R M M] [inst_6 : VAddAssocClass R M X] [inst_7 : VAdd Rᵃᵒᵖ M] [inst_8 : VAdd Rᵃᵒᵖ X]
  [inst_9 : VAddAssocClass Rᵃᵒᵖ M M] [inst_10 : VAddAssocClass Rᵃᵒᵖ M X] [IsCentralVAdd R M],
  IsCentralVAdd R (AddOreLocalization S X)
-- Std.Data.DHashMap.Raw
/-- Tries to retrieve the mapping for the given key, panicking if no such mapping is present.  -/
Std.DHashMap.Raw.Const.get! : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → [Inhabited β] → (Std.DHashMap.Raw α fun x => β) → α → β
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.map_fst' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C}
  (g : F.obj a ⟶ Y) [inst_2 : F.Full], F.map (hf'.fst' g) = hf'.fst g
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_C : ∀ {R : Type u} {a : R} [inst : Semiring R] {k : ℕ}, 0 < k → (⇑Polynomial.derivative)^[k] (Polynomial.C a) = 0
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiffAt_prod_module_iff : ∀ {𝕜 : 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] {F₁ : Type u_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂] {x : M}
  {n : WithTop ℕ∞} (f : M → F₁ × F₂),
  ContMDiffAt I (modelWithCornersSelf 𝕜 (F₁ × F₂)) n f x ↔
    ContMDiffAt I (modelWithCornersSelf 𝕜 F₁) n (Prod.fst ∘ f) x ∧
      ContMDiffAt I (modelWithCornersSelf 𝕜 F₂) n (Prod.snd ∘ f) x
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.supported.eq_1 : ∀ (R : Type u_1) (S : Type u_2) {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  (s : Set M),
  MonoidAlgebra.supported R S s = Submodule.comap (↑(MonoidAlgebra.coeffLinearEquiv R)) (Finsupp.supported S R s)
-- Mathlib.Order.RelSeries
RelSeries.head_snoc : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (newLast : α) (rel : (p.last, newLast) ∈ r),
  (p.snoc newLast rel).head = p.head
-- Std.Time.Date.Unit.Year
Std.Time.Year.instReprEra.repr : Std.Time.Year.Era → ℕ → Std.Format
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- `Cofork.ofπ f pullback.condition` is a colimit cocone in `Cᵒᵖ` if and only if
`Fork.ofι f.unop pushout.condition` in `C` is a limit cone.  -/
CategoryTheory.Limits.Cofork.isColimitCoforkPushoutEquivIsColimitForkUnopPullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : Cᵒᵖ} →
      {f : X ⟶ Y} →
        [inst_1 : CategoryTheory.Limits.HasPullback f f] →
          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f ⋯) ≃
            CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f.unop ⋯)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_mono_measure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {q : ℝ} {μ ν : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] (f : α → ε),
  ν ≤ μ → 0 ≤ q → MeasureTheory.eLpNorm' f q ν ≤ MeasureTheory.eLpNorm' f q μ
-- Mathlib.RepresentationTheory.Basic
/-- Build a `Representation` from a `[Module k[G] M]`.

Note that the representation is built on `restrictScalars k k[G] M`,
rather than on `M` itself.
 -/
Representation.ofModule : {k : Type u_1} →
  {G : Type u_2} →
    [inst : CommSemiring k] →
      [inst_1 : Monoid G] →
        (M : Type u_4) →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Module (MonoidAlgebra k G) M] → Representation k G (RestrictScalars k (MonoidAlgebra k G) M)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.coinvariantsMk_comp_H0Iso_inv_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : groupHomology.H0 A ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsMk k G).app A)
      (CategoryTheory.CategoryStruct.comp (groupHomology.H0Iso A).inv h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.H0π A) h
-- Mathlib.Data.Set.Finite.Basic
/-- If a linear order does not contain any triple of elements `x < y < z`, then this type
is finite.  -/
Finite.of_forall_not_lt_lt : ∀ {α : Type u} [inst : LinearOrder α], (∀ ⦃x y z : α⦄, x < y → y < z → False) → Finite α
-- Mathlib.Order.DirSupClosed
/-- **Alias** of the reverse direction of `dirSupClosedOn_compl`. -/
DirSupInaccOn.compl : ∀ {α : Type u_1} {s : Set α} {D : Set (Set α)} [inst : Preorder α], DirSupInaccOn D s → DirSupClosedOn D sᶜ
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
/-- `G.FiveWheelLikeFree r k` means there is no `IsFiveWheelLike r k` structure in `G`.  -/
SimpleGraph.FiveWheelLikeFree : {α : Type u_1} → [DecidableEq α] → SimpleGraph α → ℕ → ℕ → Prop
-- Mathlib.Condensed.Light.Module
/-- The forgetful functor from light condensed `R`-modules to light condensed sets.  -/
LightCondensed.forget : (R : Type u) → [inst : Ring R] → CategoryTheory.Functor (LightCondMod R) LightCondSet
-- Mathlib.Data.Nat.Order.Lemmas
Nat.set_eq_univ : ∀ {S : Set ℕ}, S = Set.univ ↔ 0 ∈ S ∧ ∀ k ∈ S, k + 1 ∈ S
-- Mathlib.Algebra.Ring.Ext
NonAssocRing.toNonAssocSemiring_injective : ∀ {R : Type u}, Function.Injective (@NonAssocRing.toNonAssocSemiring R)
-- Init.Data.String.Basic
String.Slice.Pos.toCopy : {s : String.Slice} → s.Pos → s.copy.Pos
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- Suppose we have a monoidal equivalence `F : C ≌ D`, with `D` monoidal closed. We can pull the
monoidal closed instance back along the equivalence. For `X, Y, Z : C`, this lemma describes the
resulting uncurrying map `Hom(Y, (X ⟶[C] Z)) → Hom(X ⊗ Y ⟶ Z)`. (`X ⟶[C] Z` is
defined to be `F⁻¹(F(X) ⟶[D] F(Z))`, so uncurrying in `C` is given by essentially conjugating
uncurrying in `D` by `F.`)  -/
CategoryTheory.MonoidalClosed.ofEquiv_uncurry_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.Monoidal]
  [inst_5 : F.IsEquivalence] [inst_6 : CategoryTheory.MonoidalClosed D] {X Y Z : C} (f : Y ⟶ X ⟹ Z),
  CategoryTheory.MonoidalClosed.uncurry f =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y)
      ((adj.toEquivalence.symm.toAdjunction.homEquiv
            ((F.comp (CategoryTheory.MonoidalCategory.tensorLeft (F.obj X))).obj Y) Z).symm
        (CategoryTheory.MonoidalClosed.uncurry
          ((adj.homEquiv Y (F.obj X ⟹ adj.toEquivalence.symm.inverse.obj Z)).symm f)))
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.oset.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (i : ℕ) (y : Lean.Compiler.LCNF.Arg pu)
  (k : Lean.Compiler.LCNF.Code pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_7) (fvarId_1 : Lean.FVarId)
  (i_1 : ℕ) (y_1 : Lean.Compiler.LCNF.Arg pu) (k_1 : Lean.Compiler.LCNF.Code pu)
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_7),
  (Lean.Compiler.LCNF.Code.oset fvarId i y k h = Lean.Compiler.LCNF.Code.oset fvarId_1 i_1 y_1 k_1 h_1) =
    (fvarId = fvarId_1 ∧ i = i_1 ∧ y = y_1 ∧ k = k_1)
-- Mathlib.Data.Finset.Disjoint
Finset.disjoint_right : ∀ {α : Type u_2} {s t : Finset α}, Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s
-- Batteries.Data.MLList.Basic
/-- Construct a singleton monadic lazy list from a single monadic value.  -/
MLList.singletonM : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → m α → MLList m α
-- Mathlib.Algebra.Ring.Subring.Defs
/-- A subring is closed under negation.  -/
Subring.neg_mem : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R) {x : R}, x ∈ s → -x ∈ s
-- Mathlib.Order.Partition.Finpartition
Finpartition.mk.congr_simp : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α} (parts parts_1 : Finset α) (e_parts : parts = parts_1)
  (supIndep : parts.SupIndep id) (sup_parts : parts.sup id = a) (bot_notMem : ⊥ ∉ parts),
  { parts := parts, supIndep := supIndep, sup_parts := sup_parts, bot_notMem := bot_notMem } =
    { parts := parts_1, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }
-- Lean.Environment
/-- `realizeValue _ key ..` adds a mapping from `(typeName key, key)` to a task of the realization
result (`RealizeValueResult` when called from `Lean.realizeValue`, `RealizeConstResult` from
`Environment.realizeConst`).
 -/
_private.Lean.Environment.0.Lean.RealizationContext.realizeMapRef : Lean.RealizationContext✝ → IO.Ref (Lean.NameMap NonScalar)
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inf_eq_inter' : ∀ {α : Type u_1} [inst : DecidableEq α], min = Inter.inter
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.integral_neg_eq_self : ∀ {G : Type u_4} {E : Type u_5} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  [inst_3 : AddGroup G] [MeasurableNeg G] (f : G → E) (μ : MeasureTheory.Measure G) [μ.IsNegInvariant],
  ∫ (x : G), f (-x) ∂μ = ∫ (x : G), f x ∂μ
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.copy.eq_1 : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) (s : Set G) (hs : s = ↑K),
  K.copy s hs = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
-- Mathlib.Algebra.Order.PUnit
PUnit.instLinearOrderedAddCommMonoidWithTop : LinearOrderedAddCommMonoidWithTop PUnit.{1}
-- Mathlib.Order.UpperLower.Relative
IsRelUpperSet.iInter₂ : ∀ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} {P : α → Prop} [inst : LE α] [Nonempty ι] [∀ (i : ι), Nonempty (κ i)]
  {f : (i : ι) → κ i → Set α}, (∀ (i : ι) (j : κ i), IsRelUpperSet (f i j) P) → IsRelUpperSet (⋂ i, ⋂ j, f i j) P
-- Init.Data.UInt.Bitwise
UInt32.not_eq_neg_sub : ∀ (a : UInt32), ~~~a = -a - 1
-- Init.RCases
Lean.Parser.Tactic.rintroPat.quot : Lean.ParserDescr
-- Init.Data.Format.Basic
Std.Format.text.inj : ∀ {a a_1 : String}, Std.Format.text a = Std.Format.text a_1 → a = a_1
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Limits.isBinaryBilimitOfPreserves.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {X Y : C}
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms]
  [inst_5 : CategoryTheory.Limits.PreservesBinaryBiproduct X Y F] {b : CategoryTheory.Limits.BinaryBicone X Y}
  (hb hb_1 : b.IsBilimit),
  hb = hb_1 →
    CategoryTheory.Limits.isBinaryBilimitOfPreserves F hb = CategoryTheory.Limits.isBinaryBilimitOfPreserves F hb_1
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas
aestronglyMeasurable_dirac : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : TopologicalSpace β] [MeasurableSingletonClass α] {a : α}
  {f : α → β}, MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.dirac a)
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresenter.present : ProofWidgets.ExprPresenter → Lean.Expr → Lean.MetaM ProofWidgets.Html
-- Mathlib.LinearAlgebra.Complex.Module
map_realPart : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  {B : Type u_2} {F : Type u_3} [inst_4 : AddCommGroup B] [inst_5 : Module ℂ B] [inst_6 : StarAddMonoid B]
  [inst_7 : StarModule ℂ B] [inst_8 : FunLike F A B] [StarHomClass F A B] [LinearMapClass F ℂ A B] (f : F) (x : A),
  f ↑(realPart x) = ↑(realPart (f x))
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
MeasureTheory.lpMeasToLpTrimLie_symm_toLp : ∀ {α : Type u_1} {F : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [one_le_p : Fact (1 ≤ p)] [inst_1 : NormedSpace ℝ F] (hm : m ≤ m0) (f : α → F)
  (hf : MeasureTheory.MemLp f p (μ.trim hm)),
  ↑((MeasureTheory.lpMeasToLpTrimLie F ℝ p μ hm).symm (MeasureTheory.MemLp.toLp f hf)) = MeasureTheory.MemLp.toLp f ⋯
-- Std.Data.Iterators.Combinators.Monadic.StepSize
Std.Iterators.Types.StepSizeIterator.mk.sizeOf_spec : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : SizeOf α] [inst_1 : (a : Type w) → SizeOf (m a)]
  [inst_2 : SizeOf β] (nextIdx n : ℕ) (inner : Std.IterM m β),
  sizeOf { nextIdx := nextIdx, n := n, inner := inner } = 1 + sizeOf nextIdx + sizeOf n + sizeOf inner
-- Mathlib.Data.Set.Lattice
Set.iUnion₂_comm : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} {κ : ι → Sort u_8} {κ' : ι' → Sort u_11}
  (s : (i : ι) → κ i → (i' : ι') → κ' i' → Set α), ⋃ i, ⋃ j, ⋃ i', ⋃ j', s i j i' j' = ⋃ i', ⋃ j', ⋃ i, ⋃ j, s i j i' j'
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ratUnits : {numVarsSucc : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula numVarsSucc →
    Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc))
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.Context.mk.inj : ∀ {config config_1 : Lean.Try.Config}, { config := config } = { config := config_1 } → config = config_1
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.trace_pos : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [inst_3 : Fintype n]
  [Nontrivial R] [IsOrderedCancelAddMonoid R] [Nonempty n] {A : Matrix n n R}, A.PosDef → 0 < A.trace