Loogle!

Result

Found 8328 definitions mentioning HSub.hSub. Of these, 214 have a name containing "tsub". Of these, 14 match your pattern(s).

• tsub_tsub_le 📋 Mathlib.Algebra.Order.Sub.Defs
  {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b : α} : b - (b - a) ≤ a
• tsub_tsub_tsub_le_tsub 📋 Mathlib.Algebra.Order.Sub.Defs
  {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftMono α] : c - a - (c - b) ≤ b - a
• tsub_tsub_le_tsub_add 📋 Mathlib.Algebra.Order.Sub.Defs
  {α : Type u_1} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftMono α] {a b c : α} : a - (b - c) ≤ a - b + c
• tsub_tsub_cancel_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
  {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b : α} [AddLeftReflectLE α] (h : a ≤ b) : b - (b - a) = a
• tsub_tsub_tsub_cancel_right 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
  {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (h : c ≤ b) : a - c - (b - c) = a - b
• AddLECancellable.tsub_tsub_cancel_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
  {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b : α} (hba : AddLECancellable (b - a)) (h : a ≤ b) : b - (b - a) = a
• tsub_tsub_tsub_cancel_left 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
  {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : b ≤ a) : a - c - (a - b) = b - c
• tsub_tsub_eq_add_tsub_of_le 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
  {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : c ≤ b) : a - (b - c) = a + c - b
• add_tsub_tsub_cancel 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
  {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h : c ≤ a) : a + b - (a - c) = b + c
• AddLECancellable.tsub_tsub_tsub_cancel_left 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
  {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (hab : AddLECancellable (a - b)) (h : b ≤ a) : a - c - (a - b) = b - c
• tsub_tsub_assoc 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
  {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α] (h₁ : b ≤ a) (h₂ : c ≤ b) : a - (b - c) = a - b + c
• AddLECancellable.add_tsub_tsub_cancel 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
  {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (hac : AddLECancellable (a - c)) (h : c ≤ a) : a + b - (a - c) = b + c
• AddLECancellable.tsub_tsub_assoc 📋 Mathlib.Algebra.Order.Sub.Unbundled.Basic
  {α : Type u_1} [AddCommSemigroup α] [PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α] [Sub α] [OrderedSub α] {a b c : α} (hbc : AddLECancellable (b - c)) (h₁ : b ≤ a) (h₂ : c ≤ b) : a - (b - c) = a - b + c
• tsub_tsub_eq_min 📋 Mathlib.Algebra.Order.Sub.Basic
  {α : Type u_1} [CanonicallyLinearOrderedAddCommMonoid α] [Sub α] [OrderedSub α] [AddLeftReflectLE α] (a b : α) : a - (a - b) = a ⊓ b

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, _ * _, _ ^ _, |- _ < _ → _
woould 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 026c9d9 serving mathlib revision 0e2973b