mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- A convenience function for `PreservesColimit`, which takes the functor as an explicit argument to
guide typeclass resolution.
 -/
CategoryTheory.Limits.isColimitOfPreserves : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              (F : CategoryTheory.Functor C D) →
                {c : CategoryTheory.Limits.Cocone K} →
                  CategoryTheory.Limits.IsColimit c →
                    [CategoryTheory.Limits.PreservesColimit K F] → CategoryTheory.Limits.IsColimit (F.mapCocone c)
-- Mathlib.Algebra.Order.Group.Synonym
toColex_eq_one : ∀ {α : Type u_1} [inst : One α] {a : α}, toColex a = 1 ↔ a = 1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.text : Lean.Lsp.CompletionItemKind
-- Mathlib.Analysis.Calculus.FDeriv.Add
Differentiable.sub_iff_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F},
  Differentiable 𝕜 g → (Differentiable 𝕜 (f - g) ↔ Differentiable 𝕜 f)
-- Lean.Meta.Tactic.Grind.Arith.Simproc
Lean.Meta.Grind.Arith.normIntCastNum : Lean.Meta.Simp.Simproc
-- Mathlib.RepresentationTheory.Induced
/-- Given a group hom `φ : G →* H`, `A : Rep k G` and `B : Rep k H`, this is the `k`-linear map
`(A ⊗ Res(φ)(B))_G ⟶ (Ind(φ)(A) ⊗ B))_H` sending `⟦a ⊗ₜ b⟧` to `⟦1 ⊗ₜ a⟧ ⊗ₜ b` for all
`a : A`, and `b : B`.  -/
Rep.coinvariantsTensorIndInv : {k : Type u} →
  [inst : CommRing k] →
    {G H : Type u} →
      [inst_1 : Group G] →
        [inst_2 : Group H] →
          (φ : G →* H) →
            (A : Rep.{u, u, u} k G) →
              (B : Rep.{u, u, u} k H) →
                ((Rep.coinvariantsTensor k G).obj A).obj (Rep.res φ B) ⟶
                  ((Rep.coinvariantsTensor k H).obj (Rep.ind φ A)).obj B
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- The natural monoid hom from a submonoid of monoid `M` to `M`.  -/
SubmonoidClass.subtype : {M : Type u_1} →
  {A : Type u_3} → [inst : MulOneClass M] → [inst_1 : SetLike A M] → [hA : SubmonoidClass A M] → (S' : A) → ↥S' →* M
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- Given `IsStrictSegal X`, a choice of inverse to `spine X m` for all
`m ≤ n + 1` determines an inhabitant of `StrictSegal X`.  -/
SSet.Truncated.StrictSegal.ofIsStrictSegal : {n : ℕ} → (X : SSet.Truncated (n + 1)) → [X.IsStrictSegal] → X.StrictSegal
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_eq_left : ∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ a → b ≤ a → a + b = a
-- Mathlib.Algebra.Ring.CharZero
/-- A characteristic zero domain is torsion-free.  -/
IsAddTorsionFree.of_isCancelMulZero_charZero : ∀ {R : Type u_2} [inst : Semiring R] [CharZero R] [IsCancelMulZero R], IsAddTorsionFree R
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.verticalStrip_mono_left : ∀ {A A' : ℝ}, A ≤ A' → ∀ (B : ℝ), UpperHalfPlane.verticalStrip A B ⊆ UpperHalfPlane.verticalStrip A' B
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instSMulCommClass_2 : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α], SMulCommClass α (CentroidHom α) α
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.one_apply : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (n : ℕ), ↑1 n = 1
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_add_natCast : ∀ {x : NNReal}, x ≠ 0 → ∀ (y : ℝ) (n : ℕ), x ^ (y + ↑n) = x ^ y * x ^ n
-- Mathlib.Data.Finset.Insert
Finset.coe_singleton : ∀ {α : Type u_1} (a : α), ↑{a} = {a}
-- Mathlib.Data.Multiset.Functor
Multiset.instLawfulFunctor : LawfulFunctor Multiset
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.id_apply : ∀ (A : ProfiniteGrp.{u}) (a : ↑A.toProfinite.toTop), (ProfiniteGrp.Hom.hom (CategoryTheory.CategoryStruct.id A)) a = a
-- Std.Data.Iterators.Lemmas.Producers.Empty
Std.Iter.forIn_empty : ∀ {m : Type u_1 → Type u_2} {β : Type u_3} {γ : Type u_1} [inst : Monad m] [LawfulMonad m] {init : γ}
  {f : β → γ → m (ForInStep γ)}, forIn (Std.Iter.empty β) init f = pure init
-- Lean.Meta.Instances
Lean.Meta.DefaultInstanceEntry.mk.inj : ∀ {className instanceName : Lean.Name} {priority : ℕ} {className_1 instanceName_1 : Lean.Name} {priority_1 : ℕ},
  { className := className, instanceName := instanceName, priority := priority } =
      { className := className_1, instanceName := instanceName_1, priority := priority_1 } →
    className = className_1 ∧ instanceName = instanceName_1 ∧ priority = priority_1
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.map_neg : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] {X Y : C} {f : X ⟶ Y},
  F.map (-f) = -F.map f
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.all_takeWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String}, (s.takeWhile pat).all pat = true
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.map_id : ∀ {α : Type u_1} (p : PMF α), PMF.map id p = p
-- Mathlib.Dynamics.TopologicalEntropy.Semiconj
Dynamics.IsDynCoverOf.preimage : ∀ {X : Type u_1} {Y : Type u_2} {F : Set X} {V : SetRel Y Y} {S : X → X} {T : Y → Y} {φ : X → Y} {n : ℕ},
  Function.Semiconj φ S T →
    ∀ [V.IsSymm] {t : Finset Y},
      Dynamics.IsDynCoverOf T (φ '' F) V n ↑t →
        ∃ s, Dynamics.IsDynCoverOf S F (Prod.map φ φ ⁻¹' V.comp V) n ↑s ∧ s.card ≤ t.card
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.ModuleColimit.map_smul_homEquiv'_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.IsCofiltered C] [inst_3 : CategoryTheory.InitiallySmall C]
  {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R}
  (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf}
  (hcM : CategoryTheory.Limits.IsColimit cM) {N : ModuleCat ↑cR.pt} (α : PresheafOfModules.ModuleColimit hcR hcM →+ ↑N),
  (∀ (U : Cᵒᵖ) (r : ↑(R.obj U)) (m : ↑(M.obj U)),
      (CategoryTheory.ConcreteCategory.hom (((PresheafOfModules.ModuleColimit.homEquiv' hcR hcM) α).app U)) (r • m) =
        (CategoryTheory.ConcreteCategory.hom (cR.ι.app U)) r •
          (CategoryTheory.ConcreteCategory.hom (((PresheafOfModules.ModuleColimit.homEquiv' hcR hcM) α).app U)) m) ↔
    ∀ (r : ↑cR.pt) (m : PresheafOfModules.ModuleColimit hcR hcM), α (r • m) = r • α m
-- Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished
Polynomial.IsDistinguishedAt.monic : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} {I : Ideal R}, f.IsDistinguishedAt I → f.Monic
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub.congr_simp : ∀ {X : Type u_1} {mX : MeasurableSpace X} (μ μ_1 : MeasureTheory.Measure X) (e_μ : μ = μ_1)
  (ν ν_1 : MeasureTheory.Measure X) (e_ν : ν = ν_1) [inst : MeasureTheory.IsFiniteMeasure μ]
  [inst_1 : MeasureTheory.IsFiniteMeasure ν],
  μ.jordanDecompositionOfToSignedMeasureSub ν = μ_1.jordanDecompositionOfToSignedMeasureSub ν_1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.diff_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₂.Equiv t₃ → (t₁ \ t₂).Equiv (t₁ \ t₃)
-- Mathlib.Algebra.Order.Field.Basic
exists_pos_mul_lt : ∀ {α : Type u_4} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α},
  0 < a → ∀ (b : α), ∃ c, 0 < c ∧ b * c < a
-- Mathlib.CategoryTheory.Limits.IndYoneda
/-- Variant of `coyonedaOoColimitIsoLimitCoyoneda` for contravariant `F`.  -/
CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {I : Type v₁} →
      [inst_1 : CategoryTheory.Category.{v₂, v₁} I] →
        (F : CategoryTheory.Functor Iᵒᵖ C) →
          [inst_2 : CategoryTheory.Limits.HasColimit F] →
            CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.Limits.colimit F)) ≅
              CategoryTheory.Limits.limit (F.rightOp.comp CategoryTheory.coyoneda)
-- Mathlib.Analysis.Distribution.TemperateGrowth
/-- Composition of two temperate growth functions is of temperate growth.

Version where the outer function `g` is only of temperate growth on the image of inner function
`f`.  -/
Function.HasTemperateGrowth.comp' : ∀ {D : Type u_4} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup D] [inst_5 : NormedSpace ℝ D]
  {g : E → F} {f : D → E} {t : Set E},
  Set.range f ⊆ t →
    UniqueDiffOn ℝ t →
      ContDiffOn ℝ (↑⊤) g t →
        (∀ (N : ℕ), ∃ k C, ∃ (_ : 0 ≤ C), ∀ n ≤ N, ∀ x ∈ t, ‖iteratedFDerivWithin ℝ n g t x‖ ≤ C * (1 + ‖x‖) ^ k) →
          Function.HasTemperateGrowth f → Function.HasTemperateGrowth (g ∘ f)
-- Mathlib.Topology.MetricSpace.Thickening
/-- **Alias** of `Metric.mem_thickening_iff_infEDist_lt`. -/
Metric.mem_thickening_iff_infEdist_lt : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ} {s : Set α} {x : α},
  x ∈ Metric.thickening δ s ↔ Metric.infEDist x s < ENNReal.ofReal δ
-- Mathlib.CategoryTheory.Endomorphism
/-- Isomorphisms induce isomorphisms of the automorphism group  -/
CategoryTheory.Aut.autMulEquivOfIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ≅ Y) → CategoryTheory.Aut X ≃* CategoryTheory.Aut Y
-- Mathlib.Data.EReal.Operations
EReal.sub_le_of_le_add : ∀ {a b c : EReal}, a ≤ b + c → a - c ≤ b
-- Mathlib.Data.Multiset.AddSub
Multiset.add_cons : ∀ {α : Type u_1} (a : α) (s t : Multiset α), s + a ::ₘ t = a ::ₘ (s + t)
-- Mathlib.Topology.VectorBundle.Riemannian
/-- Class used to create an inner product structure space on the fibers of a fiber bundle, without
creating diamonds. Use as follows:
* `instance : RiemannianBundle E := ⟨g⟩` where `g : RiemannianMetric E` registers the inner product
  space on the fibers;
* `instance : RiemannianBundle E := ⟨g.toRiemannianMetric⟩` where
  `g : ContinuousRiemannianMetric F E` registers the inner product space on the fibers, and the fact
  that it varies continuously (i.e., a `[IsContinuousRiemannianBundle]` instance).
* `instance : RiemannianBundle E := ⟨g.toRiemannianMetric⟩` where
  `g : ContMDiffRiemannianMetric IB n F E` registers the inner product space on the fibers, and the
  fact that it varies smoothly (and continuously), i.e., `[IsContMDiffRiemannianBundle]` and
  `[IsContinuousRiemannianBundle]` instances.

Note that this is only useful when there is a preexisting topology in the fibers of a vector
bundle, like for the tangent bundle. This should *not* be used to express theorems for general
bundles with a metric. Instead, use
```
variable {E : B → Type*} [TopologicalSpace (TotalSpace F E)]
  [∀ x, NormedAddCommGroup (E x)] [∀ x, InnerProductSpace ℝ (E x)]
  [FiberBundle F E] [VectorBundle ℝ F E] [IsContinuousRiemannianBundle F E]
```
 -/
Bundle.RiemannianBundle : {B : Type u_4} →
  (E : B → Type u_6) →
    [(b : B) → TopologicalSpace (E b)] →
      [inst : (b : B) → AddCommGroup (E b)] → [(b : B) → Module ℝ (E b)] → Type (max u_4 u_6)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.of.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R), AdjoinRoot.of f = (AdjoinRoot.mk f).comp Polynomial.C
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] [inst_3 : Inhabited α] {f : (a : α) → β a → Option (γ a)} {k : α} (h : m.WF),
  (Std.DHashMap.Raw.filterMap f m).getKey! k = ((m.getKey? k).pfilter fun x h' => (f x (m.get x ⋯)).isSome).get!
-- Mathlib.Algebra.Colimit.Ring
Ring.instInhabitedDirectLimit : {ι : Type u_1} →
  [inst : Preorder ι] →
    (G : ι → Type u_2) →
      [inst_1 : (i : ι) → CommRing (G i)] → (f : (i j : ι) → i ≤ j → G i → G j) → Inhabited (Ring.DirectLimit G f)
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_zero' : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.mgf X μ 0 = μ.real Set.univ
-- Mathlib.Topology.UniformSpace.Basic
uniformContinuous₂_curry : ∀ {α : Type ua} {β : Type ub} {γ : Type uc} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  (f : α × β → γ), UniformContinuous₂ (Function.curry f) ↔ UniformContinuous f
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.TensorProduct.map_toAlgHom : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} {D : Type u_6} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Bialgebra S A]
  [inst_5 : Bialgebra R B] [inst_6 : Algebra R A] [inst_7 : Algebra R S] [inst_8 : IsScalarTower R S A]
  [inst_9 : Semiring C] [inst_10 : Semiring D] [inst_11 : Bialgebra S C] [inst_12 : Bialgebra R D]
  [inst_13 : Algebra R C] [inst_14 : IsScalarTower R S C] (f : A →ₐc[S] C) (g : B →ₐc[R] D),
  ↑(Bialgebra.TensorProduct.map f g) = Algebra.TensorProduct.map ↑f ↑g
-- Mathlib.Topology.Defs.Filter
/-- Notation for the filter of punctured left neighborhoods of a point.  -/
Topology.nhdsLT : Lean.ParserDescr
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.counit_domCongr : ∀ {R : Type u_1} {A : Type u_3} {M : Type u_8} {N : Type u_9} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Bialgebra R A] [inst_3 : AddMonoid M] [inst_4 : AddMonoid N] (e : M ≃+ N) (x : AddMonoidAlgebra A M),
  CoalgebraStruct.counit ((AddMonoidAlgebra.domCongr R A e) x) = CoalgebraStruct.counit x
-- Mathlib.Order.Heyting.Basic
toDual_himp : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a b : α), OrderDual.toDual (a ⇨ b) = OrderDual.toDual b \ OrderDual.toDual a
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mem_iSup_of_mem : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {ι : Sort u_1} {b : M} {N : ι → LieSubmodule R L M} (i : ι),
  b ∈ N i → b ∈ ⨆ i, N i
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.pi_apply_coe : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {ι : Type u_6} (M : ι → Type u_7)
  [inst_1 : (i : ι) → AddCommGroup (M i)] [inst_2 : (i : ι) → Module R (M i)] (c : AdicCompletion I ((j : ι) → M j))
  (i : ι) (n : ℕ), ↑((AdicCompletion.pi I M) c i) n = (LinearMap.reduceModIdeal (I ^ n) (LinearMap.proj i)) (↑c n)
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
AnalyticWithinAt.rexp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {x : E},
  AnalyticWithinAt ℝ f s x → AnalyticWithinAt ℝ (fun z => Real.exp (f z)) s x
-- Mathlib.Logic.Relator
Relator.bi_total_eq : ∀ {α : Type u₁}, Relator.BiTotal Eq
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- `LightProfinite` is the category of second countable profinite spaces.  -/
LightProfinite : Type (u_1 + 1)
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- **Alias** of `mdifferentiableOn_localFrameCoeff`.

---

If `s` is differentiable on `t ⊆ e.baseSet`, so is its coefficient `b.localFrameCoeff e i`
in the local frame induced by `e`  -/
mdifferentiableOn_localFrame_coeff : ∀ {𝕜 : 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_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V]
  [inst_14 : ContMDiffVectorBundle 1 F V I] {e : Bundle.Trivialization F Bundle.TotalSpace.proj}
  [inst_15 : MemTrivializationAtlas e] {ι : Type u_7} (b : Module.Basis ι 𝕜 F) {s : (x : M) → V x} {t : Set M}
  [FiniteDimensional 𝕜 F] [CompleteSpace 𝕜],
  IsOpen t →
    t ⊆ e.baseSet →
      MDiff[t] (T% s) → ∀ (i : ι), MDiff[t] ((LinearMap.piApply (Bundle.Trivialization.localFrameCoeff I e b i)) s)
-- Mathlib.Logic.Equiv.List
Encodable.encodeList.eq_def : ∀ {α : Type u_1} [inst : Encodable α] (x : List α),
  Encodable.encodeList x =
    match x with
    | [] => 0
    | a :: l => (Nat.pair (Encodable.encode a) (Encodable.encodeList l)).succ
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.map_obj_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} {f : X ⟶ Y} {U : CategoryTheory.Under Y},
  ((CategoryTheory.Under.map f).obj U).right = U.right
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instFintypeOfDecidableEq : {n : Type u_7} →
  {m : Type u_8} →
    [Fintype m] →
      [DecidableEq m] → [Fintype n] → [DecidableEq n] → (α : Type u_9) → [Fintype α] → Fintype (CStarMatrix m n α)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- If a continuous multilinear map in finitely many variables on normed spaces satisfies
the inequality `‖f m‖ ≤ C * ∏ i, ‖m i‖` on a shell `ε i / ‖c i‖ < ‖m i‖ < ε i` for some positive
numbers `ε i` and elements `c i : 𝕜`, `1 < ‖c i‖`, then it satisfies this inequality for all `m`.  -/
MultilinearMap.bound_of_shell_of_continuous : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι] (f : MultilinearMap 𝕜 E G),
  Continuous ⇑f →
    ∀ {ε : ι → ℝ} {C : ℝ},
      (∀ (i : ι), 0 < ε i) →
        ∀ {c : ι → 𝕜},
          (∀ (i : ι), 1 < ‖c i‖) →
            (∀ (m : (i : ι) → E i),
                (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖) →
              ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
-- Mathlib.LinearAlgebra.Dimension.Constructions
finrank_le_of_span_eq_top : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {ι : Type u_2} [inst_4 : Fintype ι] {v : ι → M},
  Submodule.span R (Set.range v) = ⊤ → Module.finrank R M ≤ Fintype.card ι
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (c : CategoryTheory.Limits.KernelFork S.g)
  (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork S hf c hc).i = CategoryTheory.Limits.Fork.ι c
-- Std.Time.Date.Unit.Weekday
/-- Thursday.  -/
Std.Time.Weekday.thursday : Std.Time.Weekday
-- Mathlib.Algebra.Polynomial.AlgebraMap
/-- Polynomial evaluation on an indexed tuple is the indexed product of the evaluations
on the components.
Generalizes `Polynomial.aeval_prod` to indexed products.  -/
Polynomial.aeval_pi : ∀ {R : Type u} [inst : CommSemiring R] {I : Type u_3} {A : I → Type u_4} [inst_1 : (i : I) → Semiring (A i)]
  [inst_2 : (i : I) → Algebra R (A i)] (x : (i : I) → A i),
  Polynomial.aeval x = AlgHom.pi fun i => Polynomial.aeval (x i)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.instIsEmptyHomRightLeft : ∀ {J : CategoryTheory.Limits.MultispanShape} (a : J.R) (b : J.L),
  IsEmpty (CategoryTheory.Limits.WalkingMultispan.right a ⟶ CategoryTheory.Limits.WalkingMultispan.left b)
-- Mathlib.Combinatorics.Additive.Energy
Finset.mulEnergy_pos_iff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Mul α] {s t : Finset α}, 0 < s.mulEnergy t ↔ s.Nonempty ∧ t.Nonempty
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.const_prod_comp : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {δ : Type u_6} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel α β)
  [ProbabilityTheory.IsSFiniteKernel κ] (μ : MeasureTheory.Measure γ) [MeasureTheory.SFinite μ]
  (η : ProbabilityTheory.Kernel β δ) [ProbabilityTheory.IsSFiniteKernel η],
  ((ProbabilityTheory.Kernel.const β μ).prod η).comp κ = (ProbabilityTheory.Kernel.const α μ).prod (η.comp κ)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_modify : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k k' : α} {f : β k → β k},
      (Std.DTreeMap.Internal.Impl.modify k f t).get? k' =
        if h : compare k k' = Ordering.eq then cast ⋯ (Option.map f (t.get? k)) else t.get? k'
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {km : α},
  t.max? = some km → t.get! km = km
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isEmpty_toArray : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → m.toArray.isEmpty = m.isEmpty
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.IsColimit.inl_desc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  {t : CategoryTheory.Limits.PushoutCocone f g} (ht : CategoryTheory.Limits.IsColimit t) {W : C} (h : Y ⟶ W) (k : Z ⟶ W)
  (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) {Z_1 : C} (h_1 : W ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp t.inl
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PushoutCocone.IsColimit.desc ht h k w) h_1) =
    CategoryTheory.CategoryStruct.comp h h_1
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indepSets_congr : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ η : ProbabilityTheory.Kernel α Ω}
  {μ : MeasureTheory.Measure α} {s1 s2 : Set (Set Ω)},
  ⇑κ =ᵐ[μ] ⇑η → (ProbabilityTheory.Kernel.IndepSets s1 s2 κ μ ↔ ProbabilityTheory.Kernel.IndepSets s1 s2 η μ)
-- Mathlib.LinearAlgebra.Matrix.ToLin
endVecAlgEquivMatrixEnd_symm_apply_apply : ∀ (ι : Type u_1) [inst : Fintype ι] [inst_1 : DecidableEq ι] (R : Type u_2) [inst_2 : CommSemiring R] (A : Type u_3)
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (M : Type u_4) [inst_5 : AddCommMonoid M] [inst_6 : Module R M]
  [inst_7 : Module A M] [inst_8 : IsScalarTower R A M] (m : Matrix ι ι (Module.End A M)) (x : ι → M) (i : ι),
  ((endVecAlgEquivMatrixEnd ι R A M).symm m) x i = ∑ j, (m i j) (x j)
-- Mathlib.Topology.Order
continuous_le_rng : ∀ {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {t₂ t₃ : TopologicalSpace β},
  t₂ ≤ t₃ → Continuous f → Continuous f
-- Mathlib.Topology.NhdsWithin
tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {a : α} {l : Filter β} {s : Set α} (f : β → α),
  Filter.Tendsto f l (nhds a) → (∀ᶠ (x : β) in l, f x ∈ s) → Filter.Tendsto f l (nhdsWithin a s)
-- Mathlib.Logic.Basic
xor_not_right : ∀ {a b : Prop}, Xor a ¬b ↔ (a ↔ b)
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.toEquivalence_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G)
  [inst_2 : ∀ (X : C), CategoryTheory.IsIso (adj.unit.app X)]
  [inst_3 : ∀ (Y : D), CategoryTheory.IsIso (adj.counit.app Y)], adj.toEquivalence.inverse = G