mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_diff!_of_contains_eq_false_left : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k m₁ = false → Std.DTreeMap.Internal.Impl.Const.get? (m₁.diff! m₂) k = none
-- Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
ContinuousAffineMap.norm_eq : ∀ {𝕜 : Type u_1} {V : Type u_3} {W : Type u_4} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 V] [inst_4 : NormedSpace 𝕜 W] (f : V →ᴬ[𝕜] W),
  f 0 = 0 → ‖f‖ = ‖f.contLinear‖
-- Std.Http.Data.Body.Any
/-- Sets the size of the body.
 -/
Std.Http.Body.Any.setKnownSize : Std.Http.Body.Any → Option Std.Http.Body.Length → Std.Async.Async Unit
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k k' : α},
  cmp k k' = Ordering.eq → t.getKey? k = t.getKey? k'
-- Mathlib.CategoryTheory.Functor.FullyFaithful
/-- Structure containing the data of inverse map `(F.obj X ⟶ F.obj Y) ⟶ (X ⟶ Y)` of `F.map`
in order to express that `F` is a fully faithful functor.  -/
CategoryTheory.Functor.FullyFaithful : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Type (max (max u₁ v₁) v₂)
-- Lean.Message
Lean.SerialMessage.mk : Lean.BaseMessage String → Lean.Name → Lean.SerialMessage
-- Mathlib.RingTheory.Bialgebra.Quotient
/-- `Ideal.Quotient.mkₐ` as a bialgebra homomorphism.  -/
Bialgebra.Quotient.mkBialgHom : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : Ring A] →
        [inst_2 : Bialgebra R A] →
          (I : Ideal A) →
            [inst_3 : I.IsTwoSided] → [inst_4 : (Submodule.restrictScalars R I).IsCoideal] → A →ₐc[R] A ⧸ I
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerRightIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ≅ Y) (Z : C),
  (CategoryTheory.MonoidalCategory.whiskerRightIso f Z).inv = CategoryTheory.MonoidalCategoryStruct.whiskerRight f.inv Z
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.mem_range_self : ∀ {V₁ : Type u_3} {V₂ : Type u_4} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂) (v : V₁), f v ∈ f.range
-- Mathlib.RingTheory.Grassmannian
Module.Grassmannian.mk.sizeOf_spec : ∀ {R : Type u} [inst : CommRing R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {k : ℕ}
  [inst_3 : SizeOf R] [inst_4 : SizeOf M] (toSubmodule : Submodule R M)
  (finite_quotient : Module.Finite R (M ⧸ toSubmodule)) (projective_quotient : Module.Projective R (M ⧸ toSubmodule))
  (rankAtStalk_eq : ∀ (p : PrimeSpectrum R), Module.rankAtStalk (M ⧸ toSubmodule) p = k),
  sizeOf
      { toSubmodule := toSubmodule, finite_quotient := finite_quotient, projective_quotient := projective_quotient,
        rankAtStalk_eq := rankAtStalk_eq } =
    1 + sizeOf toSubmodule + sizeOf finite_quotient + sizeOf projective_quotient
-- Lean.Elab.Binders
Lean.Elab.Term.BinderView.type : Lean.Elab.Term.BinderView → Lean.Syntax
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesOnBall.hasFPowerSeriesWithinOnBall : ∀ {𝕜 : 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} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f p x r → HasFPowerSeriesWithinOnBall f p s x r
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_omega : ∀ {o : Ordinal.{u_1}}, Order.IsSuccLimit o → (Ordinal.omega o).cof = o.cof
-- Mathlib.Topology.VectorBundle.Riemannian
Bundle.RiemannianMetric.mk.sizeOf_spec : ∀ {B : Type u_4} {E : B → Type u_6} [inst : (b : B) → TopologicalSpace (E b)] [inst_1 : (b : B) → AddCommGroup (E b)]
  [inst_2 : (b : B) → Module ℝ (E b)] [inst_3 : SizeOf B] [inst_4 : (a : B) → SizeOf (E a)]
  (inner : (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ) (symm : ∀ (b : B) (v w : E b), ((inner b) v) w = ((inner b) w) v)
  (pos : ∀ (b : B) (v : E b), v ≠ 0 → 0 < ((inner b) v) v)
  (continuousAt : ∀ (b : B), ContinuousAt (fun v => ((inner b) v) v) 0)
  (isVonNBounded : ∀ (b : B), Bornology.IsVonNBounded ℝ {v | ((inner b) v) v < 1}),
  sizeOf { inner := inner, symm := symm, pos := pos, continuousAt := continuousAt, isVonNBounded := isVonNBounded } = 1
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
/-- **Double counting** argument.

Considering `r` as a bipartite graph, the LHS is a strict lower bound on the number of edges while
the RHS is an upper bound.  -/
Finset.card_nsmul_lt_card_nsmul_of_lt_of_le : ∀ {R : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R]
  (r : α → β → Prop) {s : Finset α} {t : Finset β} {m n : R} [inst_3 : (a : α) → (b : β) → Decidable (r a b)],
  s.Nonempty →
    (∀ a ∈ s, m < ↑(Finset.bipartiteAbove r t a).card) →
      (∀ b ∈ t, ↑(Finset.bipartiteBelow r s b).card ≤ n) → s.card • m < t.card • n
-- Lean.Compiler.IR.Basic
/-- Extract the `tobject` value at Position `sizeof(void*)*i` from `x`.
We also use `proj` for extracting fields from `struct` return values, and casting `union` return values.  -/
Lean.IR.Expr.proj : ℕ → Lean.IR.VarId → Lean.IR.Expr
-- Init.Data.String.Lemmas.Pattern.Find.Basic
String.Slice.isSome_find? : ∀ {ρ : Type} (pat : ρ) {σ : String.Slice → Type}
  [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [∀ (s : String.Slice), Std.Iterators.Finite (σ s) Id] [inst_2 : (s : String.Slice) → Std.IteratorLoop (σ s) Id Id]
  [∀ (s : String.Slice), Std.LawfulIteratorLoop (σ s) Id Id] [inst_4 : String.Slice.Pattern.ToForwardSearcher pat σ]
  {s : String.Slice}, (s.find? pat).isSome = s.contains pat
-- Mathlib.Topology.Algebra.Monoid
/-- **Alias** of `continuous_finsetSum`. -/
continuous_finset_sum : ∀ {ι : Type u_1} {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid M] [ContinuousAdd M] {f : ι → X → M} (s : Finset ι),
  (∀ i ∈ s, Continuous (f i)) → Continuous fun a => ∑ i ∈ s, f i a
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.coe_ofContinuousOpen_symm : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialEquiv X Y)
  (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap ↑e) (hs : IsOpen e.source),
  ↑(PartialHomeomorph.ofContinuousOpen e hc ho hs).symm = ↑e.symm
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.instInhabited : {α : Type} → Inhabited (Lean.Meta.LazyDiscrTree α)
-- Mathlib.Order.Max
isMin_iff_forall_not_lt : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, IsMin a ↔ ∀ (b : α), ¬b < a
-- Mathlib.Logic.Basic
BAll.imp_right : ∀ {α : Sort u_1} {p : α → Prop} {P Q : (x : α) → p x → Prop},
  (∀ (x : α) (h : p x), P x h → Q x h) → (∀ (x : α) (h : p x), P x h) → ∀ (x : α) (h : p x), Q x h
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerRight_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ⟶ Y),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
      (CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).inv)
-- Mathlib.Data.Set.CoeSort
/-- Given the set `s`, `Elem s` is the `Type` of element of `s`.

It is currently an abbreviation so that instance coming from `Subtype` are available.
If you're interested in making it a `def`, as it probably should be,
you'll then need to create additional instances (and possibly prove lemmas about them).
See e.g. `Mathlib/Data/Set/Order.lean`.
 -/
Set.Elem : {α : Type u} → Set α → Type u
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → ∀ {k a : α} {v : β}, (t.insert k v).getKey! a = if cmp k a = Ordering.eq then k else t.getKey! a
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
/-- If two morphisms of `Arrow V` become equal in the right Freyd category,
then they are right homotopic.  -/
CategoryTheory.Preadditive.RightFreyd.homotopyOfEq : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v : CategoryTheory.Arrow V} →
        (f g : u ⟶ v) →
          (CategoryTheory.Preadditive.RightFreyd.quotient V).map f =
              (CategoryTheory.Preadditive.RightFreyd.quotient V).map g →
            CategoryTheory.Arrow.RightHomotopy f g
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry?.induct_unfolding : ∀ {α : Type u} {β : α → Type v} (motive : Std.DTreeMap.Internal.Impl α β → Option ((a : α) × β a) → Prop),
  motive Std.DTreeMap.Internal.Impl.leaf none →
    (∀ (size : ℕ) (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β),
        motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) (some ⟨k, v⟩)) →
      (∀ (size : ℕ) (k : α) (v : β k) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l r r_1 : Std.DTreeMap.Internal.Impl α β),
          motive (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)
              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minEntry? →
            motive (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)
              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minEntry?) →
        ∀ (a : Std.DTreeMap.Internal.Impl α β), motive a a.minEntry?
-- Lean.Elab.Do.Basic
/-- We inferred the code is semantically dead, but we need to elaborate it to produce a program.  -/
Lean.Elab.Do.CodeLiveness.deadSemantically : Lean.Elab.Do.CodeLiveness
-- Mathlib.Algebra.MvPolynomial.Coeff
MvPolynomial.coeff_linearCombination_X_pow_of_fintype : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommSemiring R] [inst_1 : Fintype σ] (a : σ → R) (s : σ →₀ ℕ) (n : ℕ),
  MvPolynomial.coeff s ((∑ i, a i • MvPolynomial.X i) ^ n) =
    if (s.sum fun x m => m) = n then ↑s.multinomial * s.prod fun r m => a r ^ m else 0
-- Mathlib.Data.Set.Lattice.Image
Set.preimage_kernImage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, GaloisConnection (Set.preimage f) (Set.kernImage f)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- The symmetry of homotopy between morphisms of short complexes.  -/
CategoryTheory.ShortComplex.Homotopy.symm : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ₁ φ₂ : S₁ ⟶ S₂} → CategoryTheory.ShortComplex.Homotopy φ₁ φ₂ → CategoryTheory.ShortComplex.Homotopy φ₂ φ₁
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
/-- Easy inclusion: a differentiability point with derivative in `K` belongs to `D f K`.  -/
FDerivMeasurableAux.differentiable_set_subset_D : ∀ {𝕜 : 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}
  (K : Set (E →L[𝕜] F)), {x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K} ⊆ FDerivMeasurableAux.D f K
-- Mathlib.Algebra.Module.Submodule.Pointwise
/-- The action on a submodule corresponding to applying the action to every element.

This is available as an instance in the `Pointwise` locale.

This is a stronger version of `Submodule.pointwiseDistribMulAction`. Note that `add_smul` does
not hold so this cannot be stated as a `Module`.  -/
Submodule.pointwiseMulActionWithZero : {α : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : Semiring α] → [inst_4 : Module α M] → [SMulCommClass α R M] → MulActionWithZero α (Submodule R M)
-- Mathlib.Algebra.Star.Center
Set.star_mem_center : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : StarMul R] {a : R}, a ∈ Set.center R → star a ∈ Set.center R
-- Mathlib.RingTheory.Localization.Away.Basic
/-- Localizing the localization of `R` at `x` at the image of `y` is the same as localizing
`R` at `x * y`. See `IsLocalization.Away.mul` for the `y * x` version.  -/
IsLocalization.Away.mul' : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (T : Type u_5)
  [inst_3 : CommSemiring T] [inst_4 : Algebra S T] [inst_5 : Algebra R T] [IsScalarTower R S T] (x y : R)
  [IsLocalization.Away x S] [IsLocalization.Away ((algebraMap R S) y) T], IsLocalization.Away (x * y) T
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.HasOfPostcompProperty.of_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
  {W' : CategoryTheory.MorphismProperty C} (Q : CategoryTheory.MorphismProperty C) [W.HasOfPostcompProperty Q],
  W' ≤ Q → W.HasOfPostcompProperty W'
-- Mathlib.Algebra.Homology.HomotopyCategory.KProjective
CochainComplex.isKProjective_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K₁ K₂ : CochainComplex C ℤ} (e : K₁ ≅ K₂) [K₁.IsKProjective], K₂.IsKProjective
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.map_mem : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {ι : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  (self : 𝒜 →ₐᵍ[R] ℬ) {i : ι} {x : A}, x ∈ 𝒜 i → (↑self).toRingHom x ∈ ℬ i
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pushout.map.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z S T : C} (f₁ : S ⟶ W) (f₂ : S ⟶ X)
  [inst_1 : CategoryTheory.Limits.HasPushout f₁ f₂] (g₁ : T ⟶ Y) (g₂ : T ⟶ Z)
  [inst_2 : CategoryTheory.Limits.HasPushout g₁ g₂] (i₁ i₁_1 : W ⟶ Y) (e_i₁ : i₁ = i₁_1) (i₂ i₂_1 : X ⟶ Z)
  (e_i₂ : i₂ = i₂_1) (i₃ i₃_1 : S ⟶ T) (e_i₃ : i₃ = i₃_1)
  (eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₁ = CategoryTheory.CategoryStruct.comp i₃ g₁)
  (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₂ = CategoryTheory.CategoryStruct.comp i₃ g₂),
  CategoryTheory.Limits.pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂ =
    CategoryTheory.Limits.pushout.map f₁ f₂ g₁ g₂ i₁_1 i₂_1 i₃_1 ⋯ ⋯
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roc_eq_if : ∀ {m n : ℤ}, (m<...=n).toList = if m + 1 ≤ n then (m + 1) :: ((m + 1)<...=n).toList else []
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂_hom_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C) (hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hT₂ : T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (e₁ : T₁.obj₁ ≅ T₂.obj₁) (e₂ : T₁.obj₂ ≅ T₂.obj₂)
  (comm : CategoryTheory.CategoryStruct.comp T₁.mor₁ e₂.hom = CategoryTheory.CategoryStruct.comp e₁.hom T₂.mor₁),
  (CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂ T₁ T₂ hT₁ hT₂ e₁ e₂ comm).hom.hom₂ = e₂.hom
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence
_private.Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence.0.ContinuousLinearMap.isPosSemidef_diagonalStrongDualProd : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {L₁ : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ}
  {L₂ : StrongDual ℝ F →L[ℝ] StrongDual ℝ F →L[ℝ] ℝ},
  L₁.toBilinForm.IsPosSemidef →
    L₂.toBilinForm.IsPosSemidef → (ContinuousLinearMap.diagonalStrongDualProd✝ L₁ L₂).toBilinForm.IsPosSemidef
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.kerTotal_eq : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (Finsupp.linearCombination S ⇑(KaehlerDifferential.D R S)).ker = KaehlerDifferential.kerTotal R S
-- LeanSearchClient.Syntax
/-- Search [LeanSearch](https://leansearch.net/) from within Lean.
Queries should be a string that ends with a `.` or `?`. This works as a command, as a term
and as a tactic as in the following examples. In tactic mode, only valid tactics are displayed.

```lean
#leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."

example := #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."

example : 3 ≤ 5 := by
  #leansearch "If a natural number n is less than m, then the successor of n is less than the successor of m."
  sorry
```

You can modify the LeanSearch URL by setting the `LEANSEARCHCLIENT_LEANSEARCH_API_URL` environment variable.
  -/
LeanSearchClient.leansearch_search_tactic : Lean.ParserDescr
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.IndepSets.inter : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s₁ s' : Set (Set Ω)} (s₂ : Set (Set Ω)),
  ProbabilityTheory.IndepSets s₁ s' μ → ProbabilityTheory.IndepSets (s₁ ∩ s₂) s' μ
-- Mathlib.MeasureTheory.Group.Action
/-- See also `measure_preimage_smul_of_nullMeasurableSet` and `measure_preimage_smul`.  -/
MeasureTheory.measure_preimage_smul_le : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : SMul G α] (μ : MeasureTheory.Measure α)
  [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) (s : Set α), μ ((fun x => c • x) ⁻¹' s) ≤ μ s
-- Batteries.Recycling.MonadSatisfying.Array
_private.Batteries.Recycling.MonadSatisfying.Array.0.Array.SatisfiesM_foldrM.go : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {as : Array α}
  {motive : ℕ → β → Prop} {f : α → β → m β},
  (∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → SatisfiesM (motive ↑i) (f as[i] b)) →
    ∀ {i : ℕ} {b : β} (hi : i ≤ as.size), motive i b → SatisfiesM (motive 0) (Array.foldrM.fold f as 0 i hi b)
-- Lean.Util.ParamMinimizer
Lean.Util.ParamMinimizer.instReprStatus : Repr Lean.Util.ParamMinimizer.Status
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasMulAntidiagonal.map_prodComm_mulAntidiagonal : ∀ {A : Type u_1} [inst : CommMonoid A] [inst_1 : Finset.HasMulAntidiagonal A] {n : A},
  Finset.map (Equiv.prodComm A A).toEmbedding (Finset.HasMulAntidiagonal.mulAntidiagonal n) =
    Finset.HasMulAntidiagonal.mulAntidiagonal n
-- Init.Data.BitVec.Lemmas
BitVec.msb_umod_of_msb_false_of_ne_zero : ∀ {w : ℕ} {x y : BitVec w}, y.msb = false → y ≠ 0#w → (x % y).msb = false
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate `(α ≫ η ≫ ηs) ◫ β`  -/
Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp.mkEvalHorizontalCompConsNil : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEvalHorizontalComp m] →
    Mathlib.Tactic.BicategoryLike.Structural →
      Mathlib.Tactic.BicategoryLike.Structural →
        Mathlib.Tactic.BicategoryLike.WhiskerLeft →
          Mathlib.Tactic.BicategoryLike.NormalExpr →
            Mathlib.Tactic.BicategoryLike.NormalExpr →
              Mathlib.Tactic.BicategoryLike.NormalExpr →
                Mathlib.Tactic.BicategoryLike.NormalExpr →
                  Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsKolmogorovProcess.measurable_edist : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {p q : ℝ} {M : NNReal} {P : MeasureTheory.Measure Ω} {X : T → Ω → E},
  ProbabilityTheory.IsKolmogorovProcess X P p q M → ∀ {s t : T}, Measurable fun ω => edist (X s ω) (X t ω)
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
/-- This is a smooth analogue of `OpenPartialHomeomorph.continuousWithinAt_writtenInExtend_iff`.  -/
OpenPartialHomeomorph.contMDiffWithinAt_writtenInExtend_iff : ∀ {𝕜 : 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] {F : Type u_6} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {G : Type u_7} [inst_8 : TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_8}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {s : Set M}
  {φ : OpenPartialHomeomorph M H} {ψ : OpenPartialHomeomorph N G} {y : M},
  φ ∈ IsManifold.maximalAtlas I n M →
    ψ ∈ IsManifold.maximalAtlas J n N →
      y ∈ φ.source →
        f y ∈ ψ.source →
          Set.MapsTo f s ψ.source →
            (ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 F) n
                (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (↑(φ.extend I).symm ⁻¹' s ∩ Set.range ↑I) (↑(φ.extend I) y) ↔
              ContMDiffWithinAt I J n f s y)
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitHomIsoLimitYoneda'_inv_comp_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (F : CategoryTheory.Functor Iᵒᵖ C) [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I (Type u₂)] (A : C) (i : I),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitHomIsoLimitYoneda' F A).inv
      (TypeCat.ofHom fun g =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F (Opposite.op i)) g) =
    CategoryTheory.Limits.limit.π (F.rightOp.comp (CategoryTheory.yoneda.obj A)) i
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.opEquiv_symm_apply : ∀ {M : Type u_2} [inst : Add M] (x : AddSubsemigroup Mᵃᵒᵖ), (RelIso.symm AddSubsemigroup.opEquiv) x = x.unop
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.Path.mk : {J : Type u_1} →
  [inst : LinearOrder J] →
    {i j : J} →
      (I : Set J) →
        autoParam (i ∈ I) CategoryTheory.SimplicialThickening.Path.left._autoParam →
          autoParam (j ∈ I) CategoryTheory.SimplicialThickening.Path.right._autoParam →
            autoParam (∀ k ∈ I, i ≤ k) CategoryTheory.SimplicialThickening.Path.left_le._autoParam →
              autoParam (∀ k ∈ I, k ≤ j) CategoryTheory.SimplicialThickening.Path.le_right._autoParam →
                CategoryTheory.SimplicialThickening.Path i j
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.Hom.mk'.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.MonObj A] {M N : CategoryTheory.Mod D A} (f : M.X ⟶ N.X)
  (smul_hom :
    CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul f =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f)
        CategoryTheory.ModObj.smul),
  CategoryTheory.Mod.Hom.mk' f smul_hom = { hom := f, isModHom := ⋯ }
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instIsCancelAdd : ∀ {α : Type u_1} [inst : Add α] [IsCancelAdd α], IsCancelAdd (Lex α)