mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finset.Sum
Finset.disjSum_mono_left : ∀ {α : Type u_1} {β : Type u_2} (t : Finset β), Monotone fun s => s.disjSum t
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffWithinAt.prod : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {x₀ : M} {t : Finset ι}
  {f : ι → M → G},
  (∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x₀) → ContMDiffWithinAt I' I n (fun x => ∏ i ∈ t, f i x) s x₀
-- Mathlib.RingTheory.PowerSeries.Basic
/-- Coefficients of a product of power series  -/
PowerSeries.coeff_prod : ∀ {R : Type u_2} [inst : CommSemiring R] {ι : Type u_3} [inst_1 : DecidableEq ι] (f : ι → PowerSeries R) (d : ℕ)
  (s : Finset ι),
  (PowerSeries.coeff d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (PowerSeries.coeff (l i)) (f i)
-- Lean.Data.Lsp.Internal
Lean.Lsp.instInhabitedImportInfo : Inhabited Lean.Lsp.ImportInfo
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.hom_add : ∀ {R : Type u} [inst : Semiring R] {M N : SemimoduleCat R} (f g : M ⟶ N),
  SemimoduleCat.Hom.hom (f + g) = SemimoduleCat.Hom.hom f + SemimoduleCat.Hom.hom g
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform.0.EisensteinSeries.δ.eq_1 : ∀ (x : Fin 2 → ℤ), EisensteinSeries.δ✝ x = if x = ![0, 0] then 1 else if x = ![0, -1] then 2 else 0
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.comp_obj : ∀ {X Y Z : CategoryTheory.ReflQuiv} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X),
  (CategoryTheory.CategoryStruct.comp f g).obj x = g.obj (f.obj x)
-- Mathlib.Tactic.Variable
/-- Attribute to record aliases for the `variable?` command. Aliases are structures that have no
fields, and additional typeclasses are recorded as *arguments* to the structure.

Example:
```
@[variable_alias]
structure VectorSpace (k V : Type*)
  [Field k] [AddCommGroup V] [Module k V]
```
Then `variable? [VectorSpace k V]` ensures that these three typeclasses are present in
the current scope. Notice that it's looking at the arguments to the `VectorSpace` type
constructor. You should not have any fields in `variable_alias` structures.

Notice that `VectorSpace` is not a class; the `variable?` command allows non-classes with the
`variable_alias` attribute to use instance binders.
 -/
Mathlib.Command.Variable.variableAliasAttr : Lean.TagAttribute
-- Mathlib.Data.Complex.Basic
Complex.conj_ofReal : ∀ (r : ℝ), (starRingEnd ℂ) ↑r = ↑r
-- Mathlib.Algebra.Group.Basic
div_mul : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b c : α), a / b * c = a / (b / c)
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- An `n`-Freiman homomorphism from a set `A` to a set `B` is a map which preserves products of `n`
elements.  -/
IsMulFreimanHom : {α : Type u_2} → {β : Type u_3} → [CommMonoid α] → [CommMonoid β] → ℕ → Set α → Set β → (α → β) → Prop
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the reverse direction of `sub_pos`. -/
sub_pos_of_lt : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b : α}, b < a → 0 < a - b
-- Mathlib.Data.Real.Basic
Real.instAddCommMonoid : AddCommMonoid ℝ
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.IsDetector.isSeparator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasEqualizers C] {G : C},
  CategoryTheory.IsDetector G → CategoryTheory.IsSeparator G
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.supportedEquivFinsupp_apply_support_val : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  (s : Set M) (x : ↥(MonoidAlgebra.supported R S s)),
  ((MonoidAlgebra.supportedEquivFinsupp s) x).support.val =
    Multiset.map (fun x_1 => ⟨↑x_1, ⋯⟩) (Multiset.filter (fun x => x ∈ s) (↑x).coeff.support.val).attach
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.toCloseds_toCompacts : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : T2Space α] (s : TopologicalSpace.NonemptyCompacts α),
  s.toCloseds = s.toCloseds
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.IsOrdinal.mem : ∀ {x y : ZFSet.{u}}, x.IsOrdinal → y ∈ x → y.IsOrdinal
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsLowerSet.nhdsSet_eq_principal_lowerClosure : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsLowerSet α] (s : Set α),
  nhdsSet s = Filter.principal ↑(lowerClosure s)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.parseFirstByte_utf8EncodeChar_eq_threeMore : ∀ {c : Char},
  c.utf8Size = 4 →
    ByteArray.utf8DecodeChar?.parseFirstByte (String.utf8EncodeChar c)[0] =
      ByteArray.utf8DecodeChar?.FirstByte.threeMore
-- Mathlib.Algebra.BigOperators.Expect
_private.Mathlib.Algebra.BigOperators.Expect.0.«term_/ℚ_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Regular.IsSMulRegular
QuotSMulTop.map_first_exact_on_four_term_exact_of_isSMulRegular_last : ∀ {R : Type u_1} {M : Type u_3} {M' : Type u_4} {M'' : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] [inst_5 : AddCommGroup M'']
  [inst_6 : Module R M''] {M''' : Type u_6} [inst_7 : AddCommGroup M'''] [inst_8 : Module R M'''] {r : R}
  {f₁ : M →ₗ[R] M'} {f₂ : M' →ₗ[R] M''} {f₃ : M'' →ₗ[R] M'''},
  Function.Exact ⇑f₁ ⇑f₂ →
    Function.Exact ⇑f₂ ⇑f₃ → IsSMulRegular M''' r → Function.Exact ⇑((QuotSMulTop.map r) f₁) ⇑((QuotSMulTop.map r) f₂)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.divCoeffs.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr},
  Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.divCoeffs c = Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.divCoeffs c_1 →
    c = c_1
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- If a function is integrable on a set `s`, and its enorm vanishes on `t \ s`,
then it is integrable on `t` if `t` is null-measurable.  -/
MeasureTheory.IntegrableOn.of_ae_sdiff_eq_zero : ∀ {α : Type u_1} {mα : MeasurableSpace α} {s t : Set α} {μ : MeasureTheory.Measure α} {ε' : Type u_7}
  [inst : TopologicalSpace ε'] [inst_1 : ENormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε'] {f : α → ε'},
  MeasureTheory.IntegrableOn f s μ →
    MeasureTheory.NullMeasurableSet t μ → (∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0) → MeasureTheory.IntegrableOn f t μ
-- Init.Data.Bool
Bool.eq_not_self_or : ∀ {a b : Bool}, a = (!a || b) ↔ a = true ∧ b = true
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.snd_SpecTensorTo_apply : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g)
  (p : ↥(AlgebraicGeometry.Spec T.tensor)), (CategoryTheory.Limits.pullback.snd f g) (T.SpecTensorTo p) = T.y
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.map_mono : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : β → α}
  (hf : Continuous f), Monotone (TopologicalSpace.IrreducibleCloseds.map f hf)
-- Mathlib.Data.Finset.Fold
Finset.fold_congr : ∀ {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β}
  {s : Finset α} {g : α → β}, (∀ x ∈ s, f x = g x) → Finset.fold op b f s = Finset.fold op b g s
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.mapComp_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  {E : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} E] (φ : CategoryTheory.Functor C D)
  (φ' : CategoryTheory.Functor D E) (X : CategoryTheory.FreeGroupoid C),
  (CategoryTheory.FreeGroupoid.mapComp φ φ').inv.app X =
    CategoryTheory.CategoryStruct.id
      (((CategoryTheory.FreeGroupoid.map φ).comp (CategoryTheory.FreeGroupoid.map φ')).obj X)
-- Mathlib.Algebra.Ring.BooleanRing
toBoolAlg_add_add_mul : ∀ {α : Type u_1} [inst : BooleanRing α] (a b : α), toBoolAlg (a + b + a * b) = toBoolAlg a ⊔ toBoolAlg b
-- Mathlib.Topology.ContinuousMap.Star
Homeomorph.compStarAlgEquiv'_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (𝕜 : Type u_3)
  [inst_2 : CommSemiring 𝕜] (A : Type u_4) [inst_3 : TopologicalSpace A] [inst_4 : Semiring A]
  [inst_5 : IsTopologicalSemiring A] [inst_6 : StarRing A] [inst_7 : ContinuousStar A] [inst_8 : Algebra 𝕜 A]
  (f : X ≃ₜ Y) (a : C(Y, A)), (Homeomorph.compStarAlgEquiv' 𝕜 A f) a = (ContinuousMap.compStarAlgHom' 𝕜 A ↑f) a
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The left unitor: `𝟙_ C ⊗ X ≃ X`  -/
CategoryTheory.MonoidalCategoryStruct.leftUnitor : {C : Type u} →
  {𝒞 : CategoryTheory.Category.{v, u} C} →
    [self : CategoryTheory.MonoidalCategoryStruct C] →
      (X : C) →
        CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X ≅ X
-- Mathlib.Data.Finsupp.Weight
Finsupp.finite_of_nat_weight_le : ∀ {σ : Type u_1} [Finite σ] (w : σ → ℕ), (∀ (x : σ), w x ≠ 0) → ∀ (n : ℕ), {d | (Finsupp.weight w) d ≤ n}.Finite
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RcoSliceData.mk.inj : ∀ {α : Type u} {β : Type v} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α fun x => β} {range : Std.Rco α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => β} {range_1 : Std.Rco α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Mathlib.Algebra.Order.Ring.Cone
RingConeClass.toSubmonoidClass : ∀ {S : Type u_1} {R : outParam (Type u_2)} {inst : Ring R} {inst_1 : SetLike S R} [self : RingConeClass S R],
  SubmonoidClass S R
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
/-- The extra degeneracy map on the Čech nerve of a split epi. It is
given on the `0`-projection by the given section of the split epi,
and by shifting the indices on the other projections.  -/
CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (f : CategoryTheory.Arrow C) →
      [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] →
        CategoryTheory.SplitEpi f.hom →
          (n : ℕ) → f.cechNerve.obj (Opposite.op { len := n }) ⟶ f.cechNerve.obj (Opposite.op { len := n + 1 })
-- Lean.Setup
Lean.instFromJsonModuleHeader : Lean.FromJson Lean.ModuleHeader
-- Mathlib.CategoryTheory.Subfunctor.Subobject
CategoryTheory.Subfunctor.equivalenceMonoOver_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)),
  (CategoryTheory.Subfunctor.equivalenceMonoOver F).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun X => CategoryTheory.MonoOver.isoMk (CategoryTheory.asIso (CategoryTheory.Subfunctor.toRange X.arrow)).symm ⋯)
      ⋯
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapDomain_one : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : One M] [inst_2 : One N] {F : Type u_9}
  [inst_3 : FunLike F M N] [OneHomClass F M N] (f : F), MonoidAlgebra.mapDomain (⇑f) 1 = 1
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Connected.exists_isPath : ∀ {V : Type u} {G : SimpleGraph V}, G.Connected → ∀ (u v : V), ∃ p, p.IsPath
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
PartOrdEmb.isCardinalFiltered.congr_simp : ∀ (κ κ_1 : Cardinal.{u}) (e_κ : κ = κ_1) [inst : Fact κ.IsRegular] (a a_1 : PartOrdEmb),
  a = a_1 → PartOrdEmb.isCardinalFiltered κ a = PartOrdEmb.isCardinalFiltered κ_1 a_1
-- Init.Data.UInt.Lemmas
UInt8.le_iff_lt_or_eq : ∀ {a b : UInt8}, a ≤ b ↔ a < b ∨ a = b
-- Mathlib.Data.Int.ModEq
Int.add_modEq_right_iff : ∀ {n a b : ℤ}, a + b ≡ b [ZMOD n] ↔ n ∣ a
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.opEquiv_functor_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {x y : (CategoryTheory.WithTerminal C)ᵒᵖ} (x_1 : x ⟶ y),
  (CategoryTheory.WithTerminal.opEquiv C).functor.map x_1 =
    match x_1 with
    | Opposite.op f =>
      match x, y, f, x_1 with
      | Opposite.op (CategoryTheory.WithTerminal.of x), Opposite.op (CategoryTheory.WithTerminal.of y), f, x_2 =>
        (CategoryTheory.WithTerminal.down f).op
      | Opposite.op CategoryTheory.WithTerminal.star, Opposite.op (CategoryTheory.WithTerminal.of a), x, x_2 =>
        CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.of (Opposite.op a))
      | Opposite.op CategoryTheory.WithTerminal.star, Opposite.op CategoryTheory.WithTerminal.star, x, x_2 =>
        CategoryTheory.CategoryStruct.id CategoryTheory.WithInitial.star
-- Mathlib.Topology.Compactness.CountablyCompact
/-- A first-countable countably compact space is sequentially compact.  -/
instCountablyCompactSpaceSeqCompactSpace : ∀ {X : Type u_4} [inst : TopologicalSpace X] [FirstCountableTopology X] [CountablyCompactSpace X], SeqCompactSpace X
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.IsLower.topology_eq_lowerTopology : ∀ {α : Type u_3} {t : TopologicalSpace α} {inst : Preorder α} [self : Topology.IsLower α], t = Topology.lower α
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Reinterpret a non-unital ring homomorphism `f : α →ₙ+* β` as an additive
monoid homomorphism `α →+ β`. The `simp`-normal form is `(f : α →+ β)`.  -/
NonUnitalRingHom.toAddMonoidHom : {α : Type u_5} →
  {β : Type u_6} → [inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → (α →ₙ+* β) → α →+ β
-- Mathlib.Analysis.Calculus.Taylor
/-- Helper lemma for calculating the derivative of the monomial that appears in Taylor
expansions.  -/
monomial_has_deriv_aux : ∀ (t x : ℝ) (n : ℕ), HasDerivAt (fun y => (x - y) ^ (n + 1)) (-(↑n + 1) * (x - t) ^ n) t
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.CoextendScalars.smul_apply : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) (M : ModuleCat R)
  (g : ↑((ModuleCat.coextendScalars f).obj M)) (s s' : S),
  ((ModuleCat.CoextendScalars.equiv f M) (s • g)) s' = ((ModuleCat.CoextendScalars.equiv f M) g) (s' * s)
-- Mathlib.Algebra.Order.Module.Defs
smul_nonpos_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [PosSMulStrictMono α β] {a : α} {b : β}, a • b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.minEntry?.match_1.congr_eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α fun x => β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (r : Std.DTreeMap.Internal.Impl α fun x => β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1))
  (size : ℕ) (k : α) (v : β) (size_1 : ℕ) (k_1 : α) (v_1 : β) (l r r_1 : Std.DTreeMap.Internal.Impl α fun x => β),
  x = Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1 →
    (match x with
      | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
      | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => h_2 size k v r
      | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r)) r_2 =>
        h_3 size k v l size_2 k_2 v_2 l_1 r h r_2) ≍
      h_3 size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) size_1 k_1 v_1 l r ⋯ r_1
-- LeanSearchClient.LoogleSyntax
/-- Search [Loogle](https://loogle.lean-lang.org/json) from within Lean. This can be used as a command, term or tactic as in the following examples. In the case of a tactic, only valid tactics are displayed.


```lean
#loogle List ?a → ?a

example := #loogle List ?a → ?a

example : 3 ≤ 5 := by
  #loogle Nat.succ_le_succ
  sorry

```

## Loogle Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.

By lemma name substring:
🔍 \"differ\"
finds all lemmas that have \"differ\" somewhere in their lemma name.

By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b

By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, \"two\", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have \"two\" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

You can modify the Loogle server URL by setting the `LEANSEARCHCLIENT_LOOGLE_API_URL` environment variable.
 -/
LeanSearchClient.loogle_term : Lean.ParserDescr
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.Simprocs.add : Lean.Meta.Simprocs → Lean.Name → Bool → Lean.CoreM Lean.Meta.Simprocs
-- Init.Internal.Order.Basic
Lean.Order.CCPO.csup : {α : Sort u} → [inst : Lean.Order.CCPO α] → {c : α → Prop} → Lean.Order.chain c → α
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
/-- the first "inclusion" in the (pre)cylinder  -/
HomotopicalAlgebra.Precylinder.i₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {A : C} → (self : HomotopicalAlgebra.Precylinder A) → A ⟶ self.I
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.filter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} (h₁ : t₁.WF) (h₂ : t₂.WF),
  t₁.Equiv t₂ →
    ∀ {f : (a : α) → β a → Bool},
      (Std.DTreeMap.Internal.Impl.filter f t₁ ⋯).impl.Equiv (Std.DTreeMap.Internal.Impl.filter f t₂ ⋯).impl
-- Mathlib.Data.Finset.NAry
Finset.image_image₂_distrib : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq α']
  [inst_1 : DecidableEq β'] [inst_2 : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β}
  [inst_3 : DecidableEq δ] {g : γ → δ} {f' : α' → β' → δ} {g₁ : α → α'} {g₂ : β → β'},
  (∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)) →
    Finset.image g (Finset.image₂ f s t) = Finset.image₂ f' (Finset.image g₁ s) (Finset.image g₂ t)
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- If two words correspond to the same element in the free group, then they
have a common maximal reduction. This is the proof that the function that sends
an element of the free group to its maximal reduction is well-defined.  -/
FreeGroup.reduce.sound : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeGroup.mk L₁ = FreeGroup.mk L₂ → FreeGroup.reduce L₁ = FreeGroup.reduce L₂
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
/-- Composition with an isomorphism preserves closed immersions.  -/
AlgebraicGeometry.IsClosedImmersion.respectsIso : CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.IsClosedImmersion
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcConnectParams.mk.injEq : ∀ (uri uri_1 : Lean.Lsp.DocumentUri), ({ uri := uri } = { uri := uri_1 }) = (uri = uri_1)
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.filterMap : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → Option β}, t.WF → (Std.TreeMap.Raw.filterMap f t).WF
-- Mathlib.Data.Rel
SetRel.symmetrize_mono : ∀ {α : Type u_1} {R₁ R₂ : SetRel α α}, R₁ ⊆ R₂ → R₁.symmetrize ⊆ R₂.symmetrize
-- Mathlib.Algebra.Order.Antidiag.Nat
Nat.finMulAntidiag_three : ∀ {n : ℕ}, ∀ a ∈ Nat.finMulAntidiag 3 n, a 0 * a 1 * a 2 = n
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.lift_apply_inl : ∀ {S : Type u_1} {R : Type u} {M : Type v} [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Algebra S R] [inst_4 : Module S M] [inst_5 : Module R M] [inst_6 : Module Rᵐᵒᵖ M]
  [inst_7 : SMulCommClass R Rᵐᵒᵖ M] [inst_8 : IsScalarTower S R M] [inst_9 : IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2}
  [inst_10 : Semiring A] [inst_11 : Algebra S A] (f : R →ₐ[S] A) (g : M →ₗ[S] A) (hg : ∀ (x y : M), g x * g y = 0)
  (hfg : ∀ (r : R) (x : M), g (r • x) = f r * g x) (hgf : ∀ (r : R) (x : M), g (MulOpposite.op r • x) = g x * f r)
  (r : R), (TrivSqZeroExt.lift f g hg hfg hgf) (TrivSqZeroExt.inl r) = f r
-- Mathlib.Algebra.Ring.Subring.Defs
/-- The actual `Subring` obtained from an element of a `SubringClass`.  -/
Subring.ofClass : {S : Type u_1} → {R : Type u_2} → [inst : NonAssocRing R] → [inst_1 : SetLike S R] → [SubringClass S R] → S → Subring R
-- Mathlib.Tactic.Translate.Core
/-- Run `applyReplacementFun` on the given `srcDecl` to make a new declaration with name `tgt`.  -/
Mathlib.Tactic.Translate.updateDecl : Mathlib.Tactic.Translate.TranslateData →
  Lean.Name →
    Lean.ConstantInfo →
      Mathlib.Tactic.Translate.ArgReorder →
        List ℕ →
          Option Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries →
            Lean.NameMap Lean.Name → Lean.MetaM (Lean.ConstantInfo × Option Mathlib.Tactic.Translate.RelevantArg)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_zero_pos : ∀ (x : NNReal), 0 < x ^ 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_alter_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] [Inhabited α] (h : t.WF) {k fallback : α} {f : Option (β k) → Option (β k)},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.getKeyD k fallback =
    if (f (t.get? k)).isSome = true then k else fallback
-- Mathlib.Algebra.Order.Monoid.NatCast
/-- See `zero_lt_three'` for a version with the type explicit.  -/
zero_lt_three : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [ZeroLEOneClass α] [NeZero 1] [AddLeftMono α],
  0 < 3
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.PendingSolverPropagations.propagate : Lean.Meta.Grind.PendingSolverPropagations → Lean.Meta.Grind.GoalM Unit
-- Lean.Environment
Lean.Kernel.Exception.funExpected.injEq : ∀ (env : Lean.Kernel.Environment) (lctx : Lean.LocalContext) (expr : Lean.Expr) (env_1 : Lean.Kernel.Environment)
  (lctx_1 : Lean.LocalContext) (expr_1 : Lean.Expr),
  (Lean.Kernel.Exception.funExpected env lctx expr = Lean.Kernel.Exception.funExpected env_1 lctx_1 expr_1) =
    (env = env_1 ∧ lctx = lctx_1 ∧ expr = expr_1)