Loogle!

Result

Found 20 declarations mentioning HomologicalComplex₂.total.map.

• HomologicalComplex₂.total.map 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] : K.total c₁₂ ⟶ L.total c₁₂
• HomologicalComplex₂.total.map_id 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] : HomologicalComplex₂.total.map (CategoryTheory.CategoryStruct.id K) c₁₂ = CategoryTheory.CategoryStruct.id (K.total c₁₂)
• HomologicalComplex₂.total.mapIso_hom 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (e : K ≅ L) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] : (HomologicalComplex₂.total.mapIso e c₁₂).hom = HomologicalComplex₂.total.map e.hom c₁₂
• HomologicalComplex₂.total.mapIso_inv 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (e : K ≅ L) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] : (HomologicalComplex₂.total.mapIso e c₁₂).inv = HomologicalComplex₂.total.map e.inv c₁₂
• HomologicalComplex₂.total.map.eq_1 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] : HomologicalComplex₂.total.map φ c₁₂ = { f := CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂), comm' := ⋯ }
• HomologicalComplex₂.totalFunctor_map 📋 Mathlib.Algebra.Homology.TotalComplex
  (C : Type u_1) [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [∀ (K : HomologicalComplex₂ C c₁ c₂), K.HasTotal c₁₂] {X✝ Y✝ : HomologicalComplex₂ C c₁ c₂} (φ : X✝ ⟶ Y✝) : (HomologicalComplex₂.totalFunctor C c₁ c₂ c₁₂).map φ = HomologicalComplex₂.total.map φ c₁₂
• HomologicalComplex₂.total.map_comp 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L M : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (ψ : L ⟶ M) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] [M.HasTotal c₁₂] : HomologicalComplex₂.total.map (CategoryTheory.CategoryStruct.comp φ ψ) c₁₂ = CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map φ c₁₂) (HomologicalComplex₂.total.map ψ c₁₂)
• HomologicalComplex₂.total.forget_map 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] : (HomologicalComplex.forget C c₁₂).map (HomologicalComplex₂.total.map φ c₁₂) = CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂)
• HomologicalComplex₂.ιTotalOrZero_map 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K L : HomologicalComplex₂ C c₁ c₂) (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) : CategoryTheory.CategoryStruct.comp (K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂) ((HomologicalComplex₂.total.map φ c₁₂).f i₁₂) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (L.ιTotalOrZero c₁₂ i₁ i₂ i₁₂)
• HomologicalComplex₂.total.map_comp_assoc 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L M : HomologicalComplex₂ C c₁ c₂} (φ : K ⟶ L) (ψ : L ⟶ M) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] [M.HasTotal c₁₂] {Z : HomologicalComplex C c₁₂} (h : M.total c₁₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map (CategoryTheory.CategoryStruct.comp φ ψ) c₁₂) h = CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map φ c₁₂) (CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map ψ c₁₂) h)
• HomologicalComplex₂.ιTotal_map 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K L : HomologicalComplex₂ C c₁ c₂) (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂) : CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ h) ((HomologicalComplex₂.total.map φ c₁₂).f i₁₂) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (L.ιTotal c₁₂ i₁ i₂ i₁₂ h)
• HomologicalComplex₂.ιTotalOrZero_map_assoc 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K L : HomologicalComplex₂ C c₁ c₂) (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) {Z : C} (h : (L.total c₁₂).X i₁₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂) (CategoryTheory.CategoryStruct.comp ((HomologicalComplex₂.total.map φ c₁₂).f i₁₂) h) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (CategoryTheory.CategoryStruct.comp (L.ιTotalOrZero c₁₂ i₁ i₂ i₁₂) h)
• HomologicalComplex₂.ιTotal_map_assoc 📋 Mathlib.Algebra.Homology.TotalComplex
  {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K L : HomologicalComplex₂ C c₁ c₂) (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [TotalComplexShape c₁ c₂ c₁₂] [DecidableEq I₁₂] [K.HasTotal c₁₂] [L.HasTotal c₁₂] (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂) {Z : C} (h✝ : (L.total c₁₂).X i₁₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ h) (CategoryTheory.CategoryStruct.comp ((HomologicalComplex₂.total.map φ c₁₂).f i₁₂) h✝) = CategoryTheory.CategoryStruct.comp ((φ.f i₁).f i₂) (CategoryTheory.CategoryStruct.comp (L.ιTotal c₁₂ i₁ i₂ i₁₂ h) h✝)
• HomologicalComplex.mapBifunctorMap.eq_1 📋 Mathlib.Algebra.Homology.Bifunctor
  {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} D] {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} [CategoryTheory.Limits.HasZeroMorphisms C₁] [CategoryTheory.Limits.HasZeroMorphisms C₂] [CategoryTheory.Preadditive D] {K₁ L₁ : HomologicalComplex C₁ c₁} {K₂ L₂ : HomologicalComplex C₂ c₂} (f₁ : K₁ ⟶ L₁) (f₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [F.PreservesZeroMorphisms] [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [TotalComplexShape c₁ c₂ c] [K₁.HasMapBifunctor K₂ F c] [L₁.HasMapBifunctor L₂ F c] [DecidableEq J] : HomologicalComplex.mapBifunctorMap f₁ f₂ F c = HomologicalComplex₂.total.map (CategoryTheory.CategoryStruct.comp (((F.mapBifunctorHomologicalComplex c₁ c₂).map f₁).app K₂) (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).map f₂)) c
• HomologicalComplex₂.totalShift₁Iso_hom_naturality 📋 Mathlib.Algebra.Homology.TotalComplexShift
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {K L : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)} (f : K ⟶ L) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] [L.HasTotal (ComplexShape.up ℤ)] : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map ((HomologicalComplex₂.shiftFunctor₁ C x).map f) (ComplexShape.up ℤ)) (L.totalShift₁Iso x).hom = CategoryTheory.CategoryStruct.comp (K.totalShift₁Iso x).hom ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).map (HomologicalComplex₂.total.map f (ComplexShape.up ℤ)))
• HomologicalComplex₂.totalShift₂Iso_hom_naturality 📋 Mathlib.Algebra.Homology.TotalComplexShift
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {K L : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)} (f : K ⟶ L) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] [L.HasTotal (ComplexShape.up ℤ)] : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map ((HomologicalComplex₂.shiftFunctor₂ C y).map f) (ComplexShape.up ℤ)) (L.totalShift₂Iso y).hom = CategoryTheory.CategoryStruct.comp (K.totalShift₂Iso y).hom ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).map (HomologicalComplex₂.total.map f (ComplexShape.up ℤ)))
• HomologicalComplex₂.totalShift₁Iso_hom_naturality_assoc 📋 Mathlib.Algebra.Homology.TotalComplexShift
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {K L : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)} (f : K ⟶ L) (x : ℤ) [K.HasTotal (ComplexShape.up ℤ)] [L.HasTotal (ComplexShape.up ℤ)] {Z : HomologicalComplex C (ComplexShape.up ℤ)} (h : (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).obj (L.total (ComplexShape.up ℤ)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map ((HomologicalComplex₂.shiftFunctor₁ C x).map f) (ComplexShape.up ℤ)) (CategoryTheory.CategoryStruct.comp (L.totalShift₁Iso x).hom h) = CategoryTheory.CategoryStruct.comp (K.totalShift₁Iso x).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).map (HomologicalComplex₂.total.map f (ComplexShape.up ℤ))) h)
• HomologicalComplex₂.totalShift₂Iso_hom_naturality_assoc 📋 Mathlib.Algebra.Homology.TotalComplexShift
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {K L : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)} (f : K ⟶ L) (y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] [L.HasTotal (ComplexShape.up ℤ)] {Z : HomologicalComplex C (ComplexShape.up ℤ)} (h : (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).obj (L.total (ComplexShape.up ℤ)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map ((HomologicalComplex₂.shiftFunctor₂ C y).map f) (ComplexShape.up ℤ)) (CategoryTheory.CategoryStruct.comp (L.totalShift₂Iso y).hom h) = CategoryTheory.CategoryStruct.comp (K.totalShift₂Iso y).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).map (HomologicalComplex₂.total.map f (ComplexShape.up ℤ))) h)
• HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom 📋 Mathlib.Algebra.Homology.TotalComplexShift
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).totalShift₁Iso x).hom ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).map (K.totalShift₂Iso y).hom) = (x * y).negOnePow • CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map ((HomologicalComplex₂.shiftFunctor₁₂CommIso C x y).hom.app K) (ComplexShape.up ℤ)) (CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).totalShift₂Iso y).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).map (K.totalShift₁Iso x).hom) ((CategoryTheory.shiftFunctorComm (CochainComplex C ℤ) x y).hom.app (K.total (ComplexShape.up ℤ)))))
• HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom_assoc 📋 Mathlib.Algebra.Homology.TotalComplexShift
  {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x y : ℤ) [K.HasTotal (ComplexShape.up ℤ)] {Z : HomologicalComplex C (ComplexShape.up ℤ)} (h : (CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).obj ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).obj (K.total (ComplexShape.up ℤ))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).totalShift₁Iso x).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).map (K.totalShift₂Iso y).hom) h) = CategoryTheory.CategoryStruct.comp ((x * y).negOnePow • CategoryTheory.CategoryStruct.comp (HomologicalComplex₂.total.map ((HomologicalComplex₂.shiftFunctor₁₂CommIso C x y).hom.app K) (ComplexShape.up ℤ)) (CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).totalShift₂Iso y).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) y).map (K.totalShift₁Iso x).hom) ((CategoryTheory.shiftFunctorComm (CochainComplex C ℤ) x y).hom.app (K.total (ComplexShape.up ℤ)))))) h

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

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

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

3. 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

4. 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.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 19971e9 serving mathlib revision 40fea08