mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.Monoidal.Functor
CategoryTheory.Localization.Monoidal.functorMonoidalOfComp_μ : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.MonoidalCategory C] [inst_4 : CategoryTheory.MonoidalCategory D]
  [inst_5 : CategoryTheory.MonoidalCategory E] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [inst_6 : L.IsLocalization W] [inst_7 : L.Monoidal] (F : CategoryTheory.Functor D E) (G : CategoryTheory.Functor C E)
  [inst_8 : G.Monoidal] [inst_9 : W.ContainsIdentities] [inst_10 : CategoryTheory.Localization.Lifting L W G F]
  (X Y : C),
  CategoryTheory.Functor.LaxMonoidal.μ F (L.obj X) (L.obj Y) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom ((CategoryTheory.Localization.Lifting.iso L W G F).hom.app X)
        ((CategoryTheory.Localization.Lifting.iso L W G F).hom.app Y))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ G X Y)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Localization.Lifting.iso L W G F).inv.app
            (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
          (F.map (CategoryTheory.Functor.OplaxMonoidal.δ L X Y))))
-- Init.Data.BitVec.Bitblast
/-- A lawful DivModState with a fully consumed dividend (`wn = 0`) witnesses that the
quotient has been correctly computed.
 -/
BitVec.DivModState.udiv_eq_of_lawful : ∀ {w : ℕ} {n d : BitVec w} {qr : BitVec.DivModState w},
  BitVec.DivModState.Lawful { n := n, d := d } qr → qr.wn = 0 → n / d = qr.q
-- Mathlib.Algebra.Order.Floor.Ring
Int.sub_one_lt_floor : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R), a - 1 < ↑⌊a⌋
-- Mathlib.CategoryTheory.Limits.EssentiallySmall
CategoryTheory.Limits.hasCoproductsOfShape_of_small : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (β : Type w₂) [Small.{w₁, w₂} β]
  [CategoryTheory.Limits.HasCoproducts C], CategoryTheory.Limits.HasCoproductsOfShape β C
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, returning `none` if no such pair exists.
 -/
Std.ExtTreeMap.getEntryLE? : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → Option (α × β)
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- `IsCyclotomicExtension S A B` is equivalent to `IsCyclotomicExtension (S ∪ {1}) A B`.  -/
IsCyclotomicExtension.iff_union_singleton_one : ∀ (S : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
  IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {1}) A B
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.inr_comp_binaryCoproductIso_hom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (a : C)
  (x : G.obj a),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.FunctorToTypes.binaryCoproductIso F G).hom.app a))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.coprod.inr.app a)) x) =
    Sum.inr x
-- Mathlib.CategoryTheory.FinCategory.AsType
CategoryTheory.FinCategory.asTypeToObjAsType_obj : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : CategoryTheory.SmallCategory α] [inst_2 : CategoryTheory.FinCategory α]
  (a : CategoryTheory.FinCategory.AsType α), (CategoryTheory.FinCategory.asTypeToObjAsType α).obj a = id a
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_le_one : ∀ {m : ℕ∞}, ↑m ≤ 1 ↔ m ≤ 1
-- Mathlib.AlgebraicGeometry.Group.Affine
/-- `Spec` is full on `R`-bialgebras.  -/
AlgebraicGeometry.bialgSpec.instFull : ∀ {R : CommRingCat}, (AlgebraicGeometry.bialgSpec R).Full
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.instCompleteSemilatticeInf : (M : Type u_1) → [inst : AddZeroClass M] → CompleteSemilatticeInf (SaturatedAddSubmonoid M)
-- Mathlib.RingTheory.Coalgebra.Equiv
/-- See Note [custom simps projection]  -/
CoalgEquiv.Simps.symm_apply : {R : Type u_5} →
  [inst : CommSemiring R] →
    {A : Type u_6} →
      {B : Type u_7} →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : AddCommMonoid B] →
            [inst_3 : Module R A] →
              [inst_4 : Module R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → (A ≃ₗc[R] B) → B → A
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.eq_1 : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) (X₀ : C₀),
  CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso data G₀ X₀ =
    { hom := CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.hom data G₀ X₀,
      inv := CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.inv data G₀ X₀, hom_inv_id := ⋯,
      inv_hom_id := ⋯ }
-- Mathlib.Analysis.SpecificLimits.Normed
tendsto_intCast_atBot_sup_atTop_cobounded : ∀ {α : Type u_1} [inst : NormedRing α] [NormSMulClass ℤ α] [Nontrivial α],
  Filter.Tendsto Int.cast (Filter.atBot ⊔ Filter.atTop) (Bornology.cobounded α)
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
/-- Given a functor `F : J ⥤ Type w₀`, this is a "cocone" of `F` where
we allow the point `pt` to be in a different universe than `w`.  -/
CategoryTheory.Functor.CoconeTypes : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] → CategoryTheory.Functor J (Type w₀) → Type (max (max u w₀) (w₁ + 1))
-- Mathlib.Algebra.Ring.Divisibility.Basic
/-- If `G` is a `LeftCancelSemiGroup`, left multiplication by `g` yields an equivalence between `G`
and the set of elements of `G` divisible by `g`.
 -/
Equiv.dvd : {G : Type u_4} → [inst : LeftCancelSemigroup G] → (g : G) → G ≃ { a // g ∣ a }
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.listDecode.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} (n : ℕ)
  (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
  FirstOrder.Language.BoundedFormula.listDecode (Sum.inr (Sum.inr n.succ.succ) :: l) =
    ⟨n, FirstOrder.Language.BoundedFormula.falsum⟩ :: FirstOrder.Language.BoundedFormula.listDecode l
-- Mathlib.RingTheory.Idempotents
/-- If a family is complete orthogonal, it consists of idempotents.  -/
CompleteOrthogonalIdempotents.iff_ortho_complete : ∀ {R : Type u_1} [inst : Semiring R] {I : Type u_3} {e : I → R} [inst_1 : Fintype I],
  CompleteOrthogonalIdempotents e ↔ (Pairwise fun x1 x2 => e x1 * e x2 = 0) ∧ ∑ i, e i = 1
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.whisker_left : {B : Type u} →
  [inst : Quiver B] →
    {a b c : CategoryTheory.FreeBicategory B} →
      (f : a ⟶ b) →
        {g h : b ⟶ c} →
          CategoryTheory.FreeBicategory.Hom₂ g h →
            CategoryTheory.FreeBicategory.Hom₂ (CategoryTheory.CategoryStruct.comp f g)
              (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- `E` refines its deduplication.  -/
CategoryTheory.PreZeroHypercover.toShrink : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {S : C} → (E : CategoryTheory.PreZeroHypercover S) → E.Hom E.shrink
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instInhabitedDiagnosticCode : Inhabited Lean.Lsp.DiagnosticCode
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.add_const : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : Add γ] [MeasurableAdd γ],
  ProbabilityTheory.IdentDistrib f g μ ν →
    ∀ (c : γ), ProbabilityTheory.IdentDistrib (fun x => f x + c) (fun x => g x + c) μ ν
-- Mathlib.Order.CompleteLattice.Basic
Prod.fst_sInf : ∀ {α : Type u_1} {β : Type u_2} [inst : InfSet α] [inst_1 : InfSet β] (s : Set (α × β)),
  (sInf s).1 = sInf (Prod.fst '' s)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.multicospan_obj_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) (a : J.L),
  I.multicospan.obj (CategoryTheory.Limits.WalkingMulticospan.left a) = I.left a
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.lift_map_homMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {E : Type u₂} [inst_1 : CategoryTheory.Groupoid E]
  (φ : CategoryTheory.Functor C E) {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.FreeGroupoid.lift φ).map (CategoryTheory.FreeGroupoid.homMk f) = φ.map f
-- Mathlib.Analysis.Complex.Trigonometric
Complex.two_cos : ∀ (x : ℂ), 2 * Complex.cos x = Complex.exp (x * Complex.I) + Complex.exp (-x * Complex.I)
-- Mathlib.Data.Set.Lattice
Set.iInter₂_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'
-- Mathlib.Probability.Distributions.Bernoulli
ProbabilityTheory.bernoulliMeasure_apply_of_mem_of_mem : ∀ {X : Type u_1} [inst : MeasurableSpace X] {x y : X} (p : ↑unitInterval) {s : Set X},
  MeasurableSet s → x ∈ s → y ∈ s → (ProbabilityTheory.bernoulliMeasure x y p) s = 1
-- Mathlib.NumberTheory.Padics.PadicIntegers
/-- `PadicInt.valuation` lifts the `p`-adic valuation on `ℚ` to `ℤ_[p]`.  -/
PadicInt.valuation : {p : ℕ} → [hp : Fact (Nat.Prime p)] → ℤ_[p] → ℕ
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.equalCommonMVars? : Lean.MVarId → Lean.MVarId → Aesop.EqualUpToIdsM (Option Bool)
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.main : Lean.Expr →
  Lean.Meta.Simp.Context →
    optParam Lean.Meta.Simp.Stats { } →
      optParam Lean.Meta.Simp.Methods { } → Lean.MetaM (Lean.Meta.Simp.Result × Lean.Meta.Simp.Stats)
-- Mathlib.Probability.Process.Filtration
/-- The sequence of sub-σ-algebras of `m`  -/
MeasureTheory.Filtration.seq : {Ω : Type u_1} →
  {ι : Type u_2} → [inst : Preorder ι] → {m : MeasurableSpace Ω} → MeasureTheory.Filtration ι m → ι → MeasurableSpace Ω
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocycles₁IsoOfIsTrivial_inv_hom_apply_coe : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u_1, u, u} k G) [hA : A.IsTrivial]
  (a : Additive G →+ ↑A) (a_1 : Additive G),
  ↑((ModuleCat.Hom.hom (groupCohomology.cocycles₁IsoOfIsTrivial A).inv) a) a_1 = a a_1
-- Lean.Attributes
Lean.AttributeExtensionOLeanEntry.mk.inj : ∀ {builderId ref : Lean.Name} {args : List Lean.DataValue} {builderId_1 ref_1 : Lean.Name}
  {args_1 : List Lean.DataValue},
  { builderId := builderId, ref := ref, args := args } = { builderId := builderId_1, ref := ref_1, args := args_1 } →
    builderId = builderId_1 ∧ ref = ref_1 ∧ args = args_1
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preBeth_pos : ∀ {o : Ordinal.{u_1}}, 0 < Cardinal.preBeth o ↔ 0 < o
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
Filter.EventuallyEq.hasLineDerivWithinAt_iff_of_mem : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f₀ f₁ : E → F}
  {f' : F} {s : Set E} {x v : E},
  f₀ =ᶠ[nhdsWithin x s] f₁ → x ∈ s → (HasLineDerivWithinAt 𝕜 f₀ f' s x v ↔ HasLineDerivWithinAt 𝕜 f₁ f' s x v)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k} {he : (t.modify k f).isEmpty = false},
  (t.modify k f).minKey he = t.minKey ⋯
-- Mathlib.SetTheory.Ordinal.Veblen
/-- **Alias** of `Ordinal.gamma_zero_eq_nfp`. -/
Ordinal.gamma0_eq_nfp : Ordinal.gamma 0 = Ordinal.nfp (fun x => Ordinal.veblen x 0) 0
-- Mathlib.Analysis.Complex.Circle
Circle.ofConjDivSelf_coe : ∀ (z : ℂ) (hz : z ≠ 0), ↑(Circle.ofConjDivSelf z hz) = (starRingEnd ℂ) z / z
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
Char.reduceBNe : Lean.Meta.Simp.DSimproc
-- Mathlib.CategoryTheory.Subobject.Comma
/-- If `C` is well-copowered and cocomplete and `S` preserves colimits, then
`CostructuredArrow S T` is well-copowered.  -/
CategoryTheory.CostructuredArrow.well_copowered_costructuredArrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor C D} {T : D} [inst_2 : CategoryTheory.LocallySmall.{w, v₁, u₁} C]
  [CategoryTheory.WellPowered.{w, v₁, u₁} Cᵒᵖ] [CategoryTheory.Limits.HasFiniteColimits C]
  [CategoryTheory.Limits.PreservesFiniteColimits S],
  CategoryTheory.WellPowered.{w, v₁, max u₁ v₂} (CategoryTheory.CostructuredArrow S T)ᵒᵖ
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bddAbove_range_add_one_iff : ∀ {β : Type u_2} {f : β → Ordinal.{u}}, BddAbove (Set.range fun i => f i + 1) ↔ BddAbove (Set.range f)
-- Init.System.IO
/-- A byte buffer that can simulate a file in memory.

Use `IO.FS.Stream.ofBuffer` to create a stream from a buffer.
 -/
IO.FS.Stream.Buffer : Type
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Auxiliary lemma for the proof of `oangle_sign_smul_add_right`; not intended to be used
outside of that proof.  -/
Orientation.oangle_smul_add_right_eq_zero_or_eq_pi_iff : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V} (r : ℝ),
  o.oangle x (r • x + y) = 0 ∨ o.oangle x (r • x + y) = ↑Real.pi ↔ o.oangle x y = 0 ∨ o.oangle x y = ↑Real.pi
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
hasProd_subtype_iff_of_mulSupport_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α} {s : Set β},
  Function.mulSupport f ⊆ s → (HasProd (f ∘ Subtype.val) a ↔ HasProd f a)
-- Mathlib.RingTheory.Valuation.RankOne
Valuation.RankOne.restrict_RankOne : {Γ₀ : Type u_2} →
  [inst : LinearOrderedCommGroupWithZero Γ₀] →
    (K : Type u_3) → [inst_1 : DivisionRing K] → (v : Valuation K Γ₀) → [v.RankOne] → v.restrict.RankOne
-- Mathlib.Analysis.InnerProductSpace.Subspace
/-- The composition of an orthogonal family of subspaces with an injective function is also an
orthogonal family.  -/
OrthogonalFamily.comp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {G : ι → Type u_5} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E},
  OrthogonalFamily 𝕜 G V →
    ∀ {γ : Type u_6} {f : γ → ι}, Function.Injective f → OrthogonalFamily 𝕜 (fun g => G (f g)) fun g => V (f g)
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.toSlashInvariantForm_intCast : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne] (z : ℤ), (↑z).toSlashInvariantForm = ↑z
-- Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
CategoryTheory.SmallObject.SuccStruct.transfiniteCompositionOfShapeιIteration_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) (J : Type w)
  [inst_1 : LinearOrder J] [inst_2 : OrderBot J] [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C],
  (Φ.transfiniteCompositionOfShapeιIteration J).F = Φ.iterationFunctor J
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.minimalPeriod_iterate_eq_div_gcd : ∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ},
  n ≠ 0 → Function.minimalPeriod f^[n] x = Function.minimalPeriod f x / (Function.minimalPeriod f x).gcd n
-- Mathlib.Topology.Compactness.LocallyCompact
instWeaklyLocallyCompactSpaceOfCompactSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [CompactSpace X], WeaklyLocallyCompactSpace X
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
/-- Given `ℌ : DayConvolutionInternalHom F H`, if we think of `H.obj G`
as the internal hom `[F, G]`, then this is the transformation
corresponding to the component at `G` of the "coevaluation" natural morphism
`𝟭 ⟶ [F, F ⊛ _]`.  -/
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.coev_app : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            [inst_4 : CategoryTheory.MonoidalClosed V] →
              {F H G : CategoryTheory.Functor C V} →
                [inst_5 : CategoryTheory.MonoidalCategory.DayConvolution F G] →
                  CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F
                      (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H →
                    (G ⟶ H)
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.toAddHom : {M : Type u_10} → {N : Type u_11} → [inst : AddZero M] → [inst_1 : AddZero N] → (M →+ N) → M →ₙ+ N
-- Mathlib.RingTheory.PowerBasis
/-- There are finitely many algebra homomorphisms `S →ₐ[A] B` if `S` is of the form `A[x]`
and `B` is an integral domain.  -/
PowerBasis.AlgHom.fintype : {S : Type u_2} →
  [inst : Ring S] →
    {A : Type u_4} →
      {B : Type u_5} →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing B] →
            [inst_3 : Algebra A B] → [inst_4 : Algebra A S] → [IsDomain B] → PowerBasis A S → Fintype (S →ₐ[A] B)
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
/-- If `f` is a transfinite composition of shape `J`, then `F.map f` also is
provided `F` preserves suitable colimits.  -/
CategoryTheory.TransfiniteCompositionOfShape.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {J : Type w} →
          [inst_2 : LinearOrder J] →
            [inst_3 : OrderBot J] →
              {X Y : C} →
                {f : X ⟶ Y} →
                  [inst_4 : SuccOrder J] →
                    [inst_5 : WellFoundedLT J] →
                      CategoryTheory.TransfiniteCompositionOfShape J f →
                        (F : CategoryTheory.Functor C D) →
                          [CategoryTheory.Limits.PreservesWellOrderContinuousOfShape J F] →
                            [CategoryTheory.Limits.PreservesColimitsOfShape J F] →
                              CategoryTheory.TransfiniteCompositionOfShape J (F.map f)
-- Mathlib.Analysis.Normed.Group.Defs
enorm_lt_top : ∀ {E : Type u_8} [inst : NNNorm E] {x : E}, ‖x‖ₑ < ⊤
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min_le_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  (hc : t.contains k = true), (cmp (t.min ⋯) k).isLE = true
-- Mathlib.Data.ENat.Basic
ENat.recTopCoe_one : ∀ {C : ℕ∞ → Sort u_1} (d : C ⊤) (f : (a : ℕ) → C ↑a), ENat.recTopCoe d f 1 = f 1
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.uncurry_obj_map : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) {X Y : C × D} (f : X ⟶ Y),
  (CategoryTheory.Functor.uncurry.obj F).map f =
    CategoryTheory.CategoryStruct.comp ((F.map f.1).app X.2) ((F.obj Y.1).map f.2)
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
_private.Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas.0.Nat.nthRoot.match_3.eq_3 : ∀ (motive : ℕ → ℕ → Sort u_1) (n a : ℕ) (h_1 : (x : ℕ) → motive 0 x) (h_2 : (a : ℕ) → motive 1 a)
  (h_3 : (n a : ℕ) → motive n.succ.succ a),
  (match n.succ.succ, a with
    | 0, x => h_1 x
    | 1, a => h_2 a
    | n.succ.succ, a => h_3 n a) =
    h_3 n a
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.set_smul_le_iff : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_4}
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M] (s : Set S) (N p : Submodule R M),
  s • N ≤ p ↔ ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p
-- Mathlib.Computability.Reduce
ManyOneEquiv.congr_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable γ]
  {p : α → Prop} {q : β → Prop} {r : γ → Prop}, ManyOneEquiv q r → (ManyOneEquiv p q ↔ ManyOneEquiv p r)
-- Init.Data.Range.Polymorphic.UInt
UInt8.instLawfulHasSize : Std.Rxc.LawfulHasSize UInt8
-- Lean.Elab.Do.PatternVar
Lean.Elab.Do.getLetRecDeclsVars : Lean.TSyntax `Lean.Parser.Term.letRecDecls → Lean.Elab.TermElabM (Array Lean.Ident)
-- Mathlib.Order.CompleteLattice.Basic
iInf_union : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {s t : Set β},
  ⨅ x ∈ s ∪ t, f x = (⨅ x ∈ s, f x) ⊓ ⨅ x ∈ t, f x
-- Init.Data.SInt.Lemmas
Int16.toInt_ofBitVec : ∀ (b : BitVec 16), (Int16.ofBitVec b).toInt = b.toInt
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.edist_eq_eLpNorm_neg_add : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f g : ↥(MeasureTheory.Lp E p μ)), edist f g = MeasureTheory.eLpNorm (-↑↑f + ↑↑g) p μ
-- Mathlib.Data.Set.Lattice
Set.sInter_image : ∀ {α : Type u_1} {β : Type u_2} (f : α → Set β) (s : Set α), ⋂₀ (f '' s) = ⋂ a ∈ s, f a
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.toKaroubi_map_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y),
  ((CategoryTheory.Idempotents.toKaroubi C).map f).f = f
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_eq_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α] {k fallback : α},
  k ∈ m → m.getKeyD k fallback = k
-- Mathlib.Analysis.Convex.Function
StrictConcaveOn.comp_concaveOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid α] [inst_4 : PartialOrder α] [inst_5 : AddCommMonoid β]
  [inst_6 : PartialOrder β] [inst_7 : SMul 𝕜 E] [inst_8 : SMul 𝕜 α] [inst_9 : SMul 𝕜 β] {s : Set E} {f : E → β}
  {g : β → α},
  StrictConcaveOn 𝕜 (f '' s) g → ConcaveOn 𝕜 s f → MonotoneOn g (f '' s) → Set.InjOn f s → StrictConcaveOn 𝕜 s (g ∘ f)
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.decidableElim.sizeOf_spec : ∀ (classical : Bool) (p₁ x : Lean.Name) (p₂ p₃ : Mathlib.Tactic.ITauto.Proof),
  sizeOf (Mathlib.Tactic.ITauto.Proof.decidableElim classical p₁ x p₂ p₃) =
    1 + sizeOf classical + sizeOf p₁ + sizeOf x + sizeOf p₂ + sizeOf p₃
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.equiv_trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] (f : α ≃ₜ β) (g : β ≃ₜ γ),
  TopologicalSpace.Compacts.equiv (f.trans g) =
    (TopologicalSpace.Compacts.equiv f).trans (TopologicalSpace.Compacts.equiv g)
-- Mathlib.Analysis.Matrix.Normed
/-- Seminormed ring instance (using sup norm of L1 norm) for matrices over a seminormed ring. Not
declared as an instance because there are several natural choices for defining the norm of a
matrix.  -/
Matrix.linftyOpSemiNormedRing : {n : Type u_4} → {α : Type u_5} → [Fintype n] → [SeminormedRing α] → [DecidableEq n] → SeminormedRing (Matrix n n α)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.module.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.module = 1