Loogle!

Result

Found 2244 definitions mentioning instHAdd, HAdd.hAdd, Nat, instAddNat and Fin. Of these, 22 have a name containing "Cases". Of these, 22 match your pattern(s).

• Fin.addCases 📋 Init.Data.Fin.Lemmas
  {m n : ℕ} {motive : Fin (m + n) → Sort u} (left : (i : Fin m) → motive (Fin.castAdd n i)) (right : (i : Fin n) → motive (Fin.natAdd m i)) (i : Fin (m + n)) : motive i
• Fin.lastCases 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {motive : Fin (n + 1) → Sort u_1} (last : motive (Fin.last n)) (cast : (i : Fin n) → motive i.castSucc) (i : Fin (n + 1)) : motive i
• Fin.addCases_left 📋 Init.Data.Fin.Lemmas
  {m n : ℕ} {motive : Fin (m + n) → Sort u_1} {left : (i : Fin m) → motive (Fin.castAdd n i)} {right : (i : Fin n) → motive (Fin.natAdd m i)} (i : Fin m) : Fin.addCases left right (Fin.castAdd n i) = left i
• Fin.addCases_right 📋 Init.Data.Fin.Lemmas
  {m n : ℕ} {motive : Fin (m + n) → Sort u_1} {left : (i : Fin m) → motive (Fin.castAdd n i)} {right : (i : Fin n) → motive (Fin.natAdd m i)} (i : Fin n) : Fin.addCases left right (Fin.natAdd m i) = right i
• Fin.lastCases_last 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {motive : Fin (n + 1) → Sort u_1} {last : motive (Fin.last n)} {cast : (i : Fin n) → motive i.castSucc} : Fin.lastCases last cast (Fin.last n) = last
• Fin.lastCases_castSucc 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {motive : Fin (n + 1) → Sort u_1} {last : motive (Fin.last n)} {cast : (i : Fin n) → motive i.castSucc} (i : Fin n) : Fin.lastCases last cast i.castSucc = cast i
• Fin.cases 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {motive : Fin (n + 1) → Sort u_1} (zero : motive 0) (succ : (i : Fin n) → motive i.succ) (i : Fin (n + 1)) : motive i
• Fin.cases_succ 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {motive : Fin (n + 1) → Sort u_1} {zero : motive 0} {succ : (i : Fin n) → motive i.succ} (i : Fin n) : Fin.cases zero succ i.succ = succ i
• Fin.cases_zero 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {motive : Fin (n + 1) → Sort u_1} {zero : motive 0} {succ : (i : Fin n) → motive i.succ} : Fin.cases zero succ 0 = zero
• Fin.cases_succ' 📋 Init.Data.Fin.Lemmas
  {n : ℕ} {motive : Fin (n + 1) → Sort u_1} {zero : motive 0} {succ : (i : Fin n) → motive i.succ} {i : ℕ} (h : i + 1 < n + 1) : Fin.cases zero succ ⟨i.succ, h⟩ = succ ⟨i, ⋯⟩
• Fin.addCases.eq_1 📋 Init.Data.Fin.Lemmas
  {m n : ℕ} {motive : Fin (m + n) → Sort u} (left : (i : Fin m) → motive (Fin.castAdd n i)) (right : (i : Fin n) → motive (Fin.natAdd m i)) (i : Fin (m + n)) : Fin.addCases left right i = if hi : ↑i < m then ⋯ ▸ left (i.castLT hi) else ⋯ ▸ right (Fin.subNat m (Fin.cast ⋯ i) ⋯)
• Fin.snocCases 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} {P : ((i : Fin n.succ) → α i) → Sort u_2} (h : (xs : (i : Fin n) → α i.castSucc) → (x : α (Fin.last n)) → P (Fin.snoc xs x)) (x : (i : Fin n.succ) → α i) : P x
• Fin.succAboveCases 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (i.succAbove j)) (j : Fin (n + 1)) : α j
• Fin.succAbove_cases_eq_insertNth 📋 Mathlib.Data.Fin.Tuple.Basic
  : @Fin.succAboveCases = @Fin.insertNth
• Fin.consCases 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u} {P : ((i : Fin n.succ) → α i) → Sort v} (h : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → P (Fin.cons x₀ x)) (x : (i : Fin n.succ) → α i) : P x
• Fin.snocCases.eq_1 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} {P : ((i : Fin n.succ) → α i) → Sort u_2} (h : (xs : (i : Fin n) → α i.castSucc) → (x : α (Fin.last n)) → P (Fin.snoc xs x)) (x : (i : Fin n.succ) → α i) : Fin.snocCases h x = cast ⋯ (h (Fin.init x) (x (Fin.last n)))
• Fin.snocCases_snoc 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u_1} {P : ((i : Fin (n + 1)) → α i) → Sort u_2} (h : (x : (i : Fin n) → α i.castSucc) → (x₀ : α (Fin.last n)) → P (Fin.snoc x x₀)) (x : (i : Fin n) → Fin.init α i) (x₀ : α (Fin.last n)) : Fin.snocCases h (Fin.snoc x x₀) = h x x₀
• Fin.consCases.eq_1 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u} {P : ((i : Fin n.succ) → α i) → Sort v} (h : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → P (Fin.cons x₀ x)) (x : (i : Fin n.succ) → α i) : Fin.consCases h x = cast ⋯ (h (x 0) (Fin.tail x))
• Fin.consCases_cons 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u} {P : ((i : Fin n.succ) → α i) → Sort v} (h : (x₀ : α 0) → (x : (i : Fin n) → α i.succ) → P (Fin.cons x₀ x)) (x₀ : α 0) (x : (i : Fin n) → α i.succ) : Fin.consCases h (Fin.cons x₀ x) = h x₀ x
• Fin.succAboveCases.eq_1 📋 Mathlib.Data.Fin.Tuple.Basic
  {n : ℕ} {α : Fin (n + 1) → Sort u} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (i.succAbove j)) (j : Fin (n + 1)) : i.succAboveCases x p j = if hj : j = i then ⋯ ▸ x else if hlt : j < i then Eq.recOn ⋯ (p (j.castPred ⋯)) else Eq.recOn ⋯ (p (j.pred ⋯))
• Fin.take_addCases_left 📋 Mathlib.Data.Fin.Tuple.Take
  {n n' : ℕ} {motive : Fin (n + n') → Sort u_2} (m : ℕ) (h : m ≤ n) (u : (i : Fin n) → motive (Fin.castAdd n' i)) (v : (i : Fin n') → motive (Fin.natAdd n i)) : (Fin.take m ⋯ fun i => Fin.addCases u v i) = Fin.take m h u
• Fin.take_addCases_right 📋 Mathlib.Data.Fin.Tuple.Take
  {n n' : ℕ} {motive : Fin (n + n') → Sort u_2} (m : ℕ) (h : m ≤ n') (u : (i : Fin n) → motive (Fin.castAdd n' i)) (v : (i : Fin n') → motive (Fin.natAdd n i)) : (Fin.take (n + m) ⋯ fun i => Fin.addCases u v i) = fun i => Fin.addCases u (Fin.take m h v) i

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 4e1aab0 serving mathlib revision b513113