mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.instIsLeftAdjointOverTopMapOfHasPullbacksAlongOfIsStableUnderBaseChangeAlong : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {X Y : T}
  [inst_1 : P.IsStableUnderComposition] (f : X ⟶ Y) [P.HasPullbacksAlong f] [P.IsStableUnderBaseChangeAlong f]
  (hPf : P f), (CategoryTheory.MorphismProperty.Over.map ⊤ hPf).IsLeftAdjoint
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.centerToMulOpposite_symm_apply_coe : ∀ {R : Type u} [inst : NonAssocRing R] (r : ↥(Subsemigroup.center Rᵐᵒᵖ)),
  ↑(Subring.centerToMulOpposite.symm r) = MulOpposite.unop ↑r
-- Mathlib.Tactic.FastInstance
/-- `inferInstanceAs% A` is shorthand for `fast_instance% inferInstanceAs A`.
This is preferred over `inferInstanceAs` when the instance can be reduced to
constructor applications. In that case, the parameters of the constructors will be filled in
using the expected type, so that the instance will unfold nicely during unification.  -/
Mathlib.Elab.FastInstance.«termInferInstanceAs%_» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso'_inv_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  [inst_4 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.Arrow C) {I : C}
  (i : CategoryTheory.Limits.IsInitial I) {W : C},
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIso' X i).inv.left = ⋯.isoPushout.hom
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_inv : ∀ {x : ℝ}, x⁻¹.toNNReal = x.toNNReal⁻¹
-- Mathlib.Data.Set.Prod
Set.prod_mono : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β}, s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ×ˢ t₁ ⊆ s₂ ×ˢ t₂
-- Mathlib.Order.ModularLattice
inf_covBy_of_covBy_sup_right : ∀ {α : Type u_1} [inst : Lattice α] [IsLowerModularLattice α] {a b : α}, b ⋖ a ⊔ b → a ⊓ b ⋖ a
-- Mathlib.RingTheory.Radical.NatInt
Nat.radical_eq_one_iff : ∀ {n : ℕ}, UniqueFactorizationMonoid.radical n = 1 ↔ n ≤ 1
-- Lean.Declaration
Lean.instBEqDefinitionSafety.beq : Lean.DefinitionSafety → Lean.DefinitionSafety → Bool
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The Hausdorff edistance between sets or their closures is the same.  -/
Metric.hausdorffEDist_closure : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
  Metric.hausdorffEDist (closure s) (closure t) = Metric.hausdorffEDist s t
-- Mathlib.Data.Set.Lattice.Image
Set.prod_iInter : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {s : Set α} {t : ι → Set β} [hι : Nonempty ι],
  s ×ˢ ⋂ i, t i = ⋂ i, s ×ˢ t i
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
/-- The topology of bounded convergence is stronger than the topology of pointwise convergence.  -/
ContinuousLinearMap.toPointwiseConvergenceCLM : {𝕜₁ : Type u_4} →
  (𝕜₂ : Type u_5) →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        (σ : 𝕜₁ →+* 𝕜₂) →
          (E : Type u_7) →
            (F : Type u_8) →
              [inst_2 : AddCommGroup E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : TopologicalSpace F] →
                      [inst_6 : IsTopologicalAddGroup F] →
                        [inst_7 : Module 𝕜₁ E] →
                          [inst_8 : Module 𝕜₂ F] →
                            [ContinuousSMul 𝕜₁ E] →
                              [inst_10 : ContinuousConstSMul 𝕜₂ F] → (E →SL[σ] F) →L[𝕜₂] E →SLₚₜ[σ] F
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.coeffs_subset_range : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P : Algebra.Presentation R S ι σ} (R₀ : Type u_5) [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S] [P.HasCoeffs R₀],
  P.coeffs ⊆ Set.range ⇑(algebraMap R₀ R)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_eq_one_iff_of_one_le' : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : PartialOrder N] {f : ι → N} {s : Finset ι}
  [MulLeftMono N], (∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)
-- Mathlib.Order.WithBot
WithBot.total_le : ∀ {α : Type u_1} [inst : LE α] [Std.Total fun x1 x2 => x1 ≤ x2], Std.Total fun x1 x2 => x1 ≤ x2
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k a : α},
  (t.insert k).get! a = if cmp k a = Ordering.eq ∧ k ∉ t then k else t.get! a
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.upperBound?_mem_toList : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α} {t : RBTree.RBSet α cmp}, t.upperBound? x = some y → y ∈ t.toList
-- Mathlib.Analysis.Normed.Group.Pointwise
sphere_add_singleton : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x y : E), Metric.sphere x δ + {y} = Metric.sphere (x + y) δ
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
/-- **Alias** of `FourierTransform.fourierCLE_symm_apply`. -/
SchwartzMap.fourierTransformCLE_symm_apply : ∀ {R : Type u_5} {E : Type u_6} {F : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : FourierTransform E F] [inst_6 : FourierAdd E F]
  [inst_7 : FourierSMul R E F] [inst_8 : FourierTransformInv F E] [inst_9 : FourierPair E F]
  [inst_10 : FourierInvPair F E] [inst_11 : TopologicalSpace E] [inst_12 : TopologicalSpace F]
  [inst_13 : ContinuousFourier E F] [inst_14 : ContinuousFourierInv F E] (f : F),
  (FourierTransform.fourierCLE R E).symm f = FourierTransformInv.fourierInv f
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.IsHamiltonian.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a b : α} (p : G.Walk a b),
  p.IsHamiltonian = ∀ (a_1 : α), List.count a_1 p.support = 1
-- Init.Data.UInt.Lemmas
UInt64.toUInt8_ofNatTruncate_of_le : ∀ {n : ℕ},
  UInt64.size ≤ n →
    (UInt64.ofNatClamp n).toUInt8 = UInt8.ofNatLT (UInt8.size - 1) UInt16.toUInt8_ofNatClamp_of_le._proof_1
-- Mathlib.Topology.MetricSpace.Bounded
Metric.hasBasis_cobounded_compl_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] (c : α),
  (Bornology.cobounded α).HasBasis (fun x => True) fun r => (Metric.ball c r)ᶜ
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- A sequence of simple functions such that `∀ x, Tendsto (fun n ↦ hf.approx n x) atTop (𝓝 (f x))`
and `∀ n, μ (support (hf.approx n)) < ∞`. These properties are given by
`FinStronglyMeasurable.tendsto_approx` and `FinStronglyMeasurable.fin_support_approx`.  -/
MeasureTheory.FinStronglyMeasurable.approx : {α : Type u_1} →
  {β : Type u_2} →
    {m0 : MeasurableSpace α} →
      {μ : MeasureTheory.Measure α} →
        {f : α → β} →
          [inst : Zero β] →
            [inst_1 : TopologicalSpace β] → MeasureTheory.FinStronglyMeasurable f μ → ℕ → MeasureTheory.SimpleFunc α β
-- Mathlib.GroupTheory.OrderOfElement
/-- The equivalence between `Fin (addOrderOf a)` and
`Subgroup.zmultiples a`, sending `i` to `i • a`.  -/
finEquivZMultiples : {G : Type u_1} → [inst : AddGroup G] → {x : G} → IsOfFinAddOrder x → Fin (addOrderOf x) ≃ ↥(AddSubgroup.zmultiples x)
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- **Alias** of `CategoryTheory.Functor.ReflectsEpimorphisms.of_iso`. -/
CategoryTheory.Functor.reflectsEpimorphisms.of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} [F.ReflectsEpimorphisms] (α : F ≅ G), G.ReflectsEpimorphisms
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.coe_fst : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W), ⇑(Representation.IntertwiningMap.fst A ρ σ) = Prod.fst
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.singularPart_le : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α), μ.singularPart ν ≤ μ
-- Mathlib.Order.Interval.Set.Image
Set.image_subtype_val_Ici_subset : ∀ {α : Type u_1} [inst : Preorder α] {p : α → Prop} (a : { x // p x }), Subtype.val '' Set.Ici a ⊆ Set.Ici ↑a
-- Init.Data.SInt.Lemmas
Int8.toInt8_toInt64 : ∀ (n : Int8), n.toInt64.toInt8 = n
-- Mathlib.Data.Seq.Computation
Computation.liftRel_congr : ∀ {α : Type u} {β : Type v} {R : α → β → Prop} {ca ca' : Computation α} {cb cb' : Computation β},
  ca.Equiv ca' → cb.Equiv cb' → (Computation.LiftRel R ca cb ↔ Computation.LiftRel R ca' cb')
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.sub_add_cancel_right : ∀ {α : Type u} [inst : SubtractionMonoid α] {b : α}, IsAddUnit b → ∀ (a : α), b - (a + b) = -a
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.addIndex_elim : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {K V : Set G},
  IsCompact K →
    (interior V).Nonempty → ∃ t, K ⊆ ⋃ g ∈ t, (fun h => g + h) ⁻¹' V ∧ t.card = MeasureTheory.Measure.haar.addIndex K V
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} {l : List α} {k : α}
  {h : k ∈ Std.DHashMap.Raw.Const.insertManyIfNewUnit m l},
  Std.DHashMap.Raw.Const.get (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l) k h = ()
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
/-- A morphism of schemes `f : X ⟶ Y` is smooth of relative dimension `n` if for each `x : X` there
exists an affine open neighborhood `V` of `x` and an affine open neighborhood `U` of
`f.base x` with `V ≤ f ⁻¹ᵁ U` such that the induced map `Γ(Y, U) ⟶ Γ(X, V)` is
standard smooth of relative dimension `n`.
 -/
AlgebraicGeometry.SmoothOfRelativeDimension : ℕ → {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
/-- The complex sine function is everywhere strictly differentiable, with the derivative `cos x`.  -/
Complex.hasStrictDerivAt_sin : ∀ (x : ℂ), HasStrictDerivAt Complex.sin (Complex.cos x) x
-- Lean.Linter.Util
/-- Get the `parentDecl`s of every elaborated body in the infotree.  -/
Lean.Linter.getDeclsByBody : Lean.Elab.InfoTree → List Lean.Name
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.eq_append_of_dropPrefix?_slice_eq_some : ∀ {pat res : String.Slice} {s : String}, s.dropPrefix? pat = some res → s = pat.copy ++ res.copy
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
/-- `f` is a measure-preserving map w.r.t. measures `μa` and `μb` if `f` is measurable
and `map f μa = μb`.  -/
MeasureTheory.MeasurePreserving : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      [inst_1 : MeasurableSpace β] →
        (α → β) →
          autoParam (MeasureTheory.Measure α) MeasureTheory.MeasurePreserving._auto_1 →
            autoParam (MeasureTheory.Measure β) MeasureTheory.MeasurePreserving._auto_3 → Prop
-- Mathlib.Analysis.MeanInequalitiesPow
ENNReal.LpAddConst_zero : ENNReal.LpAddConst 0 = 1
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_top : ⌈⊤⌉ₑ = ⊤
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : Res(f)(A) ⟶ B`,
this is the induced map from the short complex `A --d₀₁--> Fun(H, A) --d₁₂--> Fun(H × H, A)`
to `B --d₀₁--> Fun(G, B) --d₁₂--> Fun(G × G, B)`.  -/
groupCohomology.mapShortComplexH1 : {k G H : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Group H] →
        {A : Rep.{max u u_1, u, u} k H} →
          {B : Rep.{max u u_1, u, u} k G} →
            (f : G →* H) → (Rep.res f A ⟶ B) → (groupCohomology.shortComplexH1 A ⟶ groupCohomology.shortComplexH1 B)
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_X_sub_C_le : ∀ {R : Type u} [inst : Ring R] (r : R), (Polynomial.X - Polynomial.C r).degree ≤ 1
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.sdiff_ae_eq_self : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t : Set α}, s \ t =ᵐ[μ] s ↔ μ (s ∩ t) = 0
-- Mathlib.RingTheory.Derivation.MapCoeffs
Differential.mapCoeffs_monomial : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Differential A] (n : ℕ) (x : A),
  Differential.mapCoeffs ((Polynomial.monomial n) x) = (Polynomial.monomial n) x′
-- Mathlib.Order.Cofinal
IsCofinal.of_not_bddAbove : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α}, ¬BddAbove s → IsCofinal s
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr : Type → Type
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast!_map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : LawfulBEq α] {f : (a : α) → β a → γ a}
  {l : List ((a : α) × β a)} {k : α} [inst_2 : Inhabited (γ k)],
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValueCast! k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) =
      (Option.map (f k) (Std.Internal.List.getValueCast? k l)).get!
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inr_fst : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr CategoryTheory.Limits.biprod.fst = 0
-- Mathlib.Order.OrderDual
/-- **Alias** of the reverse direction of `OrderDual.toDual_lt_toDual`. -/
LT.lt.dual : ∀ {α : Type u_1} [inst : LT α] {a b : α}, b < a → OrderDual.toDual a < OrderDual.toDual b
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.δ_comp_δ'_apply : ∀ {S : SSet} {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 3)} (H : i.castSucc < j)
  (x : S.obj (Opposite.op { len := n + 2 })),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S i))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S j)) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S (j.pred ⋯)))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S i.castSucc)) x)
-- Mathlib.CategoryTheory.Monad.Types
CategoryTheory.ofTypeMonad_η_app : ∀ (m : Type u → Type u) [inst : Monad m] [inst_1 : LawfulMonad m] (X : Type u),
  (CategoryTheory.ofTypeMonad m).η.app X = TypeCat.ofHom pure
-- Mathlib.Analysis.SpecialFunctions.Log.Summable
Real.multipliable_of_summable_log : ∀ {ι : Type u_1} {f : ι → ℝ}, (∀ (i : ι), 0 < f i) → (Summable fun i => Real.log (f i)) → Multipliable f
-- Lean.Meta.LazyDiscrTree
_private.Lean.Meta.LazyDiscrTree.0.Lean.Meta.LazyDiscrTree.MatchResult.push.loop.eq_def : ∀ {α : Type} (score : ℕ) (e : Array α) (a : Array (Array (Array α))),
  Lean.Meta.LazyDiscrTree.MatchResult.push.loop✝ score e a =
    if a.size < score then Lean.Meta.LazyDiscrTree.MatchResult.push.loop✝ score e (a.push #[])
    else { elts := a.push #[e] }
-- Init.Control.Basic
/-- Converts the result of the monadic action `x` to a `Bool`. If it is `true`, returns `y`; otherwise,
returns the original result of `x`.

This is a monadic counterpart to the short-circuiting `&&` operator, usually accessed via the `<&&>`
operator.


Conventions for notations in identifiers:

 * The recommended spelling of `<&&>` in identifiers is `andM`. -/
andM : {m : Type u → Type v} → {β : Type u} → [Monad m] → [ToBool β] → m β → m β → m β
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.edge_adj : ∀ {V : Type u_1} (s t v w : V), (SimpleGraph.edge s t).Adj v w ↔ (v = s ∧ w = t ∨ v = t ∧ w = s) ∧ v ≠ w
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
/-- `P` is a sheaf for `R`, iff the fork given by `w` is an equalizer.  -/
CategoryTheory.Equalizer.Presieve.sheaf_condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C}
  (R : CategoryTheory.Presieve X) [inst_1 : R.HasPairwisePullbacks],
  CategoryTheory.Presieve.IsSheafFor P R ↔
    Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Equalizer.forkMap P R) ⋯))
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac_assoc : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [inst : AlgebraicGeometry.IsOpenImmersion f]
  [inst_1 : AlgebraicGeometry.IsOpenImmersion g] (e : Set.range ⇑f = Set.range ⇑g) {Z_1 : AlgebraicGeometry.Scheme}
  (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq f g e).inv
      (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp g h
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- The additive monoid algebra over a semiring `R` generated by the additive monoid `M`.

It is the type of finite formal `R`-linear combinations of terms of `M`,
endowed with the convolution product.  -/
AddMonoidAlgebra : (R : Type u_8) → Type u_9 → [Semiring R] → Type (max u_8 u_9)
-- Lean.Server.FileWorker.SemanticHighlighting
_private.Lean.Server.FileWorker.SemanticHighlighting.0.Lean.Server.FileWorker.collectVersoTokens : Lean.FileMap →
  Lean.Syntax →
    (Lean.Syntax → Array Lean.Server.FileWorker.LeanSemanticToken) → Array Lean.Server.FileWorker.LeanSemanticToken
-- Mathlib.Tactic.Linter.Whitespace
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.Style.Whitespace.getUnlintedRanges.match_1.eq_2 : ∀ (motive : Option Lean.Syntax.Range → Sort u_1) (x : Option Lean.Syntax.Range)
  (h_1 : (trail : Lean.Syntax.Range) → motive (some trail)) (h_2 : (x : Option Lean.Syntax.Range) → motive x),
  (∀ (trail : Lean.Syntax.Range), x = some trail → False) →
    (match x with
      | some trail => h_1 trail
      | x => h_2 x) =
      h_2 x
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sum_finsetSum_index : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] {γ : Type w} {α : Type x}
  [inst_1 : (i : ι) → AddCommMonoid (β i)] [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddCommMonoid γ]
  {s : Finset α} {g : α → Π₀ (i : ι), β i} {h : (i : ι) → β i → γ},
  (∀ (i : ι), h i 0 = 0) →
    (∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ + h i b₂) → ∑ i ∈ s, (g i).sum h = (∑ i ∈ s, g i).sum h
-- Mathlib.Data.List.Basic
List.filterMap_congr : ∀ {α : Type u} {β : Type v} {f g : α → Option β} {l : List α},
  (∀ x ∈ l, f x = g x) → List.filterMap f l = List.filterMap g l
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.setLike : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : Semiring A] →
          [inst_3 : StarRing A] → [inst_4 : Algebra R A] → [inst_5 : StarModule R A] → SetLike (StarSubalgebra R A) A
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_map_equiv : ∀ {α : Type u_1} {δ : Type u_4} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : MeasurableSpace δ] [inst_1 : TopologicalSpace ε] [inst_2 : ContinuousENorm ε] (f : α ≃ᵐ δ) (g : δ → ε),
  MeasureTheory.Integrable g (MeasureTheory.Measure.map (⇑f) μ) ↔ MeasureTheory.Integrable (g ∘ ⇑f) μ
-- Mathlib.Algebra.Algebra.Equiv
/-- `simp` normal form of `invFun_eq_symm`  -/
AlgEquiv.symm_toEquiv_eq_symm : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] {e : A₁ ≃ₐ[R] A₂}, (↑e).symm = ↑e.symm
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Define a pass that tries replacing a specific tactic with `grind`.

`tacticName` is a human-readable name for the tactic, for example "linarith".
This can be used to group messages together, so that `ring`, `ring_nf`, `ring1`, ...
all produce the same message.

`tacticKind` is the `SyntaxNodeKind` for the tactic's main parser,
for example `Mathlib.Tactic.linarith`.

If `extractArgs` is provided, it extracts term arguments from the original tactic
(e.g., `linarith [X, Y]`) and passes them to grind (e.g., `grind [X, Y]`).
Local hypotheses are filtered out since grind uses them automatically.
 -/
Mathlib.TacticAnalysis.grindReplacementWith : String →
  Lean.SyntaxNodeKind →
    (optParam (Lean.Syntax → Option (Lean.Syntax.TSepArray `term ",")) fun x => none) →
      optParam Bool true → optParam Bool false → optParam Bool false → optParam Float 1 → Mathlib.TacticAnalysis.Config
-- Mathlib.Order.CompleteLattice.Basic
/-- When taking the infimum of `f : ι → α`, the elements of `ι` on which `f` gives `⊤`
can be dropped, without changing the result.  -/
iInf_ne_top_subtype : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] (f : ι → α), ⨅ i, f ↑i = ⨅ i, f i
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.finrank_bot' : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E],
  Module.finrank (↥⊥) E = Module.finrank F E
-- Mathlib.Tactic.ClickSuggestions.Rewrite
Mathlib.Tactic.ClickSuggestions.RwLemma.mk : Mathlib.Tactic.ClickSuggestions.Premise → Bool → Mathlib.Tactic.ClickSuggestions.RwLemma
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toListRev_map_eq_toListRev_mapM : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → γ} {it : Std.IterM m β},
  (Std.IterM.map f it).toListRev = (Std.IterM.mapM (fun b => pure (f b)) it).toListRev
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- Additive subsemigroups of an additive semigroup `A` are isomorphic to
multiplicative subsemigroups of `Multiplicative A`.  -/
AddSubsemigroup.toSubsemigroup : {A : Type u_5} → [inst : Add A] → AddSubsemigroup A ≃o Subsemigroup (Multiplicative A)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.norm_condExpIndL1Fin_le : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)]
  (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G), ‖MeasureTheory.condExpIndL1Fin hm hs hμs x‖ ≤ μ.real s * ‖x‖
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.SymExtensionState : Type
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_hom_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (j : J) (k : K),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F k).hom
      (CategoryTheory.Limits.limit.π (F.comp ((CategoryTheory.evaluation K C).obj k)) j) =
    (CategoryTheory.Limits.limit.π F j).app k
-- Mathlib.Data.Sum.Interval
Finset.inr_mem_sumLexLift : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  {f₁ : α₁ → β₁ → Finset γ₁} {f₂ : α₂ → β₂ → Finset γ₂} {g₁ : α₁ → β₂ → Finset γ₁} {g₂ : α₁ → β₂ → Finset γ₂}
  {a : α₁ ⊕ α₂} {b : β₁ ⊕ β₂} {c₂ : γ₂},
  Sum.inr c₂ ∈ Finset.sumLexLift f₁ f₂ g₁ g₂ a b ↔
    (∃ a₁ b₂, a = Sum.inl a₁ ∧ b = Sum.inr b₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨
      ∃ a₂ b₂, a = Sum.inr a₂ ∧ b = Sum.inr b₂ ∧ c₂ ∈ f₂ a₂ b₂