mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] {δ : Type u_5} [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : TopologicalSpace δ] [inst_4 : Zero δ]
  (f : CompactlySupportedContinuousMap γ δ) (g : CocompactMap β γ) (h : CocompactMap α β),
  (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.Data.Quot
Quotient.instIsEquivEquiv : ∀ {α : Type u_4} [inst : Setoid α], IsEquiv α fun x1 x2 => x1 ≈ x2
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_relabelEquiv : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'} {g : α ≃ β} {k : ℕ}
  {φ : L.BoundedFormula α k} {v : β → M} {xs : Fin k → M},
  ((FirstOrder.Language.BoundedFormula.relabelEquiv g) φ).Realize v xs ↔ φ.Realize (v ∘ ⇑g) xs
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.realize_toPrenex : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {n : ℕ} [Nonempty M]
  (φ : L.BoundedFormula α n) {v : α → M} {xs : Fin n → M}, φ.toPrenex.Realize v xs ↔ φ.Realize v xs
-- Mathlib.LinearAlgebra.Dual.Basis
Module.DualBases.dual_lc : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {e : ι → M} {ε : ι → Module.Dual R M},
  Module.DualBases e ε → ∀ (l : ι →₀ R) (i : ι), (ε i) (Module.DualBases.lc e l) = l i
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct
SSet.instQuasicategoryObjIhom : ∀ {A X : SSet} [X.Quasicategory], (A ⟹ X).Quasicategory
-- Mathlib.Logic.Function.Basic
Function.Bijective.surjective : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Bijective f → Function.Surjective f
-- Mathlib.Algebra.BigOperators.Pi
/-- An 'unapplied' analogue of `Finset.prod_apply`.  -/
Finset.prod_fn : ∀ {α : Type u_7} {M : α → Type u_8} {ι : Type u_9} [inst : (a : α) → CommMonoid (M a)] (s : Finset ι)
  (g : ι → (a : α) → M a), ∏ c ∈ s, g c = fun a => ∏ c ∈ s, g c a
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.insert.match_3.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.eq with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_3 ()
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.IsIntegral.mem_minimalPrimes_map_under : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_3} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.IsIntegral R A] (I : Ideal A) [I.IsPrime], I ∈ (Ideal.map (algebraMap R A) (Ideal.under R I)).minimalPrimes
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.del.match_1.eq_5 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → RBTree.RBNode α → RBTree.RBColor → Sort u_2) (c : RBTree.RBColor)
  (a : RBTree.RBNode α) (y : α) (parent : RBTree.RBNode.Path α) (b : RBTree.RBNode α)
  (h_1 : (t : RBTree.RBNode α) → (x : RBTree.RBColor) → motive RBTree.RBNode.Path.root t x)
  (h_2 :
    (c : RBTree.RBColor) →
      (parent : RBTree.RBNode.Path α) →
        (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left c parent y b) a RBTree.RBColor.red)
  (h_3 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) →
        (y : α) →
          (parent : RBTree.RBNode.Path α) →
            (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right c a y parent) b RBTree.RBColor.red)
  (h_4 :
    (c : RBTree.RBColor) →
      (parent : RBTree.RBNode.Path α) →
        (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left c parent y b) a RBTree.RBColor.black)
  (h_5 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) →
        (y : α) →
          (parent : RBTree.RBNode.Path α) →
            (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right c a y parent) b RBTree.RBColor.black),
  (match RBTree.RBNode.Path.right c a y parent, b, RBTree.RBColor.black with
    | RBTree.RBNode.Path.root, t, x => h_1 t x
    | RBTree.RBNode.Path.left c parent y b, a, RBTree.RBColor.red => h_2 c parent y b a
    | RBTree.RBNode.Path.right c a y parent, b, RBTree.RBColor.red => h_3 c a y parent b
    | RBTree.RBNode.Path.left c parent y b, a, RBTree.RBColor.black => h_4 c parent y b a
    | RBTree.RBNode.Path.right c a y parent, b, RBTree.RBColor.black => h_5 c a y parent b) =
    h_5 c a y parent b
-- Init.Data.Int.DivMod.Lemmas
Int.sign_tdiv : ∀ (a b : ℤ), (a.tdiv b).sign = if a.natAbs < b.natAbs then 0 else a.sign * b.sign
-- Mathlib.RingTheory.Length
Submodule.length_quotient_lt : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsArtinian R M]
  [IsNoetherian R M] (p : Submodule R M), p ≠ ⊥ → Module.length R (M ⧸ p) < Module.length R M
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleMapOfLE : {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) →
                (A : C) →
                  (a b : ℤ) →
                    a ≤ b →
                      (CategoryTheory.Triangulated.TStructure.TruncAux.triangle✝ t a A ⟶
                        CategoryTheory.Triangulated.TStructure.TruncAux.triangle✝ t b A)
-- Std.Http.Data.Extensions
_private.Std.Http.Data.Extensions.0.Std.Http.Extensions.mk.inj : ∀ {data data_1 : Std.TreeMap Lean.Name Dynamic Std.Http.Extensions.compareName},
  { data := data } = { data := data_1 } → data = data_1
-- Init.Data.Nat.Gcd
Nat.gcd_div_gcd_div_gcd_of_pos_left : ∀ {n m : ℕ}, 0 < n → (n / n.gcd m).gcd (m / n.gcd m) = 1
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- The equivalence relation on vertices given by `SimpleGraph.Reachable`.  -/
SimpleGraph.reachableSetoid : {V : Type u} → SimpleGraph V → Setoid V
-- Mathlib.RingTheory.PicardGroup
instSmallUnitsSkeletonModuleCat : ∀ (R : Type u) [inst : CommRing R], Small.{u, u + 1} (CategoryTheory.Skeleton (ModuleCat R))ˣ
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.map_X : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁) (n : σ),
  (MvPolynomial.map f) (MvPolynomial.X n) = MvPolynomial.X n
-- Init.Data.SInt.Bitwise
Int16.and_not_self : ∀ {a : Int16}, a &&& ~~~a = 0
-- Mathlib.Algebra.Group.Submonoid.Units
ofAddUnits_addUnits_gc : ∀ {M : Type u_1} [inst : AddMonoid M], GaloisConnection AddSubgroup.ofAddUnits AddSubmonoid.addUnits
-- Mathlib.Data.List.Rotate
List.IsRotated.refl : ∀ {α : Type u} (l : List α), l ~r l
-- Init.Data.Int.LemmasAux
_private.Init.Data.Int.LemmasAux.0.Int.toNat.match_1.splitter : (motive : ℤ → Sort u_1) → (x : ℤ) → ((n : ℕ) → motive (Int.ofNat n)) → ((a : ℕ) → motive (Int.negSucc a)) → motive x
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.memLp_approxOn_range : ∀ {β : Type u_2} {E : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace E] [inst_2 : NormedAddCommGroup E]
  {p : ENNReal} [inst_3 : BorelSpace E] {f : β → E} {μ : MeasureTheory.Measure β} (fmeas : Measurable f)
  [inst_4 : TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {0})],
  MeasureTheory.MemLp f p μ →
    ∀ (n : ℕ), MeasureTheory.MemLp (⇑(MeasureTheory.SimpleFunc.approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n)) p μ
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `M` is flat, `N` is contained in `i(R)`, where `i : R → S` is the structure map,
then `M` and `N` are linearly disjoint.  -/
Submodule.LinearDisjoint.of_right_le_one_of_flat : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (M N : Submodule R S),
  N ≤ 1 → ∀ [Module.Flat R ↥M], M.LinearDisjoint N
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.isZero_spectralSequence_page_X_of_isZero_H' : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : X.HasSpectralSequence data] (r : ℤ) (hr : r₀ ≤ r) (pq : κ),
  CategoryTheory.Limits.IsZero
      ((X.H (data.deg pq)).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯))) →
    CategoryTheory.Limits.IsZero (((X.spectralSequence data).page r ⋯).X pq)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.InfiniteNeg.lt_zero : ∀ {x : ℝ*}, x.InfiniteNeg → x < 0
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithBot.instSupSet.eq_1 : ∀ {α : Type u_1} [inst : LE α] [inst_1 : SupSet α],
  WithBot.instSupSet = { sSup := fun S => if S ⊆ {⊥} ∨ ¬BddAbove S then ⊥ else ↑(sSup ((fun a => ↑a) ⁻¹' S)) }
-- Mathlib.Algebra.Group.Defs
/-- An additive magma which `IsMulCommutative` is a `AddCommMagma`.

This is primarily used to deduce the bundled version from the unbundled one for commutative
subobjects in a noncommutative ambient type. As such this is only available inside the
`IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
commutativity.

See note [commutative subobjects].  -/
IsAddCommutative.instAddCommMagma : {M : Type u_2} → [inst : Add M] → [IsAddCommutative M] → AddCommMagma M
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clearRatUnits.eq_1 : ∀ {n : ℕ} (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)))
  (rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments }.clearRatUnits =
    { clauses := clauses, rupUnits := rupUnits, ratUnits := #[],
      assignments := Array.foldl Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clearUnit assignments ratUnits }
-- Mathlib.Data.Set.Operations
Set.mem_prod_eq : ∀ {α : Type u} {β : Type v} {s : Set α} {t : Set β} {p : α × β}, (p ∈ s ×ˢ t) = (p.1 ∈ s ∧ p.2 ∈ t)
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.ker_mulVecLin_transpose_mul_self : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Fintype n] [inst_1 : Fintype m] [inst_2 : Field R]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] (A : Matrix m n R), (A.transpose * A).mulVecLin.ker = A.mulVecLin.ker
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.Measure.outerMeasure_le_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {m : MeasureTheory.OuterMeasure α},
  m ≤ μ.toOuterMeasure ↔ ∀ (s : Set α), MeasurableSet s → m s ≤ μ s
-- Mathlib.Algebra.FiniteSupport.Basic
/-- Eta-expanded form of `Function.HasFiniteSupport.sub` -/
Function.HasFiniteSupport.fun_sub : ∀ {α : Type u_1} {M : Type u_3} [inst : SubtractionMonoid M] {f g : α → M},
  Function.HasFiniteSupport f → Function.HasFiniteSupport g → Function.HasFiniteSupport fun i => f i - g i
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.notMem_top : ∀ {α : Type u_1} [inst : LE α] {a : α}, a ∉ ⊤
-- Lean.Elab.MutualInductive
Lean.Elab.Command.CtorView.mk.inj : ∀ {ref : Lean.Syntax} {modifiers : Lean.Elab.Modifiers} {declName : Lean.Name} {declId binders : Lean.Syntax}
  {type? : Option Lean.Syntax} {ref_1 : Lean.Syntax} {modifiers_1 : Lean.Elab.Modifiers} {declName_1 : Lean.Name}
  {declId_1 binders_1 : Lean.Syntax} {type?_1 : Option Lean.Syntax},
  { ref := ref, modifiers := modifiers, declName := declName, declId := declId, binders := binders, type? := type? } =
      { ref := ref_1, modifiers := modifiers_1, declName := declName_1, declId := declId_1, binders := binders_1,
        type? := type?_1 } →
    ref = ref_1 ∧
      modifiers = modifiers_1 ∧ declName = declName_1 ∧ declId = declId_1 ∧ binders = binders_1 ∧ type? = type?_1
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.prod_zero : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β), κ.prod 0 = 0
-- Mathlib.Analysis.Normed.Group.Basic
enorm_add_le_of_le : ∀ {E : Type u_8} [inst : TopologicalSpace E] [inst_1 : ESeminormedAddMonoid E] {r₁ r₂ : ENNReal} {a₁ a₂ : E},
  ‖a₁‖ₑ ≤ r₁ → ‖a₂‖ₑ ≤ r₂ → ‖a₁ + a₂‖ₑ ≤ r₁ + r₂
-- Mathlib.Geometry.Euclidean.Circumcenter
_private.Mathlib.Geometry.Euclidean.Circumcenter.0.Affine.Simplex.instFintypePointsWithCircumcenterIndex.match_5.eq_1 : ∀ (n : ℕ) (motive : Affine.Simplex.PointsWithCircumcenterIndex n → Sort u_1) (a : Fin (n + 1))
  (h_1 : (a : Fin (n + 1)) → motive (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a))
  (h_2 : Unit → motive Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex),
  (match Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a with
    | Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a => h_1 a
    | Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex => h_2 ()) =
    h_1 a
-- Mathlib.Order.OrderDual
OrderDual.toDual_symm_eq : ∀ {α : Type u_1}, OrderDual.toDual.symm = OrderDual.ofDual
-- Mathlib.Data.ENNReal.Basic
ENNReal.forall_ennreal : ∀ {p : ENNReal → Prop}, (∀ (a : ENNReal), p a) ↔ (∀ (r : NNReal), p ↑r) ∧ p ⊤
-- Mathlib.Analysis.InnerProductSpace.Reproducing
/-- The kernel of the reproducing kernel Hilbert space
generated by a positive semidefinite matrix is the original positive semidefinite matrix.
 -/
RKHS.OfKernel.kernel_ofKernel : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : CompleteSpace V] {K : Matrix X X (V →L[𝕜] V)} [inst_4 : Fact K.PosSemidef],
  RKHS.kernel (RKHS.OfKernel K) = K
-- Mathlib.Order.Irreducible
infIrred_ofDual : ∀ {α : Type u_2} [inst : SemilatticeInf α] {a : αᵒᵈ}, InfIrred (OrderDual.ofDual a) ↔ SupIrred a
-- Mathlib.LinearAlgebra.Basis.SMul
/-- The action on a `Basis` by acting on each element.

See also `Basis.unitsSMul` and `Basis.groupSMul`, for the cases when a different action is applied
to each basis element.  -/
Module.Basis.instSMul : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_4} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            {G : Type u_5} →
              [inst_3 : Group G] → [inst_4 : DistribMulAction G M] → [SMulCommClass G R M] → SMul G (Module.Basis ι R M)
-- Mathlib.Tactic.Ring.RingNF
/-- `ring_nf` simplifies expressions in the language of commutative (semi)rings,
which rewrites all ring expressions into a normal form, allowing variables in the exponents.

`ring_nf` works as both a tactic and a conv tactic.

See also the `ring` tactic for solving a goal which is an equation in the language
of commutative (semi)rings.

* `ring_nf!` will use a more aggressive reducibility setting to identify atoms.
* `ring_nf (config := cfg)` allows for additional configuration (see `RingNF.Config`):
  * `red`: the reducibility setting (overridden by `!`)
  * `zetaDelta`: if true, local let variables can be unfolded (overridden by `!`)
  * `recursive`: if true, `ring_nf` will also recurse into atoms
* `ring_nf at l1 l2 ...` can be used to rewrite at the given locations.

Examples:
This can be used non-terminally to normalize ring expressions in the goal such as
`⊢ P (x + x + x)` ~> `⊢ P (x * 3)`, as well as being able to prove some equations that
`ring` cannot because they involve ring reasoning inside a subterm, such as
`sin (x + y) + sin (y + x) = 2 * sin (x + y)`.
 -/
Mathlib.Tactic.RingNF.ringNFConv : Lean.ParserDescr
-- Init.Data.UInt.Lemmas
USize.lt_of_lt_of_le : ∀ {a b c : USize}, a < b → b ≤ c → a < c
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.prod.instIsAddLeftInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Add G] {μ : MeasureTheory.Measure G} [MeasurableAdd G]
  [μ.IsAddLeftInvariant] [MeasureTheory.SFinite μ] {H : Type u_3} [inst_5 : Add H] {mH : MeasurableSpace H}
  {ν : MeasureTheory.Measure H} [MeasurableAdd H] [ν.IsAddLeftInvariant] [MeasureTheory.SFinite ν],
  (μ.prod ν).IsAddLeftInvariant
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.ExprCnstr.toPoly_norm_eq : ∀ (c : Nat.Internal.Linear.ExprCnstr), c.toPoly.norm = c.toNormPoly
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.lintegral_singleton : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasurableSingletonClass α] (f : α → ENNReal)
  (a : α), ∫⁻ (x : α) in {a}, f x ∂μ = f a * μ {a}
-- Mathlib.Algebra.BigOperators.Group.List.Defs
List.prod_eq_pow_card : ∀ {M : Type u_2} [inst : Monoid M] (l : List M) (m : M), (∀ x ∈ l, x = m) → l.prod = m ^ l.length
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities.mk : Option Lean.Lsp.TextDocumentSyncOptions →
  Option Lean.Lsp.CompletionOptions →
    Bool →
      Bool →
        Bool →
          Bool →
            Bool →
              Bool →
                Bool →
                  Bool →
                    Option Lean.Lsp.RenameOptions →
                      Bool →
                        Bool →
                          Option Lean.Lsp.SemanticTokensOptions →
                            Option Lean.Lsp.CodeActionOptions →
                              Option Lean.Lsp.InlayHintOptions →
                                Option Lean.Lsp.SignatureHelpOptions →
                                  Option Lean.Lsp.DocumentColorOptions →
                                    Option Lean.Lsp.LeanServerCapabilities → Lean.Lsp.ServerCapabilities
-- Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
/-- Morphisms obtained using an exponentiable object.  -/
CategoryTheory.CartesianClosed.«term_⟹_» : Lean.TrailingParserDescr
-- Init.Data.List.Basic
List.nil_zipWithAll : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : Option α → Option α_1 → α_2} {bs : List α_1},
  List.zipWithAll f [] bs = List.map (fun b => f none (some b)) bs
-- Mathlib.Topology.MetricSpace.Algebra
Bornology.IsBounded.uniformContinuousOn_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero α]
  [inst_3 : Zero β] [inst_4 : SMul α β] [IsBoundedSMul α β] {s : Set (α × β)},
  Bornology.IsBounded s → UniformContinuousOn (Function.uncurry fun x1 x2 => x1 • x2) s
-- Mathlib.Order.SuccPred.Limit
Order.IsPredLimit.pred_ne : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : PredOrder α] [NoMinOrder α],
  Order.IsPredLimit a → ∀ (b : α), Order.pred b ≠ a
-- Mathlib.Topology.Covering.Quotient
Topology.IsQuotientMap.isQuotientCoveringMap_of_subgroupOp : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X},
  Topology.IsQuotientMap f →
    ∀ [inst_2 : Group E] [IsTopologicalGroup E] (G : Subgroup E),
      IsDiscrete ↑G → (∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁⁻¹ * e₂ ∈ G) → IsQuotientCoveringMap f ↥G.op
-- Std.Http.Data.URI.Basic
/-- Checks whether a single domain label is valid. A label must be non-empty, contain only ASCII
alphanumeric characters and `-`, cannot start or end with `-`, and must be at most 63 characters.

References:
* https://www.rfc-editor.org/rfc/rfc1034.html#section-3.5
* https://www.rfc-editor.org/rfc/rfc1123.html#section-2.1
 -/
Std.Http.URI.isValidDomainLabel : String → Bool
-- Lean.Meta.HasNotBit
Lean.isHasNotBit? : Lean.Expr → Option Lean.Expr
-- Lean.Meta.Tactic.Grind.Util
Lean.Meta.Grind.isPreMatchCond : Lean.Expr → Bool
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Adjunction.mapGrp_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (a : F ⊣ G) [inst_4 : F.Monoidal]
  [inst_5 : G.Monoidal],
  a.mapGrp.counit =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.mapGrpCompIso.inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapGrpNatTrans a.counit)
        CategoryTheory.Functor.mapGrpIdIso.hom)
-- Mathlib.Topology.Algebra.Module.LocallyConvex
locallyConvexSpace_iff_exists_convex_subset_zero : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E],
  LocallyConvexSpace 𝕜 E ↔ ∀ U ∈ nhds 0, ∃ S ∈ nhds 0, Convex 𝕜 S ∧ S ⊆ U
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.instUniqueOfIsEmpty : {V : Type u_2} → [IsEmpty V] → Unique (Digraph V)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift
AffineSubspace.shift_one : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : AddTorsor V P]
  [inst_3 : Module k V] (s : AffineSubspace k P) (c : P), s.shift c 1 = s
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.mk.sizeOf_spec : ∀ {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₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  [inst_2 : SizeOf C] (φK : h₁.K ⟶ h₂.K) (φH : h₁.H ⟶ h₂.H)
  (commi :
    autoParam (CategoryTheory.CategoryStruct.comp φK h₂.i = CategoryTheory.CategoryStruct.comp h₁.i φ.τ₂)
      CategoryTheory.ShortComplex.LeftHomologyMapData.commi._autoParam)
  (commf' :
    autoParam (CategoryTheory.CategoryStruct.comp h₁.f' φK = CategoryTheory.CategoryStruct.comp φ.τ₁ h₂.f')
      CategoryTheory.ShortComplex.LeftHomologyMapData.commf'._autoParam)
  (commπ :
    autoParam (CategoryTheory.CategoryStruct.comp h₁.π φH = CategoryTheory.CategoryStruct.comp φK h₂.π)
      CategoryTheory.ShortComplex.LeftHomologyMapData.commπ._autoParam),
  sizeOf { φK := φK, φH := φH, commi := commi, commf' := commf', commπ := commπ } =
    1 + sizeOf φK + sizeOf φH + sizeOf commi + sizeOf commf' + sizeOf commπ
-- Mathlib.RingTheory.SimpleModule.Isotypic
/-- If an `R`-module `M` is the direct sum of fully invariant submodules `Nᵢ`,
then `End R M` is isomorphic to `Πᵢ End R Nᵢ` as a ring.  -/
iSupIndep.ringEquiv : {R : Type u_2} →
  {M : Type u} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {ι : Type u_5} →
            [DecidableEq ι] →
              {N : ι → Submodule R M} →
                iSupIndep N →
                  ⨆ i, N i = ⊤ →
                    (∀ (i : ι), (N i).IsFullyInvariant) → Module.End R M ≃+* ((i : ι) → Module.End R ↥(N i))
-- Mathlib.CategoryTheory.Monad.EquivMon
CategoryTheory.Monad.monadMonEquiv_counitIso_inv_app_hom : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (x : CategoryTheory.Mon (CategoryTheory.Functor C C)),
  ((CategoryTheory.Monad.monadMonEquiv C).counitIso.inv.app x).hom =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Functor.id (CategoryTheory.Mon (CategoryTheory.Functor C C))).obj x).X
-- Mathlib.Control.Monad.Cont
WriterT.goto_mkLabel : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type u_1} {β ω : Type u} [inst_1 : EmptyCollection ω]
  (x : MonadCont.Label (α × ω) m β) (i : α), MonadCont.goto (WriterT.mkLabel x) i = monadLift (MonadCont.goto x (i, ∅))
-- Mathlib.Topology.Compactness.Compact
nhdsSet_prod_le_of_disjoint_cocompact : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : Filter Y},
  IsCompact s → Disjoint f (Filter.cocompact Y) → nhdsSet s ×ˢ f ≤ nhdsSet (s ×ˢ Set.univ)
-- Mathlib.Order.Heyting.Hom
HeytingHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β]
  [inst_2 : HeytingAlgebra γ] {f₁ f₂ : HeytingHom α β} {g : HeytingHom β γ},
  Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)