mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finset.NAry
/-- Symmetric statement to `Finset.image₂_image_left_anticomm`.  -/
Finset.image_image₂_antidistrib_left : ∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq β']
  [inst_1 : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β} [inst_2 : DecidableEq δ] {g : γ → δ}
  {f' : β' → α → δ} {g' : β → β'},
  (∀ (a : α) (b : β), g (f a b) = f' (g' b) a) →
    Finset.image g (Finset.image₂ f s t) = Finset.image₂ f' (Finset.image g' t) s
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.powerSeriesPart_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] (x : LaurentSeries R), x.powerSeriesPart = 0 ↔ x = 0
-- Std.Do.WP.Monad
_private.Std.Do.WP.Monad.0.EStateM.run_bind.match_1.splitter : {ε σ α : Type u_1} →
  (motive : EStateM.Result ε σ α → Sort u_2) →
    (x : EStateM.Result ε σ α) →
      ((x : α) → (s : σ) → motive (EStateM.Result.ok x s)) →
        ((e : ε) → (s : σ) → motive (EStateM.Result.error e s)) → motive x
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncGELTToLTGE_app_pentagon_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : ℤ) (X : C) {Z : C}
  (h : (t.truncGE a).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.truncGEπ a).app ((t.truncLT b).obj X))
      (CategoryTheory.CategoryStruct.comp ((t.truncGELTToLTGE a b).app X)
        (CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app ((t.truncGE a).obj X)) h)) =
    CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app X)
      (CategoryTheory.CategoryStruct.comp ((t.truncGEπ a).app X) h)
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.const_sub : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (x y : β),
  CauSeq.const abv (x - y) = CauSeq.const abv x - CauSeq.const abv y
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.IsPreLocalizingSequence.tendsto_top : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [inst : Preorder ι] [inst_1 : TopologicalSpace ι]
  [inst_2 : OrderTopology ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {τ : ℕ → Ω → WithTop ι}
  {P : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IsPreLocalizingSequence._auto_1},
  ProbabilityTheory.IsPreLocalizingSequence 𝓕 τ P → ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun x => τ x ω) Filter.atTop (nhds ⊤)
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb'_cast : ∀ {w a : ℕ} {hcast : w = a} {start len : ℕ} {x : BitVec w},
  BitVec.extractLsb' start len (BitVec.cast hcast x) = BitVec.extractLsb' start len x
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
FundamentalGroupoid.subsingleton_iff : ∀ (X : Type u_3), Subsingleton (FundamentalGroupoid X) ↔ Subsingleton X
-- Mathlib.Topology.Order.Lattice
ContinuousOn.finset_inf : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeInf L] [inst_3 : OrderTop L] [ContinuousInf L] {s : Finset ι} {f : ι → X → L} {t : Set X},
  (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (s.inf f) t
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
/-- Special case of `isSheafFor_singleton_iff` with `c = pullback.cone f f`.  -/
CategoryTheory.Equalizer.Presieve.isSheafFor_singleton_iff_of_hasPullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type u_1)} {X Y : C}
  {f : X ⟶ Y} [inst_1 : CategoryTheory.Limits.HasPullback f f],
  CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.singleton f) ↔
    Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (F.map f.op) ⋯))
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.smul_zero : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : AddMonoid X] [inst_3 : DistribMulAction R X] (x : OreLocalization S R), x • 0 = 0
-- Lean.Level
Lean.Level.geq : Lean.Level → Lean.Level → Bool
-- Mathlib.Analysis.Fourier.AddCircle
fourierCoeff_liftIoc_eq : ∀ {T : ℝ} [hT : Fact (0 < T)] {a : ℝ} (f : ℝ → ℂ) (n : ℤ),
  fourierCoeff (AddCircle.liftIoc T a f) n = fourierCoeffOn ⋯ f n
-- Mathlib.Data.Nat.Log
Nat.lt_clog_iff_pow_lt : ∀ {b : ℕ}, 1 < b → ∀ {x y : ℕ}, y < Nat.clog b x ↔ b ^ y < x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.maxKey!_alter_eq_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {f : Option β → Option β},
  Std.ExtDTreeMap.Const.alter t k f ≠ ∅ →
    ((Std.ExtDTreeMap.Const.alter t k f).maxKey! = k ↔
      (f (Std.ExtDTreeMap.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true)
-- Init.Data.String.Basic
String.Pos.str_toSlice : ∀ {s : String} {p : s.Pos}, p.toSlice.str = p
-- Init.Data.Array.Attach
Array.getElem?_unattach : ∀ {α : Type u_1} {p : α → Prop} {xs : Array { x // p x }} (i : ℕ), xs.unattach[i]? = Option.map Subtype.val xs[i]?
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mod_lt : ∀ (a : Ordinal.{u_4}) {b : Ordinal.{u_4}}, b ≠ 0 → a % b < b
-- Mathlib.Order.Closure
/-- The Galois insertion associated to a closure operator can be used to reconstruct the closure
operator.
Note that the inverse in the opposite direction does not hold in general.  -/
closureOperator_gi_self : ∀ {α : Type u_1} [inst : PartialOrder α] (c : ClosureOperator α), ⋯.closureOperator = c
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.all.injEq : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (f f_1 : L.BoundedFormula α (n + 1)), (f.all = f_1.all) = (f = f_1)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.toPoly.go.eq_2 : ∀ (coeff : ℕ) (i : Nat.Internal.Linear.Var),
  Nat.Internal.Linear.Expr.toPoly.go coeff (Nat.Internal.Linear.Expr.var i) = fun x => (coeff, i) :: x
-- Mathlib.Algebra.Group.Translate
translate_translate : ∀ {α : Type u_2} {G : Type u_5} [inst : AddCommGroup G] (a b : G) (f : G → α),
  translate a (translate b f) = translate (a + b) f
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpace.secondCountable_of_countable_cover : ∀ (H : Type u) {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  [SecondCountableTopology H] {s : Set M},
  ⋃ x ∈ s, (chartAt H x).source = Set.univ → s.Countable → SecondCountableTopology M
-- Init.Data.Sum.Lemmas
Sum.getLeft?.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (val : β), (Sum.inr val).getLeft? = none
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.liftStar_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → F.obj x ⟶ Z)
  (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (F.map f) (M y) = M x),
  (CategoryTheory.WithTerminal.liftStar F M hM).hom = CategoryTheory.CategoryStruct.id Z
-- Mathlib.RingTheory.Valuation.Discrete.Basic
/-- A constructor for `Uniformizer`.  -/
Valuation.Uniformizer.mk' : {Γ : Type u_1} →
  [inst : LinearOrderedCommGroupWithZero Γ] →
    {A : Type u_2} →
      [inst_1 : Ring A] → {v : Valuation A Γ} → [hv : v.IsRankOneDiscrete] → {x : A} → v.IsUniformizer x → v.Uniformizer
-- Init.Data.SInt.Lemmas
Int64.ofBitVec_int16ToBitVec : ∀ (x : Int16), Int64.ofBitVec (BitVec.signExtend 64 x.toBitVec) = x.toInt64
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- When both maps `S.f` and `S.g` of a short complex `S` are zero, this is the right homology map
data (for the identity of `S`) which relates the right homology data `ofZeros` and
`ofIsColimitCokernelCofork`.  -/
CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork : {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) →
          (hg : S.g = 0) →
            (c : CategoryTheory.Limits.CokernelCofork S.f) →
              (hc : CategoryTheory.Limits.IsColimit c) →
                CategoryTheory.ShortComplex.RightHomologyMapData (CategoryTheory.CategoryStruct.id S)
                  (CategoryTheory.ShortComplex.RightHomologyData.ofZeros S hf hg)
                  (CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork S hg c hc)
-- Mathlib.RingTheory.Multiplicity
emultiplicity.eq_1 : ∀ {α : Type u_1} [inst : Monoid α] (a b : α),
  emultiplicity a b = if h : FiniteMultiplicity a b then ↑(Nat.find h) else ⊤
-- Mathlib.Computability.NFA
Language.IsRegular.reverse : ∀ {α : Type u} {L : Language α}, L.IsRegular → L.reverse.IsRegular
-- Aesop.Tree.Stats
Aesop.collectGoalStatsIfEnabled : Aesop.TreeM Unit
-- Mathlib.Topology.Separation.CompletelyRegular
CompletelyRegularSpace.completely_regular : ∀ {X : Type u} {inst : TopologicalSpace X} [self : CompletelyRegularSpace X] (x : X) (K : Set X),
  IsClosed K → x ∉ K → ∃ f, Continuous f ∧ f x = 0 ∧ Set.EqOn f 1 K
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.SigmaFinite.mk : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  Nonempty (μ.FiniteSpanningSetsIn Set.univ) → MeasureTheory.SigmaFinite μ
-- Mathlib.Algebra.SkewMonoidAlgebra.Support
/-- An element of `SkewMonoidAlgebra k G` is in the subalgebra generated by its support.  -/
SkewMonoidAlgebra.mem_span_support : ∀ {k : Type u_1} {G : Type u_2} [inst : Monoid G] [inst_1 : Semiring k] [inst_2 : MulSemiringAction G k]
  (f : SkewMonoidAlgebra k G), f ∈ Submodule.span k (⇑(SkewMonoidAlgebra.of k G) '' ↑f.support)
-- Mathlib.Data.Set.Countable
/-- Restate `Set.Countable` as a `Countable` instance.  -/
Set.Countable.to_subtype : ∀ {α : Type u} {s : Set α}, s.Countable → Countable ↑s
-- Mathlib.Topology.Basic
isClosed_biUnion_finset : ∀ {X : Type u} {α : Type u_1} [inst : TopologicalSpace X] {s : Finset α} {f : α → Set X},
  (∀ i ∈ s, IsClosed (f i)) → IsClosed (⋃ i ∈ s, f i)
-- Std.Do.SPred.DerivedLaws
/-- A proof that the decomposition is logically equivalent to the original predicate.  -/
Std.Do.SPred.Tactic.IsAnd.to_and : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs} {Q₁ Q₂ : outParam (Std.Do.SPred σs)}
  [self : Std.Do.SPred.Tactic.IsAnd P Q₁ Q₂], P ⊣⊢ₛ Q₁ ∧ Q₂
-- Mathlib.LinearAlgebra.Basis.MulOpposite
Module.Basis.mulOpposite_apply : ∀ {R : Type u_1} {H : Type u_2} {ι : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid H] [inst_2 : Module R H]
  (b : Module.Basis ι R H) (i : ι), b.mulOpposite i = MulOpposite.op (b i)
-- Mathlib.GroupTheory.CoprodI
/-- One can replace the first letter in a non-empty reduced word by an element of the same
group  -/
Monoid.CoprodI.NeWord.replaceHead : {ι : Type u_1} →
  {M : ι → Type u_2} →
    [inst : (i : ι) → Monoid (M i)] →
      {i j : ι} → (x : M i) → x ≠ 1 → Monoid.CoprodI.NeWord M i j → Monoid.CoprodI.NeWord M i j
-- Init.Internal.Order.While
/-- One-step unfolding of `repeatM` for any `MonadTail m`.  -/
repeatM_eq_of_monadTail : ∀ {α : Type u} {m : Type u → Type v} [inst : Monad m] {β : Type u} [Lean.Order.MonadTail m] [inst_2 : Nonempty β]
  {f : α → m (α ⊕ β)} (a : α), repeatM f a = repeatM.body f (repeatM f) a
-- Mathlib.Tactic.MkIffOfInductiveProp
/-- Splits the goal `n` times via `refine ⟨?_,?_⟩`, and then applies `constructor` to
close the resulting subgoals.
 -/
Mathlib.Tactic.MkIff.splitThenConstructor : Lean.MVarId → ℕ → Lean.MetaM Unit
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.empty : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G), μ ⊥ = 0
-- Mathlib.Data.ENNReal.Operations
ENNReal.top_sub : ∀ {a : ENNReal}, a ≠ ⊤ → ⊤ - a = ⊤
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.one_mem : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  1 ∈ S
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
/-- Let `L : C ⥤ D` be a localization functor for `W`, if an extension `E`
of `F : C ⥤ H` along `L` is such that the natural transformation
`E.hom : L ⋙ E.right ⟶ F` is an isomorphism, then `E` is a pointwise
right Kan extension.  -/
CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionOfIsIsoOfIsLocalization : {C : Type u₁} →
  {D : Type u₂} →
    {H : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} H] →
            {F : CategoryTheory.Functor C H} →
              {L : CategoryTheory.Functor C D} →
                (W : CategoryTheory.MorphismProperty C) →
                  (E : L.RightExtension F) →
                    [CategoryTheory.IsIso (CategoryTheory.CostructuredArrow.hom E)] →
                      [L.IsLocalization W] → E.IsPointwiseRightKanExtension
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.Karoubi.HomologicalComplex.comp_p_d : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {P Q : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} (f : P ⟶ Q) (n : ι),
  CategoryTheory.CategoryStruct.comp (f.f.f n) (Q.p.f n) = f.f.f n
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
HasStrictFDerivAt.localInverse_continuousAt : ∀ {𝕜 : 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 : E → F}
  {f' : E ≃L[𝕜] F} {a : E} [inst_5 : CompleteSpace E] (hf : HasStrictFDerivAt f (↑f') a),
  ContinuousAt (HasStrictFDerivAt.localInverse f f' a hf) (f a)
-- Mathlib.Order.CompleteLattice.Finset
Finset.set_biUnion_insert_update : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] {x : α} {t : Finset α} (f : α → Set β) {s : Set β},
  x ∉ t → ⋃ i ∈ insert x t, Function.update f x s i = s ∪ ⋃ i ∈ t, f i
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelFactorThruImage_hom_comp_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] [inst_3 : CategoryTheory.Limits.HasImage f]
  [inst_4 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.factorThruImage f)] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelFactorThruImage f).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.factorThruImage f)) h
-- Mathlib.Computability.Language
Language.mem_pow : ∀ {α : Type u_1} {l : Language α} {x : List α} {n : ℕ}, x ∈ l ^ n ↔ ∃ S, x = S.flatten ∧ S.length = n ∧ ∀ y ∈ S, y ∈ l
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCycle.isPath_drop : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {n : ℕ} {p : G.Walk u u}, p.IsCycle → 0 < n → (p.drop n).IsPath
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.functorProdFunctorEquivCounitIso_hom_app_app : ∀ (A : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (C : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (X : CategoryTheory.Functor A (B × C)) (X_1 : A),
  ((CategoryTheory.functorProdFunctorEquivCounitIso A B C).hom.app X).app X_1 =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (X.obj X_1).1)
      (CategoryTheory.CategoryStruct.id (X.obj X_1).2)
-- Mathlib.Algebra.Ring.Ext
Ring.toSemiring_injective : ∀ {R : Type u}, Function.Injective (@Ring.toSemiring R)
-- Std.Net.Addr
Std.Net.AddressFamily.ofNat_ctorIdx : ∀ (x : Std.Net.AddressFamily), Std.Net.AddressFamily.ofNat x.ctorIdx = x
-- Mathlib.Algebra.Star.SelfAdjoint
isSelfAdjoint_ringInverse_iff : ∀ {A : Type u_2} {a : A} [inst : Semiring A] [inst_1 : StarRing A],
  IsUnit a → (IsSelfAdjoint (Ring.inverse a) ↔ IsSelfAdjoint a)
-- Mathlib.Algebra.CharP.MixedCharZero
/-- Reduction to `p` prime: When proving any statement `P` about mixed characteristic rings we
can always assume that `p` is prime.
 -/
MixedCharZero.reduce_to_p_prime : ∀ (R : Type u_1) [inst : CommRing R] {P : Prop},
  (∀ p > 0, MixedCharZero R p → P) ↔ ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
-- Mathlib.Analysis.Calculus.Deriv.Inv
deriv_const_div : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {d : 𝕜 → 𝕜'} (c : 𝕜'),
  DifferentiableAt 𝕜 d x → d x ≠ 0 → deriv (fun x => c / d x) x = -c * deriv d x / d x ^ 2
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolutionUnit.corepresentableByRight_homEquiv : ∀ {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]
  (U : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolutionUnit U]
  (F : CategoryTheory.Functor C V)
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F U] {Y : CategoryTheory.Functor C V},
  (CategoryTheory.MonoidalCategory.DayConvolutionUnit.corepresentableByRight U F).homEquiv =
    ((CategoryTheory.MonoidalCategory.DayConvolution.convolution F U).homEquivOfIsLeftKanExtension
          (CategoryTheory.MonoidalCategory.DayConvolution.unit F U) Y).trans
      ((CategoryTheory.MonoidalCategory.externalProduct F U).homEquivOfIsLeftKanExtension
        (CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitRight U
          (CategoryTheory.MonoidalCategory.DayConvolutionUnit.φ U) F)
        ((CategoryTheory.MonoidalCategory.tensor C).comp Y))
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- From a natural transformation of functors `C ⥤ D`, the induced natural transformation
of functors `WithTerminal C ⥤ WithTerminal D`.  -/
CategoryTheory.WithTerminal.map₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {F G : CategoryTheory.Functor C D} →
          (F ⟶ G) → (CategoryTheory.WithTerminal.map F ⟶ CategoryTheory.WithTerminal.map G)
-- Init.Data.Array.Count
Array.countP_eq_size_filter' : ∀ {α : Type u_1} {p : α → Bool}, Array.countP p = Array.size ∘ fun as => Array.filter p as
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.startsWith_char_eq_head? : ∀ {c : Char} {s : String.Slice}, s.startsWith c = (s.copy.toList.head? == some c)
-- Aesop.Tree.Data
Aesop.Goal.hasSafeRapp : Aesop.Goal → BaseIO Bool
-- Mathlib.Order.Lex
instBEqLex : (α : Type u_2) → [BEq α] → BEq (Lex α)
-- Lean.Util.Trace
_private.Lean.Util.Trace.0.Lean.withTraceNodeBefore.postCallback : {α : Type} →
  {m : Type → Type} →
    [Monad m] →
      [Lean.MonadTrace m] →
        {ε : Type} →
          [Lean.MonadRef m] →
            [Lean.AddMessageContext m] →
              [always : Lean.MonadAlwaysExcept ε m] →
                [Lean.ExceptToTraceResult ε α] →
                  Lean.Name →
                    Bool →
                      String →
                        Lean.Options →
                          Bool →
                            Lean.PersistentArray Lean.TraceElem →
                              Lean.Syntax → Lean.MessageData → Except ε α × Float × Float → m α
-- Std.Async.System
/-- CPU model name.
 -/
Std.Async.System.CPUInfo.model : Std.Async.System.CPUInfo → String
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.algebraMap_residue : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : IsLocalRing R] [inst_2 : CommRing S]
  [inst_3 : IsLocalRing S] [inst_4 : Algebra R S] [inst_5 : IsLocalHom (algebraMap R S)] (x : R),
  (algebraMap (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)) ((IsLocalRing.residue R) x) =
    (IsLocalRing.residue S) ((algebraMap R S) x)
-- Mathlib.Analysis.Distribution.TemperateGrowth
Function.HasTemperateGrowth.sub : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f g : E → F},
  Function.HasTemperateGrowth f → Function.HasTemperateGrowth g → Function.HasTemperateGrowth (f - g)
-- Mathlib.Data.Fintype.Pi
Fintype.eval_image_piFinset_const : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {β : Type u_5} [inst_2 : DecidableEq β] (t : Finset β)
  (a : α), Finset.image (fun f => f a) (Fintype.piFinset fun _i => t) = t
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.Subshift.mk.sizeOf_spec : ∀ {A : Type u_1} [inst : TopologicalSpace A] {G : Type u_2} [inst_1 : AddMonoid G] [inst_2 : SizeOf A]
  [inst_3 : SizeOf G] (carrier : Set (G → A)) (isClosed : IsClosed carrier)
  (mapsTo : ∀ (g : G), Set.MapsTo (SymbolicDynamics.FullShift.shift g) carrier carrier),
  sizeOf { carrier := carrier, isClosed := isClosed, mapsTo := mapsTo } = 1 + sizeOf isClosed
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithLower.ofLower_toLower : ∀ {α : Type u_1} (a : α), Topology.WithLower.ofLower (Topology.WithLower.toLower a) = a
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.cocone_ι_app : ∀ {ι : Type v} {α : Type u} (U : ι → α) [inst : CompleteLattice α] (o : CategoryTheory.Pairwise ι),
  (CategoryTheory.Pairwise.cocone U).ι.app o = CategoryTheory.Pairwise.coconeιApp U o
-- Mathlib.NumberTheory.Chebyshev
Nat.lcmUpto.eq_1 : ∀ (n : ℕ), n.lcmUpto = (Finset.Icc 1 n).lcm id
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.aleph0_toNat : Cardinal.toNat Cardinal.aleph0 = 0
-- Init.Data.List.Sublist
List.Sublist.subset : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₁ ⊆ l₂
-- Init.Notation
/-- Heterogeneous equality. `a ≍ b` asserts that `a` and `b` have the same
type, and casting `a` across the equality yields `b`, and vice versa.

You should avoid using this type if you can. Heterogeneous equality does not
have all the same properties as `Eq`, because the assumption that the types of
`a` and `b` are equal is often too weak to prove theorems of interest. One
public important non-theorem is the analogue of `congr`: If `f ≍ g` and `x ≍ y`
and `f x` and `g y` are well typed it does not follow that `f x ≍ g y`.
(This does follow if you have `f = g` instead.) However if `a` and `b` have
the same type then `a = b` and `a ≍ b` are equivalent.


Conventions for notations in identifiers:

 * The recommended spelling of `≍` in identifiers is `heq`. -/
«term_≍_» : Lean.TrailingParserDescr
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.Node.atom : Mathlib.Tactic.Widget.StringDiagram.AtomNode → Mathlib.Tactic.Widget.StringDiagram.Node
-- Mathlib.Algebra.Order.UpperLower
upperClosure_add_distrib : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α] (s t : Set α),
  upperClosure (s + t) = upperClosure s + upperClosure t
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- The type of lifts of  `S ⊗[R] M` to a polynomial ring.  -/
PolynomialLaw.lifts : (R : Type u) →
  [inst : CommSemiring R] →
    (M : Type u_1) → [inst_1 : AddCommMonoid M] → [Module R M] → Type v → Type (max (max u_1 u) v)
-- Aesop.RuleSet
Aesop.instInhabitedBaseRuleSet.default : Aesop.BaseRuleSet
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonInlayHintClientCapabilities : Lean.FromJson Lean.Lsp.InlayHintClientCapabilities