mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.SInt.Basic
/-- Multiplies two word-sized signed integers, wrapping around on over- or underflow.  Usually accessed
via the `*` operator.

This function is overridden at runtime with an efficient implementation.
 -/
ISize.mul : ISize → ISize → ISize
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.algebraMapInv.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  TensorAlgebra.algebraMapInv = (TensorAlgebra.lift R) 0
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatchAt.sliceTo : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {startPos endPos : s.Pos}
  (h : String.Slice.Pattern.Model.IsLongestMatchAt pat startPos endPos) (p : s.Pos) (hp : endPos ≤ p),
  String.Slice.Pattern.Model.IsLongestMatchAt pat (p.sliceTo startPos ⋯) (p.sliceTo endPos hp)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.isChain_range : ∀ {α : Type u_2} [inst : Preorder α] (c : OmegaCompletePartialOrder.Chain α),
  IsChain (fun x1 x2 => x1 ≤ x2) (Set.range ⇑c)
-- Mathlib.Algebra.Group.Prod
/-- The equivalence between `(M × N) × P` and `M × (N × P)` is multiplicative.  -/
MulEquiv.prodAssoc : {M : Type u_3} →
  {N : Type u_4} →
    {P : Type u_5} →
      [inst : MulOneClass M] → [inst_1 : MulOneClass N] → [inst_2 : MulOneClass P] → (M × N) × P ≃* M × N × P
-- Mathlib.Algebra.Group.Commute.Units
AddCommute.addUnits_neg_left : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {u : AddUnits M}, AddCommute (↑u) a → AddCommute (↑(-u)) a
-- Init.Data.UInt.Lemmas
USize.add_mul : ∀ {a b c : USize}, (a + b) * c = a * c + b * c
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.concat.induct_unfolding : ∀ (p₂ : Lean.Grind.CommRing.Poly) (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Prop),
  (∀ (k : ℤ), motive (Lean.Grind.CommRing.Poly.num k) (p₂.addConst k)) →
    (∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
        motive p (p.concat p₂) →
          motive (Lean.Grind.CommRing.Poly.add k m p) (Lean.Grind.CommRing.Poly.add k m (p.concat p₂))) →
      ∀ (p₁ : Lean.Grind.CommRing.Poly), motive p₁ (p₁.concat p₂)
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- For nonzero `I, I'`, `val_v(I*I') = val_v(I) + val_v(I')`. If `I` or `I'` is zero, then
`val_v(I*I') = 0`.  -/
FractionalIdeal.count_mul' : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  (I I' : FractionalIdeal (nonZeroDivisors R) K) [inst_5 : Decidable (I ≠ 0 ∧ I' ≠ 0)],
  FractionalIdeal.count K v (I * I') =
    if I ≠ 0 ∧ I' ≠ 0 then FractionalIdeal.count K v I + FractionalIdeal.count K v I' else 0
-- Mathlib.Order.Filter.AtTopBot.Ring
/-- The monomial function `x^n` tends to `+∞` at `+∞` for any positive natural `n`.
A version for positive real powers exists as `tendsto_rpow_atTop`.  -/
Filter.tendsto_pow_atTop : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α] {n : ℕ},
  n ≠ 0 → Filter.Tendsto (fun x => x ^ n) Filter.atTop Filter.atTop
-- Mathlib.Algebra.Order.Group.Unbundled.Int
Int.sign_eq_ediv_abs' : ∀ (a : ℤ), a.sign = a / |a|
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.forIn'.loop.match_3.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (__do_lift : ForInStep β) →
      ((b : β) → motive (ForInStep.done b)) → ((b : β) → motive (ForInStep.yield b)) → motive __do_lift
-- Std.Http.Data.URI.Encoding
/-- A percent-encoded query string component with a compile-time proof that it contains only valid encoded
query characters. Extends `EncodedString` to support the '+' character for spaces, following the
application/x-www-form-urlencoded format.

This type is specifically designed for encoding query parameters where spaces can be represented as '+'
instead of "%20".
 -/
Std.Http.URI.EncodedQueryString : (UInt8 → Bool) → Type
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageDirection.noConfusionType : Sort v✝ → Lean.JsonRpc.MessageDirection → Lean.JsonRpc.MessageDirection → Sort v✝
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
inv_riemannZeta_eq_sub_mul : ∀ᶠ (s : ℂ) in nhdsWithin 1 {1}ᶜ, (riemannZeta s)⁻¹ = (s - 1) * (riemannZeta₁ s)⁻¹
-- Init.Data.Vector.Lemmas
Vector.zipIdx_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} (h : xs.size = n) (k : optParam ℕ 0),
  (Vector.mk xs h).zipIdx k = Vector.mk (xs.zipIdx k) ⋯
-- Mathlib.Topology.Order.Basic
nhds_basis_Ioo' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α},
  (∃ l, l < a) → (∃ u, a < u) → (nhds a).HasBasis (fun b => b.1 < a ∧ a < b.2) fun b => Set.Ioo b.1 b.2
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.neg_pi_lt_arg : ∀ (x : ℂ), -Real.pi < x.arg
-- Std.Sync.Channel
/-- A multi-producer multi-consumer FIFO channel that offers both bounded and unbounded buffering
and a synchronous API. This type acts as a convenient layer to use a channel in a blocking fashion
and is not actually different from the original channel.

If a channel needs to be closed to indicate some sort of completion event use
`Std.CloseableChannel.Sync` instead. Note that `Std.CloseableChannel.Sync` introduces a need for error
handling in some cases, thus `Std.Channel.Sync` is usually easier to use if applicable.
 -/
Std.Channel.Sync : Type → Type
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
UniqueMDiffWithinAt.inter' : ∀ {𝕜 : 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] {x : M} {s t : Set M},
  UniqueMDiffAt[s] x → t ∈ nhdsWithin x s → UniqueMDiffAt[s ∩ t] x
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : TopologicalSpace α] [inst_1 : Preorder α]
  [inst_2 : TopologicalSpace β] [inst_3 : Preorder β] [inst_4 : TopologicalSpace γ] [inst_5 : Preorder γ]
  [inst_6 : TopologicalSpace δ] [inst_7 : Preorder δ] (h : EsakiaHom γ δ) (g : EsakiaHom β γ) (f : EsakiaHom α β),
  (h.comp g).comp f = h.comp (g.comp f)
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.toLp_add : ∀ (p : ENNReal) {V : Type u_4} [inst : AddCommGroup V] (x y : V),
  WithLp.toLp p (x + y) = WithLp.toLp p x + WithLp.toLp p y
-- Mathlib.CategoryTheory.Limits.FinallySmall
/-- An arbitrarily chosen initial functor `InitialModel J ⥤ J`.  -/
CategoryTheory.fromInitialModel : (J : Type u) →
  [inst : CategoryTheory.Category.{v, u} J] →
    [inst_1 : CategoryTheory.InitiallySmall J] → CategoryTheory.Functor (CategoryTheory.InitialModel J) J
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.instIsCentralScalar : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] {S : Type u_10} [inst_7 : TopologicalSpace W] [inst_8 : Monoid S]
  [inst_9 : DistribMulAction S W] [inst_10 : SMulCommClass R S W] [inst_11 : ContinuousConstSMul S W]
  [inst_12 : DistribMulAction Sᵐᵒᵖ W] [inst_13 : IsCentralScalar S W], IsCentralScalar S (P →ᴬ[R] W)
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.tag_mem : ∀ {ι : Type u_1} (n : ℕ) [inst : NeZero n] (ν : ι → ℤ),
  BoxIntegral.unitPartition.tag n ν ∈ BoxIntegral.unitPartition.box n ν
-- Mathlib.LinearAlgebra.Complex.Module
/-- Linear map version of the real part function, from `ℂ` to `ℝ`.  -/
Complex.reLm : ℂ →ₗ[ℝ] ℝ
-- Mathlib.Algebra.Homology.QuasiIso
QuasiIsoAt.congr_simp : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c}
  (f f_1 : K ⟶ L),
  f = f_1 →
    ∀ (i i_1 : ι) (e_i : i = i_1) [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i],
      QuasiIsoAt f i = QuasiIsoAt f_1 i_1
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
AddGroup.addRightReflectLT_of_addRightStrictMono : ∀ {N : Type u_2} [inst : AddGroup N] [inst_1 : LT N] [AddRightStrictMono N], AddRightReflectLT N
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.coe_one : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α], ⇑1 = id
-- Mathlib.Combinatorics.Graph.Simple
Graph.toSimpleGraph_adj : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β) (u v : ↑G.vertexSet), G.toSimpleGraph.Adj u v = (u ≠ v ∧ G.Adj ↑u ↑v)
-- Init.Data.Vector.Extract
Vector.extract_add_left : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j k : ℕ},
  xs.extract (i + j) k = Vector.cast ⋯ ((xs.extract i k).extract j (k - i))
-- Mathlib.Algebra.GroupWithZero.Action.Pi
Pi.mulDistribMulAction' : {I : Type u} →
  {f : I → Type v} →
    {g : I → Type u_1} →
      {m : (i : I) → Monoid (f i)} →
        {n : (i : I) → Monoid (g i)} →
          [(i : I) → MulDistribMulAction (f i) (g i)] → MulDistribMulAction ((i : I) → f i) ((i : I) → g i)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
CategoryTheory.Adjunction.ofCat_counit : ∀ {C D : CategoryTheory.Cat} {F : C ⟶ D} {G : D ⟶ C} (adj : CategoryTheory.Bicategory.Adjunction F G),
  (CategoryTheory.Adjunction.ofCat adj).counit = adj.counit.toNatTrans
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_diff_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {k : α}, k ∈ t₂ → Std.DTreeMap.Const.get! (t₁ \ t₂) k = default
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.ne_bot_iff : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p : Submodule R M), p ≠ ⊥ ↔ ∃ x ∈ p, x ≠ 0
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
MeasureTheory.TendstoInMeasure.congr_left : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : EDist E]
  {l : Filter ι} {f f' : ι → α → E} {g : α → E},
  (∀ (i : ι), f i =ᵐ[μ] f' i) → MeasureTheory.TendstoInMeasure μ f l g → MeasureTheory.TendstoInMeasure μ f' l g
-- Mathlib.Topology.Algebra.Monoid
ContinuousMap.addLeft.eq_1 : ∀ {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : Add X] [inst_2 : SeparatelyContinuousAdd X] (x : X),
  ContinuousMap.addLeft x = { toFun := fun x_1 => x + x_1, continuous_toFun := ⋯ }
-- Mathlib.Logic.Equiv.Basic
/-- Transport dependent functions through
an equivalence of the base spaces and a family
of equivalences of the matching fibres.
 -/
Equiv.piCongr' : {α : Sort u_1} →
  {β : Sort u_4} →
    {W : α → Sort w} →
      {Z : β → Sort z} → (h₁ : α ≃ β) → ((b : β) → W (h₁.symm b) ≃ Z b) → ((a : α) → W a) ≃ ((b : β) → Z b)
-- Init.Omega.IntList
Lean.Omega.IntList.smul_def : ∀ (xs : Lean.Omega.IntList) (i : ℤ), i * xs = List.map (fun x => i * x) xs
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.getCast.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α)
  (l l_1 : Std.DHashMap.Internal.AssocList α β) (e_l : l = l_1)
  (a_1 : Std.DHashMap.Internal.AssocList.contains a l = true),
  Std.DHashMap.Internal.AssocList.getCast a l a_1 = Std.DHashMap.Internal.AssocList.getCast a l_1 ⋯
-- Init.WF
PSigma.RevLex : {α : Sort u} → {β : Sort v} → (α → α → Prop) → (β → β → Prop) → (_ : α) ×' β → (_ : α) ×' β → Prop
-- Mathlib.NumberTheory.Real.GoldenRatio
/-- Relationship between the Fibonacci Sequence, exponents of the golden ratio,
and its conjugate.  -/
Real.fib_succ_sub_goldenConj_mul_fib : ∀ (n : ℕ), ↑(Nat.fib (n + 1)) - Real.goldenConj * ↑(Nat.fib n) = Real.goldenRatio ^ n
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_le_size_insertManyIfNewUnit : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} {ρ : Type w}
  [inst_2 : ForIn Id ρ α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : ρ}, m.size ≤ (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l).size
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.instMonadicRightAdjointAlgebraForget : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (T : CategoryTheory.Monad C) → CategoryTheory.MonadicRightAdjoint T.forget
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.recv : {α : Type} → Std.CloseableChannel.Bounded✝ α → BaseIO (Task (Option α))
-- Mathlib.Order.BooleanAlgebra.Defs
/-- A generalized Boolean algebra is a distributive lattice with `⊥` and a relative complement
operation `\` (called `sdiff`, after "set difference") satisfying `(a ⊓ b) ⊔ (a \ b) = a` and
`(a ⊓ b) ⊓ (a \ b) = ⊥`, i.e. `a \ b` is the complement of `b` in `a`.

This is a generalization of Boolean algebras which applies to `Finset α` for arbitrary
(not-necessarily-`Fintype`) `α`.  -/
GeneralizedBooleanAlgebra : Type u → Type u
-- Mathlib.Combinatorics.SetFamily.Compression.UV
UV.sup_sdiff_mem_of_mem_compression_of_notMem : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  {s : Finset α} {u v a : α} [inst_3 : DecidableEq α], a ∈ UV.compression u v s → a ∉ s → (a ⊔ v) \ u ∈ s
-- Mathlib.Analysis.Analytic.CPolynomialDef
HasFiniteFPowerSeriesOnBall.mono : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r r' : ENNReal} {n : ℕ},
  HasFiniteFPowerSeriesOnBall f p x n r → 0 < r' → r' ≤ r → HasFiniteFPowerSeriesOnBall f p x n r'
-- Mathlib.Analysis.Calculus.Deriv.Add
derivWithin_const_add_fun : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} (c : F), (derivWithin fun x => c + f x) = derivWithin f
-- Mathlib.Tactic.DefEqAbuse
/-- The continuation for `visitTraceNodesM`; this is mainly for readability (takes only one
argument in source).  -/
_private.Mathlib.Tactic.DefEqAbuse.0.Lean.MessageData.visitTraceNodesM.go : {m : Type → Type} →
  [Monad m] →
    {α : Type} →
      (Lean.TraceData → Lean.MessageData → Array Lean.MessageData → m (Lean.MessageData.VisitStep✝ α)) →
        α → (α → α → α) → Lean.MessageData → m α
-- Mathlib.Topology.Piecewise
continuous_piecewise : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s : Set α}
  [inst_2 : (a : α) → Decidable (a ∈ s)],
  (∀ a ∈ frontier s, f a = g a) →
    ContinuousOn f (closure s) → ContinuousOn g (closure sᶜ) → Continuous (s.piecewise f g)
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
ContinuousMap.comp_attachBound_mem_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)) (f : ↥A)
  (p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)), p.comp (↑f).attachBound ∈ A.topologicalClosure
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.insertMany_empty_list_nil : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α},
  ↑(Std.DTreeMap.Internal.Impl.empty.insertMany [] ⋯) = Std.DTreeMap.Internal.Impl.empty
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
/-- the class of weak equivalences  -/
HomotopicalAlgebra.CategoryWithWeakEquivalences.weakEquivalences : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    [self : HomotopicalAlgebra.CategoryWithWeakEquivalences C] → CategoryTheory.MorphismProperty C
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.Colorable.card_le_of_pairwise_adj : ∀ {V : Type u} {G : SimpleGraph V} {n : ℕ} {ι : Type u_1},
  G.Colorable n → ∀ (f : ι → V), (Pairwise fun i j => G.Adj (f i) (f j)) → Nat.card ι ≤ n
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.monadMap_ExceptT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε : Type u}
  (f : {β : Type u} → m β → m β) {α : Type u} (x : ExceptT ε m α) (post : α → Pred)
  (epost : EPost.Cons✝ (ε → Pred) EPred),
  ⦃ Std.Internal.Do.wp (f x.run) (Std.Internal.Do.EPost.Cons.pushExcept post epost) epost.tail ⦄
    MonadFunctor.monadMap (fun {β} => f) x ⦃ post; epost ⦄
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.cyclesOpIso_inv_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ).op S₁.cyclesOpIso.inv =
    CategoryTheory.CategoryStruct.comp S₂.cyclesOpIso.inv
      (CategoryTheory.ShortComplex.cyclesMap (CategoryTheory.ShortComplex.opMap φ))
-- Std.Http.Data.URI.Basic
/-- Proposition that asserts `s` is a valid dot-separated domain name.
Each label must satisfy `IsValidDomainLabel`, and the full name must be at most 255 characters.
 -/
Std.Http.URI.IsValidDomainName : String → Prop
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.evalWhiskerRightAux_of : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {f g : C}
  (η : f ⟶ g) (h : C),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight η h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorObj f h)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight η h)
        (CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorObj g h)).hom)
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `B` are linearly disjoint and such that `A.toSubalgebra ⊔ B.toSubalgebra = ⊤`,
then any `F`-basis of `B` is also an `A`-basis of `E`.
Note that the condition `A.toSubalgebra ⊔ B.toSubalgebra = ⊤` is equivalent to
`A ⊔ B = ⊤` in many cases, see `IntermediateField.sup_toSubalgebra_of_isAlgebraic_right` and similar
results.
 -/
IntermediateField.LinearDisjoint.basisOfBasisRight : {F : Type u} →
  {E : Type v} →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          {A B : IntermediateField F E} →
            A.LinearDisjoint ↥B →
              A.toSubalgebra ⊔ B.toSubalgebra = ⊤ → {ι : Type u_1} → Module.Basis ι F ↥B → Module.Basis ι (↥A) E
-- Std.Time.Zoned.TimeZone
/-- Creates a `Timestamp` from a given number of second.
 -/
Std.Time.TimeZone.ofSeconds : String → String → Std.Time.Second.Offset → optParam Bool false → Std.Time.TimeZone
-- Mathlib.Tactic.SetNotationForOrder
/-- Declare `∀ x ⊆ y, ...` as syntax for `∀ x, x ⊆ y → ...` and `∃ x ⊆ y, ...` as syntax for
`∃ x, x ⊆ y ∧ ...`  -/
Mathlib.Meta.SetNotationForOrder.«binderPred⊆_» : Lean.ParserDescr
-- Mathlib.Algebra.Order.Monoid.Units
AddUnits.orderEmbeddingVal.eq_1 : ∀ {α : Type u_1} [inst : AddMonoid α] [inst_1 : LinearOrder α],
  AddUnits.orderEmbeddingVal = { toFun := AddUnits.val, inj' := ⋯, map_rel_iff' := ⋯ }
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mapIsometry.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (f : X ≃ᵢ Y),
  Delone.DeloneSet.mapIsometry f =
    {
      toFun := fun D =>
        (Delone.DeloneSet.mapBilipschitz f.toEquiv 1 1 Delone.DeloneSet.mapIsometry._proof_1
              Delone.DeloneSet.mapIsometry._proof_1 ⋯ ⋯ D).copy
          (⇑f '' D.carrier) D.packingRadius D.coveringRadius ⋯ ⋯ ⋯,
      invFun := fun D =>
        (Delone.DeloneSet.mapBilipschitz f.symm.toEquiv 1 1 Delone.DeloneSet.mapIsometry._proof_1
              Delone.DeloneSet.mapIsometry._proof_1 ⋯ ⋯ D).copy
          (⇑f.symm '' D.carrier) D.packingRadius D.coveringRadius ⋯ ⋯ ⋯,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Data.Set.Card
Set.ncard_inter_add_ncard_union : ∀ {α : Type u_1} (s t : Set α),
  autoParam s.Finite Set.ncard_inter_add_ncard_union._auto_1 →
    autoParam t.Finite Set.ncard_inter_add_ncard_union._auto_3 → (s ∩ t).ncard + (s ∪ t).ncard = s.ncard + t.ncard
-- Mathlib.Topology.Algebra.Star.LinearMap
ContinuousLinearMap.intrinsicStar_comp : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : InvolutiveStar R]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : StarAddMonoid E] [inst_5 : StarModule R E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module R F] [inst_8 : StarAddMonoid F] [inst_9 : StarModule R F]
  [inst_10 : TopologicalSpace E] [inst_11 : TopologicalSpace F] [inst_12 : ContinuousStar E]
  [inst_13 : ContinuousStar F] {G : Type u_4} [inst_14 : AddCommMonoid G] [inst_15 : Module R G]
  [inst_16 : StarAddMonoid G] [inst_17 : StarModule R G] [inst_18 : TopologicalSpace G] [inst_19 : ContinuousStar G]
  (f : WithConv (E →L[R] F)) (g : WithConv (G →L[R] E)),
  star (WithConv.toConv (f.ofConv ∘SL g.ofConv)) = WithConv.toConv ((star f).ofConv ∘SL (star g).ofConv)
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.Icc_subset_uIcc : ∀ {α : Type u_1} [inst : Lattice α] {a b : α}, Set.Icc a b ⊆ Set.uIcc a b
-- Mathlib.Algebra.Group.Defs
npowRec'_mul_comm : ∀ {M : Type u_2} [inst : Semigroup M] [inst_1 : One M] {k : ℕ}, k ≠ 0 → ∀ (m : M), m * npowRec' k m = npowRec' k m * m
-- Std.Time.Date.Unit.Week
Std.Time.Week.instDecidableEqOffset : DecidableEq Std.Time.Week.Offset
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
/-- The obvious equivalence `ShortComplex (J ⥤ C) ≌ J ⥤ ShortComplex C`.  -/
CategoryTheory.ShortComplex.functorEquivalence : (J : Type u_1) →
  (C : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          CategoryTheory.ShortComplex (CategoryTheory.Functor J C) ≌
            CategoryTheory.Functor J (CategoryTheory.ShortComplex C)
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Roc.toArray_iter_eq_toArray : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_4 : Std.Rxc.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Roc α}, r.iter.toArray = r.toArray
-- Init.Data.String.Defs
/-- `pos.IsAtEnd` is just shorthand for `pos = s.endPos` that is easier to write if `s` is long.
 -/
String.Pos.IsAtEnd : {s : String} → s.Pos → Prop
-- Mathlib.RepresentationTheory.Invariants
Representation.linHom.mem_invariants_iff_comm : ∀ {k : Type u} [inst : CommRing k] {G : Type v} [inst_1 : Group G] {X Y : Rep.{w, u, v} k G} (f : ↑X →ₗ[k] ↑Y) (g : G),
  ((X.ρ.linHom Y.ρ) g) f = f ↔ f ∘ₗ X.ρ g = Y.ρ g ∘ₗ f
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_restrict : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) {p : Submodule R M} {q : Submodule R₂ M₂} (h : ∀ x ∈ p, f x ∈ q),
  (f.restrict h).range = Submodule.comap q.subtype (Submodule.map f p)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- The colimit cocone exhibiting `⨁ Subtype.restrict pᶜ f` as the cokernel of
`biproduct.fromSubtype f p`  -/
CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {K : Type} →
        [inst_2 : Finite K] →
          [inst_3 : CategoryTheory.Limits.HasFiniteBiproducts C] →
            (f : K → C) →
              (p : K → Prop) →
                CategoryTheory.Limits.ColimitCocone
                  (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.fromSubtype f p) 0)