Loogle!

Result

Found 247 definitions mentioning List and Fin. Of these, only the first 200 are shown.

• List.get 📋 Init.Prelude
  {α : Type u} (as : List α) : Fin as.length → α
• List.sizeOf_get 📋 Init.Data.List.BasicAux
  {α : Type u_1} [SizeOf α] (as : List α) (i : Fin as.length) : sizeOf (as.get i) < sizeOf as
• List.get_last 📋 Init.Data.List.BasicAux
  {α : Type u_1} {a : α} {as : List α} {i : Fin (as ++ [a]).length} (h : ¬↑i < as.length) : (as ++ [a]).get i = a
• List.get_cons_succ' 📋 Init.Data.List.Lemmas
  {α : Type u_1} {a : α} {as : List α} {i : Fin as.length} : (a :: as).get i.succ = as.get i
• List.get_of_mem 📋 Init.Data.List.Lemmas
  {α : Type u_1} {a : α} {l : List α} (h : a ∈ l) : ∃ n, l.get n = a
• List.mem_iff_get 📋 Init.Data.List.Lemmas
  {α : Type u_1} {a : α} {l : List α} : a ∈ l ↔ ∃ n, l.get n = a
• List.get_eq_getElem 📋 Init.Data.List.Lemmas
  {α : Type u_1} (l : List α) (i : Fin l.length) : l.get i = l[↑i]
• List.get_cons_zero 📋 Init.Data.List.Lemmas
  {α✝ : Type u_1} {a : α✝} {l : List α✝} : (a :: l).get 0 = a
• List.get_of_eq 📋 Init.Data.List.Lemmas
  {α : Type u_1} {l l' : List α} (h : l = l') (i : Fin l.length) : l.get i = l'.get ⟨↑i, ⋯⟩
• List.get_cons_cons_one 📋 Init.Data.List.Lemmas
  {α✝ : Type u_1} {a₁ a₂ : α✝} {as : List α✝} : (a₁ :: a₂ :: as).get 1 = a₂
• List.get_map 📋 Init.Data.List.Lemmas
  {α : Type u_1} {β : Type u_2} (f : α → β) {l : List α} {n : Fin (List.map f l).length} : (List.map f l).get n = f (l.get ⟨↑n, ⋯⟩)
• List.get_dropLast 📋 Init.Data.List.Lemmas
  {α : Type u_1} (xs : List α) (i : Fin xs.dropLast.length) : xs.dropLast.get i = xs.get ⟨↑i, ⋯⟩
• List.get_cons_drop 📋 Init.Data.List.TakeDrop
  {α : Type u_1} (l : List α) (i : Fin l.length) : l.get i :: List.drop (↑i + 1) l = List.drop (↑i) l
• List.get_take' 📋 Init.Data.List.Nat.TakeDrop
  {α : Type u_1} (L : List α) {j : ℕ} {i : Fin (List.take j L).length} : (List.take j L).get i = L.get ⟨↑i, ⋯⟩
• List.get_drop' 📋 Init.Data.List.Nat.TakeDrop
  {α : Type u_1} (L : List α) {i : ℕ} {j : Fin (List.drop i L).length} : (List.drop i L).get j = L.get ⟨i + ↑j, ⋯⟩
• List.map_get_sublist 📋 Init.Data.List.Nat.Pairwise
  {α : Type u_1} {l : List α} {is : List (Fin l.length)} (h : List.Pairwise (fun x1 x2 => ↑x1 < ↑x2) is) : (List.map l.get is).Sublist l
• List.sublist_eq_map_get 📋 Init.Data.List.Nat.Pairwise
  {α✝ : Type u_1} {l' l : List α✝} (h : l'.Sublist l) : ∃ is, l' = List.map l.get is ∧ List.Pairwise (fun x1 x2 => x1 < x2) is
• List.map_getElem_sublist 📋 Init.Data.List.Nat.Pairwise
  {α : Type u_1} {l : List α} {is : List (Fin l.length)} (h : List.Pairwise (fun x1 x2 => x1 < x2) is) : (List.map (fun x => l[x]) is).Sublist l
• List.sublist_eq_map_getElem 📋 Init.Data.List.Nat.Pairwise
  {α : Type u_1} {l l' : List α} (h : l'.Sublist l) : ∃ is, l' = List.map (fun x => l[x]) is ∧ List.Pairwise (fun x1 x2 => x1 < x2) is
• Array.data_set 📋 Init.Data.Array.Lemmas
  {α : Type u_1} (a : Array α) (i : Fin a.size) (v : α) : (a.set i v).toList = a.toList.set (↑i) v
• Array.toList_set 📋 Init.Data.Array.Lemmas
  {α : Type u_1} (a : Array α) (i : Fin a.size) (v : α) : (a.set i v).toList = a.toList.set (↑i) v
• List.set_toArray 📋 Init.Data.Array.Lemmas
  {α : Type u_1} (l : List α) (i : Fin l.toArray.size) (a : α) : l.toArray.set i a = (l.set (↑i) a).toArray
• Array.data_swap 📋 Init.Data.Array.Lemmas
  {α : Type u_1} (a : Array α) (i j : Fin a.size) : (a.swap i j).toList = (a.toList.set (↑i) (a.get j)).set (↑j) (a.get i)
• Array.toList_swap 📋 Init.Data.Array.Lemmas
  {α : Type u_1} (a : Array α) (i j : Fin a.size) : (a.swap i j).toList = (a.toList.set (↑i) (a.get j)).set (↑j) (a.get i)
• Array.getElem_fin_eq_data_get 📋 Init.Data.Array.Lemmas
  {α : Type u_1} (a : Array α) (i : Fin a.size) : a[i] = a.toList[i]
• Array.getElem_fin_eq_getElem_toList 📋 Init.Data.Array.Lemmas
  {α : Type u_1} (a : Array α) (i : Fin a.size) : a[i] = a.toList[i]
• Array.getElem_fin_eq_toList_get 📋 Init.Data.Array.Lemmas
  {α : Type u_1} (a : Array α) (i : Fin a.size) : a[i] = a.toList[i]
• List.swap_toArray 📋 Init.Data.Array.Lemmas
  {α : Type u_1} (l : List α) (i j : Fin l.toArray.size) : l.toArray.swap i j = ((l.set (↑i) l[j]).set (↑j) l[i]).toArray
• List.ofFn 📋 Batteries.Data.List.Basic
  {α : Type u_1} {n : ℕ} (f : Fin n → α) : List α
• List.get_eq_iff 📋 Batteries.Data.List.Lemmas
  {α✝ : Type u_1} {l : List α✝} {n : Fin l.length} {x : α✝} : l.get n = x ↔ l.get? ↑n = some x
• Fin.list 📋 Batteries.Data.Fin.Basic
  (n : ℕ) : List (Fin n)
• Fin.list.eq_1 📋 Batteries.Data.Fin.Lemmas
  (n : ℕ) : Fin.list n = (Fin.enum n).toList
• Fin.list_reverse 📋 Batteries.Data.Fin.Lemmas
  (n : ℕ) : (Fin.list n).reverse = List.map Fin.rev (Fin.list n)
• Fin.list_zero 📋 Batteries.Data.Fin.Lemmas
  : Fin.list 0 = []
• Fin.getElem_list 📋 Batteries.Data.Fin.Lemmas
  {n : ℕ} (i : ℕ) (h : i < (Fin.list n).length) : (Fin.list n)[i] = Fin.cast ⋯ ⟨i, h⟩
• Fin.list_succ 📋 Batteries.Data.Fin.Lemmas
  (n : ℕ) : Fin.list (n + 1) = 0 :: List.map Fin.succ (Fin.list n)
• Fin.list_succ_last 📋 Batteries.Data.Fin.Lemmas
  (n : ℕ) : Fin.list (n + 1) = List.map Fin.castSucc (Fin.list n) ++ [Fin.last n]
• List.ofFn.eq_1 📋 Batteries.Data.List.OfFn
  {α : Type u_1} {n : ℕ} (f : Fin n → α) : List.ofFn f = Fin.foldr n (fun x1 x2 => f x1 :: x2) []
• List.getElem?_ofFn 📋 Batteries.Data.List.OfFn
  {n : ℕ} {α : Type u_1} (f : Fin n → α) (i : ℕ) : (List.ofFn f)[i]? = List.ofFnNthVal f i
• List.getElem_ofFn 📋 Batteries.Data.List.OfFn
  {n : ℕ} {α : Type u_1} (f : Fin n → α) (i : ℕ) (h : i < (List.ofFn f).length) : (List.ofFn f)[i] = f ⟨i, ⋯⟩
• Array.toList_ofFn 📋 Batteries.Data.Array.OfFn
  {n : ℕ} {α : Type u_1} (f : Fin n → α) : (Array.ofFn f).toList = List.ofFn f
• List.pairwise_iff_get 📋 Batteries.Data.List.Pairwise
  {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {l : List α✝} : List.Pairwise R l ↔ ∀ (i j : Fin l.length), i < j → R (l.get i) (l.get j)
• List.mem_eraseIdx_iff_get 📋 Batteries.Data.List.EraseIdx
  {α : Type u} {x : α} {l : List α} {k : ℕ} : x ∈ l.eraseIdx k ↔ ∃ i, ↑i ≠ k ∧ l.get i = x
• Batteries.Linter.UnnecessarySeqFocus.getPath 📋 Batteries.Linter.UnnecessarySeqFocus
  : Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → List ((n : ℕ) × Fin n) → Option Lean.Elab.Info
• Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.existsRatHint_of_ratHintsExhaustive 📋 Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
  {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_readyForRatAdd : f.ReadyForRatAdd) (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (ratHints : Array (ℕ × Array ℕ)) (ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true) (c' : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (c'_in_f : c' ∈ f.toList) (negPivot_in_c' : pivot.negate ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c') : ∃ i, f.clauses[ratHints[i].1]! = some c'
• List.finRange 📋 Mathlib.Data.List.Defs
  (n : ℕ) : List (Fin n)
• List.erase_get 📋 Mathlib.Data.List.Basic
  {ι : Type u_1} [DecidableEq ι] {l : List ι} (i : Fin l.length) : (l.erase (l.get i)).Perm (l.eraseIdx ↑i)
• List.cons_get_drop_succ 📋 Mathlib.Data.List.Basic
  {α : Type u} {l : List α} {n : Fin l.length} : l.get n :: List.drop (↑n + 1) l = List.drop (↑n) l
• List.get_map_rev 📋 Mathlib.Data.List.Basic
  {α : Type u} {β : Type v} (f : α → β) {l : List α} {n : Fin l.length} : f (l.get n) = (List.map f l).get ⟨↑n, ⋯⟩
• List.get_reverse' 📋 Mathlib.Data.List.Basic
  {α : Type u} (l : List α) (n : Fin l.reverse.length) (hn' : l.length - 1 - ↑n < l.length) : l.reverse.get n = l.get ⟨l.length - 1 - ↑n, hn'⟩
• List.get_attach 📋 Mathlib.Data.List.Basic
  {α : Type u} (L : List α) (i : Fin L.attach.length) : ↑(L.attach.get i) = L.get ⟨↑i, ⋯⟩
• List.get_eq_get? 📋 Mathlib.Data.List.Basic
  {α : Type u} (l : List α) (i : Fin l.length) : l.get i = (l.get? ↑i).get ⋯
• List.nodup_iff_injective_get 📋 Mathlib.Data.List.Nodup
  {α : Type u} {l : List α} : l.Nodup ↔ Function.Injective l.get
• List.get_indexOf 📋 Mathlib.Data.List.Nodup
  {α : Type u} [DecidableEq α] {l : List α} (H : l.Nodup) (i : Fin l.length) : List.indexOf (l.get i) l = ↑i
• List.not_nodup_of_get_eq_of_ne 📋 Mathlib.Data.List.Nodup
  {α : Type u} (xs : List α) (n m : Fin xs.length) (h : xs.get n = xs.get m) (hne : n ≠ m) : ¬xs.Nodup
• List.Nodup.get_inj_iff 📋 Mathlib.Data.List.Nodup
  {α : Type u} {l : List α} (h : l.Nodup) {i j : Fin l.length} : l.get i = l.get j ↔ i = j
• List.Nodup.erase_get 📋 Mathlib.Data.List.Nodup
  {α : Type u} [DecidableEq α] {l : List α} (hl : l.Nodup) (i : Fin l.length) : l.erase (l.get i) = l.eraseIdx ↑i
• List.nodup_iff_injective_getElem 📋 Mathlib.Data.List.Nodup
  {α : Type u} {l : List α} : l.Nodup ↔ Function.Injective fun i => l[↑i]
• List.drop_take_succ_eq_cons_get 📋 Mathlib.Data.List.Flatten
  {α : Type u_1} (L : List α) (i : Fin L.length) : List.drop (↑i) (List.take (↑i + 1) L) = [L.get i]
• List.drop_take_succ_join_eq_get' 📋 Mathlib.Data.List.Flatten
  {α : Type u_1} (L : List (List α)) (i : Fin L.length) : List.drop (Nat.sum (List.take (↑i) (List.map List.length L))) (List.take (Nat.sum (List.take (↑i + 1) (List.map List.length L))) L.flatten) = L.get i
• List.mem_finRange 📋 Mathlib.Data.List.Range
  {n : ℕ} (a : Fin n) : a ∈ List.finRange n
• List.finRange_eq_nil 📋 Mathlib.Data.List.Range
  {n : ℕ} : List.finRange n = [] ↔ n = 0
• List.finRange_map_get 📋 Mathlib.Data.List.Range
  {α : Type u} (l : List α) : List.map l.get (List.finRange l.length) = l
• List.finRange_zero 📋 Mathlib.Data.List.Range
  : List.finRange 0 = []
• List.finRange.eq_1 📋 Mathlib.Data.List.Range
  (n : ℕ) : List.finRange n = List.pmap Fin.mk (List.range n) ⋯
• List.getElem_finRange 📋 Mathlib.Data.List.Range
  {n i : ℕ} (h : i < (List.finRange n).length) : (List.finRange n)[i] = ⟨i, ⋯⟩
• List.get_inits 📋 Mathlib.Data.List.Infix
  {α : Type u_1} (l : List α) (n : Fin l.inits.length) : l.inits.get n = List.take (↑n) l
• List.get_tails 📋 Mathlib.Data.List.Infix
  {α : Type u_1} (l : List α) (n : Fin l.tails.length) : l.tails.get n = List.drop (↑n) l
• List.get_cyclicPermutations 📋 Mathlib.Data.List.Rotate
  {α : Type u} (l : List α) (n : Fin l.cyclicPermutations.length) : l.cyclicPermutations.get n = l.rotate ↑n
• List.get_rotate 📋 Mathlib.Data.List.Rotate
  {α : Type u} (l : List α) (n : ℕ) (k : Fin (l.rotate n).length) : (l.rotate n).get k = l.get ⟨(↑k + n) % l.length, ⋯⟩
• List.get_rotate_one 📋 Mathlib.Data.List.Rotate
  {α : Type u} (l : List α) (k : Fin (l.rotate 1).length) : (l.rotate 1).get k = l.get ⟨(↑k + 1) % l.length, ⋯⟩
• List.nthLe_rotate_one 📋 Mathlib.Data.List.Rotate
  {α : Type u} (l : List α) (k : Fin (l.rotate 1).length) : (l.rotate 1).get k = l.get ⟨(↑k + 1) % l.length, ⋯⟩
• List.get_eq_get_rotate 📋 Mathlib.Data.List.Rotate
  {α : Type u} (l : List α) (n : ℕ) (k : Fin l.length) : l.get k = (l.rotate n).get ⟨(l.length - n % l.length + ↑k) % l.length, ⋯⟩
• List.drop_take_succ_join_eq_get 📋 Mathlib.Algebra.BigOperators.Group.List
  {α : Type u_2} (L : List (List α)) (i : Fin L.length) : List.drop (List.take (↑i) (List.map List.length L)).sum (List.take (List.take (↑i + 1) (List.map List.length L)).sum L.flatten) = L.get i
• Set.range_list_get 📋 Mathlib.Data.Set.List
  {α : Type u_1} (l : List α) : Set.range l.get = {x | x ∈ l}
• Set.range_list_nthLe 📋 Mathlib.Data.Set.List
  {α : Type u_1} (l : List α) : Set.range l.get = {x | x ∈ l}
• List.equivSigmaTuple 📋 Mathlib.Data.List.OfFn
  {α : Type u} : List α ≃ (n : ℕ) × (Fin n → α)
• List.ofFn_injective 📋 Mathlib.Data.List.OfFn
  {α : Type u} {n : ℕ} : Function.Injective List.ofFn
• List.ofFn_const 📋 Mathlib.Data.List.OfFn
  {α : Type u} (n : ℕ) (c : α) : (List.ofFn fun x => c) = List.replicate n c
• List.ofFnRec 📋 Mathlib.Data.List.OfFn
  {α : Type u} {C : List α → Sort u_1} (h : (n : ℕ) → (f : Fin n → α) → C (List.ofFn f)) (l : List α) : C l
• List.forall_iff_forall_tuple 📋 Mathlib.Data.List.OfFn
  {α : Type u} {P : List α → Prop} : (∀ (l : List α), P l) ↔ ∀ (n : ℕ) (f : Fin n → α), P (List.ofFn f)
• List.ofFn_zero 📋 Mathlib.Data.List.OfFn
  {α : Type u} (f : Fin 0 → α) : List.ofFn f = []
• List.ofFn_eq_nil_iff 📋 Mathlib.Data.List.OfFn
  {α : Type u} {n : ℕ} {f : Fin n → α} : List.ofFn f = [] ↔ n = 0
• List.ofFn_inj 📋 Mathlib.Data.List.OfFn
  {α : Type u} {n : ℕ} {f g : Fin n → α} : List.ofFn f = List.ofFn g ↔ f = g
• List.exists_iff_exists_tuple 📋 Mathlib.Data.List.OfFn
  {α : Type u} {P : List α → Prop} : (∃ l, P l) ↔ ∃ n f, P (List.ofFn f)
• List.forall_mem_ofFn_iff 📋 Mathlib.Data.List.OfFn
  {α : Type u} {n : ℕ} {f : Fin n → α} {P : α → Prop} : (∀ i ∈ List.ofFn f, P i) ↔ ∀ (j : Fin n), P (f j)
• List.ofFn_get_eq_map 📋 Mathlib.Data.List.OfFn
  {α : Type u} {β : Type u_1} (l : List α) (f : α → β) : (List.ofFn fun x => f (l.get x)) = List.map f l
• List.ofFn_succ' 📋 Mathlib.Data.List.OfFn
  {α : Type u} {n : ℕ} (f : Fin n.succ → α) : List.ofFn f = (List.ofFn fun i => f i.castSucc).concat (f (Fin.last n))
• List.map_ofFn 📋 Mathlib.Data.List.OfFn
  {α : Type u} {β : Type u_1} {n : ℕ} (f : Fin n → α) (g : α → β) : List.map g (List.ofFn f) = List.ofFn (g ∘ f)
• List.mem_ofFn 📋 Mathlib.Data.List.OfFn
  {α : Type u} {n : ℕ} (f : Fin n → α) (a : α) : a ∈ List.ofFn f ↔ a ∈ Set.range f
• List.ofFn_congr 📋 Mathlib.Data.List.OfFn
  {α : Type u} {m n : ℕ} (h : m = n) (f : Fin m → α) : List.ofFn f = List.ofFn fun i => f (Fin.cast ⋯ i)
• List.ofFnRec_ofFn 📋 Mathlib.Data.List.OfFn
  {α : Type u} {C : List α → Sort u_1} (h : (n : ℕ) → (f : Fin n → α) → C (List.ofFn f)) {n : ℕ} (f : Fin n → α) : List.ofFnRec h (List.ofFn f) = h n f
• List.ofFn_fin_repeat 📋 Mathlib.Data.List.OfFn
  {α : Type u} {m : ℕ} (a : Fin m → α) (n : ℕ) : List.ofFn (Fin.repeat n a) = (List.replicate n (List.ofFn a)).flatten
• List.ofFn_succ 📋 Mathlib.Data.List.OfFn
  {α : Type u} {n : ℕ} (f : Fin n.succ → α) : List.ofFn f = f 0 :: List.ofFn fun i => f i.succ
• List.ofFn_inj' 📋 Mathlib.Data.List.OfFn
  {α : Type u} {m n : ℕ} {f : Fin m → α} {g : Fin n → α} : List.ofFn f = List.ofFn g ↔ ⟨m, f⟩ = ⟨n, g⟩
• List.equivSigmaTuple_apply_fst 📋 Mathlib.Data.List.OfFn
  {α : Type u} (l : List α) : (List.equivSigmaTuple l).fst = l.length
• List.ofFn_fin_append 📋 Mathlib.Data.List.OfFn
  {α : Type u} {m n : ℕ} (a : Fin m → α) (b : Fin n → α) : List.ofFn (Fin.append a b) = List.ofFn a ++ List.ofFn b
• List.ofFn_cons 📋 Mathlib.Data.List.OfFn
  {α : Type u} {n : ℕ} (a : α) (f : Fin n → α) : List.ofFn (Fin.cons a f) = a :: List.ofFn f
• List.equivSigmaTuple_apply_snd 📋 Mathlib.Data.List.OfFn
  {α : Type u} (l : List α) (a✝ : Fin l.length) : (List.equivSigmaTuple l).snd a✝ = l.get a✝
• List.ofFn_add 📋 Mathlib.Data.List.OfFn
  {α : Type u} {m n : ℕ} (f : Fin (m + n) → α) : List.ofFn f = (List.ofFn fun i => f (Fin.castAdd n i)) ++ List.ofFn fun j => f (Fin.natAdd m j)
• List.ofFn_getElem 📋 Mathlib.Data.List.OfFn
  {α : Type u} (l : List α) : (List.ofFn fun i => l[↑i]) = l
• List.getLast_ofFn_succ 📋 Mathlib.Data.List.OfFn
  {α : Type u} {n : ℕ} (f : Fin n.succ → α) : (List.ofFn f).getLast ⋯ = f (Fin.last n)
• List.ofFn_getElem_eq_map 📋 Mathlib.Data.List.OfFn
  {α : Type u} {β : Type u_1} (l : List α) (f : α → β) : (List.ofFn fun i => f l[↑i]) = List.map f l
• List.equivSigmaTuple_symm_apply 📋 Mathlib.Data.List.OfFn
  {α : Type u} (f : (n : ℕ) × (Fin n → α)) : List.equivSigmaTuple.symm f = List.ofFn f.snd
• List.head_ofFn 📋 Mathlib.Data.List.OfFn
  {α : Type u} {n : ℕ} (f : Fin n → α) (h : List.ofFn f ≠ []) : (List.ofFn f).head h = f ⟨0, ⋯⟩
• List.last_ofFn_succ 📋 Mathlib.Data.List.OfFn
  {α : Type u} {n : ℕ} (f : Fin n.succ → α) (h : List.ofFn f ≠ [] := ⋯) : (List.ofFn f).getLast h = f (Fin.last n)
• List.getLast_ofFn 📋 Mathlib.Data.List.OfFn
  {α : Type u} {n : ℕ} (f : Fin n → α) (h : List.ofFn f ≠ []) : (List.ofFn f).getLast h = f ⟨n - 1, ⋯⟩
• List.last_ofFn 📋 Mathlib.Data.List.OfFn
  {α : Type u} {n : ℕ} (f : Fin n → α) (h : List.ofFn f ≠ []) (hn : n - 1 < n := ⋯) : (List.ofFn f).getLast h = f ⟨n - 1, hn⟩
• List.ofFn_mul 📋 Mathlib.Data.List.OfFn
  {α : Type u} {m n : ℕ} (f : Fin (m * n) → α) : List.ofFn f = (List.ofFn fun i => List.ofFn fun j => f ⟨↑i * n + ↑j, ⋯⟩).flatten
• List.ofFn_mul' 📋 Mathlib.Data.List.OfFn
  {α : Type u} {m n : ℕ} (f : Fin (m * n) → α) : List.ofFn f = (List.ofFn fun i => List.ofFn fun j => f ⟨m * ↑i + ↑j, ⋯⟩).flatten
• List.map_coe_finRange 📋 Mathlib.Data.List.FinRange
  (n : ℕ) : List.map Fin.val (List.finRange n) = List.range n
• List.ofFn_id 📋 Mathlib.Data.List.FinRange
  (n : ℕ) : List.ofFn id = List.finRange n
• List.ofFn_eq_map 📋 Mathlib.Data.List.FinRange
  {α : Type u} {n : ℕ} {f : Fin n → α} : List.ofFn f = List.map f (List.finRange n)
• List.finRange_succ 📋 Mathlib.Data.List.FinRange
  (n : ℕ) : List.finRange n.succ = (List.map Fin.castSucc (List.finRange n)).concat (Fin.last n)
• List.ofFn_eq_pmap 📋 Mathlib.Data.List.FinRange
  {α : Type u} {n : ℕ} {f : Fin n → α} : List.ofFn f = List.pmap (fun i hi => f ⟨i, hi⟩) (List.range n) ⋯
• List.finRange_succ_eq_map 📋 Mathlib.Data.List.FinRange
  (n : ℕ) : List.finRange n.succ = 0 :: List.map Fin.succ (List.finRange n)
• Fin.univ_image_get 📋 Mathlib.Data.Fintype.Basic
  {α : Type u_1} [DecidableEq α] (l : List α) : Finset.image l.get Finset.univ = l.toFinset
• Fin.univ_image_get' 📋 Mathlib.Data.Fintype.Basic
  {α : Type u_1} {β : Type u_2} [DecidableEq β] (l : List α) (f : α → β) : Finset.image (fun x => f (l.get x)) Finset.univ = (List.map f l).toFinset
• Fin.univ_image_getElem' 📋 Mathlib.Data.Fintype.Basic
  {α : Type u_1} {β : Type u_2} [DecidableEq β] (l : List α) (f : α → β) : Finset.image (fun i => f l[↑i]) Finset.univ = (List.map f l).toFinset
• List.get_zip 📋 Mathlib.Data.List.Zip
  {α : Type u} {β : Type u_1} {l : List α} {l' : List β} {i : Fin (l.zip l').length} : (l.zip l').get i = (l.get ⟨↑i, ⋯⟩, l'.get ⟨↑i, ⋯⟩)
• List.get_zipWith 📋 Mathlib.Data.List.Zip
  {α : Type u} {β : Type u_1} {γ : Type u_2} {f : α → β → γ} {l : List α} {l' : List β} {i : Fin (List.zipWith f l l').length} : (List.zipWith f l l').get i = f (l.get ⟨↑i, ⋯⟩) (l'.get ⟨↑i, ⋯⟩)
• List.Sorted.rel_get_of_lt 📋 Mathlib.Data.List.Sort
  {α : Type u} {r : α → α → Prop} {l : List α} (h : List.Sorted r l) {a b : Fin l.length} (hab : a < b) : r (l.get a) (l.get b)
• List.Sorted.rel_get_of_le 📋 Mathlib.Data.List.Sort
  {α : Type u} {r : α → α → Prop} [IsRefl α r] {l : List α} (h : List.Sorted r l) {a b : Fin l.length} (hab : a ≤ b) : r (l.get a) (l.get b)
• List.Nodup.getEquivOfForallMemList 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [DecidableEq α] (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x ∈ l) : Fin l.length ≃ α
• List.Nodup.getEquiv 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [DecidableEq α] (l : List α) (H : l.Nodup) : Fin l.length ≃ { x // x ∈ l }
• List.Nodup.getBijectionOfForallMemList 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x ∈ l) : { f // Function.Bijective f }
• List.Sorted.get_mono 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [Preorder α] {l : List α} (h : List.Sorted (fun x1 x2 => x1 ≤ x2) l) : Monotone l.get
• List.Sorted.get_strictMono 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [Preorder α] {l : List α} (h : List.Sorted (fun x1 x2 => x1 < x2) l) : StrictMono l.get
• List.Nodup.getBijectionOfForallMemList_coe 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x ∈ l) (i : Fin l.length) : ↑(List.Nodup.getBijectionOfForallMemList l nd h) i = l.get i
• List.Sorted.getIso 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [Preorder α] [DecidableEq α] (l : List α) (H : List.Sorted (fun x1 x2 => x1 < x2) l) : Fin l.length ≃o { x // x ∈ l }
• List.Nodup.getEquivOfForallMemList_apply 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [DecidableEq α] (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x ∈ l) (i : Fin l.length) : (List.Nodup.getEquivOfForallMemList l nd h) i = l.get i
• List.Nodup.getEquivOfForallMemList_symm_apply_val 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [DecidableEq α] (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x ∈ l) (a : α) : ↑((List.Nodup.getEquivOfForallMemList l nd h).symm a) = List.indexOf a l
• List.duplicate_iff_exists_distinct_get 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} {l : List α} {x : α} : List.Duplicate x l ↔ ∃ n m, ∃ (_ : n < m), x = l.get n ∧ x = l.get m
• List.Nodup.getEquiv_apply_coe 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [DecidableEq α] (l : List α) (H : l.Nodup) (i : Fin l.length) : ↑((List.Nodup.getEquiv l H) i) = l.get i
• List.Nodup.getEquiv_symm_apply_val 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [DecidableEq α] (l : List α) (H : l.Nodup) (x : { x // x ∈ l }) : ↑((List.Nodup.getEquiv l H).symm x) = List.indexOf (↑x) l
• List.sublist_iff_exists_fin_orderEmbedding_get_eq 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} {l l' : List α} : l.Sublist l' ↔ ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
• List.Sorted.coe_getIso_apply 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [Preorder α] {l : List α} [DecidableEq α] (H : List.Sorted (fun x1 x2 => x1 < x2) l) {i : Fin l.length} : ↑((List.Sorted.getIso l H) i) = l.get i
• List.Sorted.coe_getIso_symm_apply 📋 Mathlib.Data.List.NodupEquivFin
  {α : Type u_1} [Preorder α] {l : List α} [DecidableEq α] (H : List.Sorted (fun x1 x2 => x1 < x2) l) {x : { x // x ∈ l }} : ↑((List.Sorted.getIso l H).symm x) = List.indexOf (↑x) l
• Mathlib.Vector.toList_ofFn 📋 Mathlib.Data.Vector.Basic
  {α : Type u_1} {n : ℕ} (f : Fin n → α) : (Mathlib.Vector.ofFn f).toList = List.ofFn f
• Mathlib.Vector.toList_set 📋 Mathlib.Data.Vector.Basic
  {α : Type u_1} {n : ℕ} (v : Mathlib.Vector α n) (i : Fin n) (a : α) : (v.set i a).toList = v.toList.set (↑i) a
• Mathlib.Vector.set.eq_1 📋 Mathlib.Data.Vector.Basic
  {α : Type u_1} {n : ℕ} (v : Mathlib.Vector α n) (i : Fin n) (a : α) : v.set i a = ⟨(↑v).set (↑i) a, ⋯⟩
• Mathlib.Vector.eraseIdx_val 📋 Mathlib.Data.Vector.Basic
  {α : Type u_1} {n : ℕ} {i : Fin n} {v : Mathlib.Vector α n} : ↑(Mathlib.Vector.eraseIdx i v) = (↑v).eraseIdx ↑i
• Mathlib.Vector.eraseNth_val 📋 Mathlib.Data.Vector.Basic
  {α : Type u_1} {n : ℕ} {i : Fin n} {v : Mathlib.Vector α n} : ↑(Mathlib.Vector.eraseIdx i v) = (↑v).eraseIdx ↑i
• Mathlib.Vector.removeNth_val 📋 Mathlib.Data.Vector.Basic
  {α : Type u_1} {n : ℕ} {i : Fin n} {v : Mathlib.Vector α n} : ↑(Mathlib.Vector.eraseIdx i v) = (↑v).eraseIdx ↑i
• Mathlib.Vector.insertIdx_val 📋 Mathlib.Data.Vector.Basic
  {α : Type u_1} {n : ℕ} {a : α} {i : Fin (n + 1)} {v : Mathlib.Vector α n} : ↑(Mathlib.Vector.insertIdx a i v) = List.insertIdx (↑i) a ↑v
• Mathlib.Vector.insertNth_val 📋 Mathlib.Data.Vector.Basic
  {α : Type u_1} {n : ℕ} {a : α} {i : Fin (n + 1)} {v : Mathlib.Vector α n} : ↑(Mathlib.Vector.insertIdx a i v) = List.insertIdx (↑i) a ↑v
• Fin.prod_univ_get 📋 Mathlib.Algebra.BigOperators.Fin
  {α : Type u_1} [CommMonoid α] (l : List α) : ∏ i : Fin l.length, l[↑i] = l.prod
• Fin.sum_univ_get 📋 Mathlib.Algebra.BigOperators.Fin
  {α : Type u_1} [AddCommMonoid α] (l : List α) : ∑ i : Fin l.length, l[↑i] = l.sum
• Fin.prod_univ_get' 📋 Mathlib.Algebra.BigOperators.Fin
  {α : Type u_1} {β : Type u_2} [CommMonoid β] (l : List α) (f : α → β) : ∏ i : Fin l.length, f l[↑i] = (List.map f l).prod
• Fin.sum_univ_get' 📋 Mathlib.Algebra.BigOperators.Fin
  {α : Type u_1} {β : Type u_2} [AddCommMonoid β] (l : List α) (f : α → β) : ∑ i : Fin l.length, f l[↑i] = (List.map f l).sum
• List.alternatingProd_eq_finset_prod 📋 Mathlib.Algebra.BigOperators.Fin
  {G : Type u_3} [CommGroup G] (L : List G) : L.alternatingProd = ∏ i : Fin L.length, L[i] ^ (-1) ^ ↑i
• List.alternatingSum_eq_finset_sum 📋 Mathlib.Algebra.BigOperators.Fin
  {G : Type u_3} [AddCommGroup G] (L : List G) : L.alternatingSum = ∑ i : Fin L.length, (-1) ^ ↑i • L[i]
• Fin.sort_univ 📋 Mathlib.Data.Finset.Sort
  (n : ℕ) : Finset.sort (fun x y => x ≤ y) Finset.univ = List.finRange n
• Finset.orderEmbOfFin_apply 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} [LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k) (i : Fin k) : (s.orderEmbOfFin h) i = (Finset.sort (fun x1 x2 => x1 ≤ x2) s)[i]
• List.prev_get 📋 Mathlib.Data.List.Cycle
  {α : Type u_1} [DecidableEq α] (l : List α) (h : l.Nodup) (i : Fin l.length) : l.prev (l.get i) ⋯ = l.get ⟨(↑i + (l.length - 1)) % l.length, ⋯⟩
• List.next_get 📋 Mathlib.Data.List.Cycle
  {α : Type u_1} [DecidableEq α] (l : List α) (h : l.Nodup) (i : Fin l.length) : l.next (l.get i) ⋯ = l.get ⟨(↑i + 1) % l.length, ⋯⟩
• Composition.blocksFun_mem_blocks 📋 Mathlib.Combinatorics.Enumerative.Composition
  {n : ℕ} (c : Composition n) (i : Fin c.length) : c.blocksFun i ∈ c.blocks
• Composition.blocksFun_congr 📋 Mathlib.Combinatorics.Enumerative.Composition
  {n₁ n₂ : ℕ} (c₁ : Composition n₁) (c₂ : Composition n₂) (i₁ : Fin c₁.length) (i₂ : Fin c₂.length) (hn : n₁ = n₂) (hc : c₁.blocks = c₂.blocks) (hi : ↑i₁ = ↑i₂) : c₁.blocksFun i₁ = c₂.blocksFun i₂
• List.get_splitWrtComposition 📋 Mathlib.Combinatorics.Enumerative.Composition
  {n : ℕ} {α : Type u_1} (l : List α) (c : Composition n) (i : Fin (l.splitWrtComposition c).length) : (l.splitWrtComposition c).get i = List.drop (c.sizeUpTo ↑i) (List.take (c.sizeUpTo (↑i + 1)) l)
• List.formPerm_apply_get 📋 Mathlib.GroupTheory.Perm.List
  {α : Type u_1} [DecidableEq α] (xs : List α) (h : xs.Nodup) (i : Fin xs.length) : xs.formPerm (xs.get i) = xs.get ⟨(↑i + 1) % xs.length, ⋯⟩
• List.formPerm_pow_apply_get 📋 Mathlib.GroupTheory.Perm.List
  {α : Type u_1} [DecidableEq α] (l : List α) (h : l.Nodup) (n : ℕ) (i : Fin l.length) : (l.formPerm ^ n) (l.get i) = l.get ⟨(↑i + n) % l.length, ⋯⟩
• Equiv.Perm.signAux_eq_signAux2 📋 Mathlib.GroupTheory.Perm.Sign
  {α : Type u} [DecidableEq α] {n : ℕ} (l : List α) (f : Equiv.Perm α) (e : α ≃ Fin n) (_h : ∀ (x : α), f x ≠ x → x ∈ l) : Equiv.Perm.signAux ((e.symm.trans f).trans e) = Equiv.Perm.signAux2 l f
• Matrix.Pivot.listTransvecCol 📋 Mathlib.LinearAlgebra.Matrix.Transvection
  {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)
• Matrix.Pivot.listTransvecRow 📋 Mathlib.LinearAlgebra.Matrix.Transvection
  {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜)
• Matrix.Pivot.listTransvecCol.eq_1 📋 Mathlib.LinearAlgebra.Matrix.Transvection
  {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) : Matrix.Pivot.listTransvecCol M = List.ofFn fun i => Matrix.transvection (Sum.inl i) (Sum.inr ()) (-M (Sum.inl i) (Sum.inr ()) / M (Sum.inr ()) (Sum.inr ()))
• Matrix.Pivot.listTransvecRow.eq_1 📋 Mathlib.LinearAlgebra.Matrix.Transvection
  {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) : Matrix.Pivot.listTransvecRow M = List.ofFn fun i => Matrix.transvection (Sum.inr ()) (Sum.inl i) (-M (Sum.inr ()) (Sum.inl i) / M (Sum.inr ()) (Sum.inr ()))
• Matrix.Pivot.listTransvecCol_getElem 📋 Mathlib.LinearAlgebra.Matrix.Transvection
  {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) {i : ℕ} (h : i < (Matrix.Pivot.listTransvecCol M).length) : (Matrix.Pivot.listTransvecCol M)[i] = Matrix.transvection (Sum.inl ⟨i, ⋯⟩) (Sum.inr ()) (-M (Sum.inl ⟨i, ⋯⟩) (Sum.inr ()) / M (Sum.inr ()) (Sum.inr ()))
• Matrix.Pivot.listTransvecRow_getElem 📋 Mathlib.LinearAlgebra.Matrix.Transvection
  {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) {i : ℕ} (h : i < (Matrix.Pivot.listTransvecRow M).length) : (Matrix.Pivot.listTransvecRow M)[i] = Matrix.transvection (Sum.inr ()) (Sum.inl ⟨i, ⋯⟩) (-M (Sum.inr ()) (Sum.inl ⟨i, ⋯⟩) / M (Sum.inr ()) (Sum.inr ()))
• Matrix.Pivot.exists_isTwoBlockDiagonal_list_transvec_mul_mul_list_transvec 📋 Mathlib.LinearAlgebra.Matrix.Transvection
  {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) : ∃ L L', ((List.map Matrix.TransvectionStruct.toMatrix L).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L').prod).IsTwoBlockDiagonal
• Matrix.Pivot.exists_isTwoBlockDiagonal_of_ne_zero 📋 Mathlib.LinearAlgebra.Matrix.Transvection
  {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (hM : M (Sum.inr ()) (Sum.inr ()) ≠ 0) : ∃ L L', ((List.map Matrix.TransvectionStruct.toMatrix L).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L').prod).IsTwoBlockDiagonal
• Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction 📋 Mathlib.LinearAlgebra.Matrix.Transvection
  {𝕜 : Type u_3} [Field 𝕜] {r : ℕ} (IH : ∀ (M : Matrix (Fin r) (Fin r) 𝕜), ∃ L₀ L₀' D₀, (List.map Matrix.TransvectionStruct.toMatrix L₀).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L₀').prod = Matrix.diagonal D₀) (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) : ∃ L L' D, (List.map Matrix.TransvectionStruct.toMatrix L).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L').prod = Matrix.diagonal D
• RelSeries.fromListChain'_toFun 📋 Mathlib.Order.RelSeries
  {α : Type u_1} {r : Rel α α} (x : List α) (x_ne_nil : x ≠ []) (hx : List.Chain' r x) (i : Fin (x.length - 1 + 1)) : (RelSeries.fromListChain' x x_ne_nil hx).toFun i = x[Fin.cast ⋯ i]
• List.Nat.antidiagonalTuple 📋 Mathlib.Data.Fin.Tuple.NatAntidiagonal
  (k a✝ : ℕ) : List (Fin k → ℕ)
• List.Nat.antidiagonalTuple.eq_2 📋 Mathlib.Data.Fin.Tuple.NatAntidiagonal
  (n : ℕ) : List.Nat.antidiagonalTuple 0 n.succ = []
• List.Nat.antidiagonalTuple_zero_succ 📋 Mathlib.Data.Fin.Tuple.NatAntidiagonal
  (n : ℕ) : List.Nat.antidiagonalTuple 0 (n + 1) = []
• List.Nat.antidiagonalTuple_zero_zero 📋 Mathlib.Data.Fin.Tuple.NatAntidiagonal
  : List.Nat.antidiagonalTuple 0 0 = [![]]
• List.Nat.antidiagonalTuple.eq_1 📋 Mathlib.Data.Fin.Tuple.NatAntidiagonal
  : List.Nat.antidiagonalTuple 0 0 = [![]]
• List.Nat.mem_antidiagonalTuple 📋 Mathlib.Data.Fin.Tuple.NatAntidiagonal
  {n k : ℕ} {x : Fin k → ℕ} : x ∈ List.Nat.antidiagonalTuple k n ↔ ∑ i : Fin k, x i = n
• List.Nat.antidiagonalTuple_zero_right 📋 Mathlib.Data.Fin.Tuple.NatAntidiagonal
  (k : ℕ) : List.Nat.antidiagonalTuple k 0 = [0]
• List.Nat.antidiagonalTuple_one 📋 Mathlib.Data.Fin.Tuple.NatAntidiagonal
  (n : ℕ) : List.Nat.antidiagonalTuple 1 n = [![n]]
• List.Nat.antidiagonalTuple_two 📋 Mathlib.Data.Fin.Tuple.NatAntidiagonal
  (n : ℕ) : List.Nat.antidiagonalTuple 2 n = List.map (fun i => ![i.1, i.2]) (List.Nat.antidiagonal n)
• List.Nat.antidiagonalTuple.eq_3 📋 Mathlib.Data.Fin.Tuple.NatAntidiagonal
  (x✝ k : ℕ) : List.Nat.antidiagonalTuple k.succ x✝ = (List.Nat.antidiagonal x✝).flatMap fun ni => List.map (fun x => Fin.cons ni.1 x) (List.Nat.antidiagonalTuple k ni.2)
• Composition.sigmaCompositionAux.eq_1 📋 Mathlib.Analysis.Analytic.Composition
  {n : ℕ} (a : Composition n) (b : Composition a.length) (i : Fin (a.gather b).length) : a.sigmaCompositionAux b i = { blocks := (a.blocks.splitWrtComposition b)[↑i], blocks_pos := ⋯, blocks_sum := ⋯ }
• Composition.sigma_pi_composition_eq_iff 📋 Mathlib.Analysis.Analytic.Composition
  {n : ℕ} (u v : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))) : u = v ↔ (List.ofFn fun i => (u.snd i).blocks) = List.ofFn fun i => (v.snd i).blocks
• HasFDerivAt.list_prod' 📋 Mathlib.Analysis.Calculus.FDeriv.Mul
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {ι : Type u_5} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f : ι → E → 𝔸} {f' : ι → E →L[𝕜] 𝔸} {l : List ι} {x : E} (h : ∀ i ∈ l, HasFDerivAt (fun x => f i x) (f' i) x) : HasFDerivAt (fun x => (List.map (fun x_1 => f x_1 x) l).prod) (∑ i : Fin l.length, (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod • (f' l[i]).smulRight (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod) x
• HasStrictFDerivAt.list_prod' 📋 Mathlib.Analysis.Calculus.FDeriv.Mul
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {ι : Type u_5} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f : ι → E → 𝔸} {f' : ι → E →L[𝕜] 𝔸} {l : List ι} {x : E} (h : ∀ i ∈ l, HasStrictFDerivAt (fun x => f i x) (f' i) x) : HasStrictFDerivAt (fun x => (List.map (fun x_1 => f x_1 x) l).prod) (∑ i : Fin l.length, (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod • (f' l[i]).smulRight (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod) x
• HasFDerivWithinAt.list_prod' 📋 Mathlib.Analysis.Calculus.FDeriv.Mul
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {ι : Type u_5} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f : ι → E → 𝔸} {f' : ι → E →L[𝕜] 𝔸} {l : List ι} {x : E} (h : ∀ i ∈ l, HasFDerivWithinAt (fun x => f i x) (f' i) s x) : HasFDerivWithinAt (fun x => (List.map (fun x_1 => f x_1 x) l).prod) (∑ i : Fin l.length, (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod • (f' l[i]).smulRight (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod) s x
• fderiv_list_prod' 📋 Mathlib.Analysis.Calculus.FDeriv.Mul
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {ι : Type u_5} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f : ι → E → 𝔸} {l : List ι} {x : E} (h : ∀ i ∈ l, DifferentiableAt 𝕜 (fun x => f i x) x) : fderiv 𝕜 (fun x => (List.map (fun x_1 => f x_1 x) l).prod) x = ∑ i : Fin l.length, (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod • (fderiv 𝕜 (fun x => f l[i] x) x).smulRight (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod
• fderivWithin_list_prod' 📋 Mathlib.Analysis.Calculus.FDeriv.Mul
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {ι : Type u_5} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {f : ι → E → 𝔸} {l : List ι} {x : E} (hxs : UniqueDiffWithinAt 𝕜 s x) (h : ∀ i ∈ l, DifferentiableWithinAt 𝕜 (fun x => f i x) s x) : fderivWithin 𝕜 (fun x => (List.map (fun x_1 => f x_1 x) l).prod) s x = ∑ i : Fin l.length, (List.map (fun x_1 => f x_1 x) (List.take (↑i) l)).prod • (fderivWithin 𝕜 (fun x => f l[i] x) s x).smulRight (List.map (fun x_1 => f x_1 x) (List.drop (↑i).succ l)).prod
• hasStrictFDerivAt_list_prod' 📋 Mathlib.Analysis.Calculus.FDeriv.Mul
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_5} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] [Fintype ι] {l : List ι} {x : ι → 𝔸} : HasStrictFDerivAt (fun x => (List.map x l).prod) (∑ i : Fin l.length, (List.map x (List.take (↑i) l)).prod • (ContinuousLinearMap.proj l[i]).smulRight (List.map x (List.drop (↑i).succ l)).prod) x
• hasFDerivAt_list_prod' 📋 Mathlib.Analysis.Calculus.FDeriv.Mul
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_5} {𝔸' : Type u_7} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] [Fintype ι] {l : List ι} {x : ι → 𝔸'} : HasFDerivAt (fun x => (List.map x l).prod) (∑ i : Fin l.length, (List.map x (List.take (↑i) l)).prod • (ContinuousLinearMap.proj l[i]).smulRight (List.map x (List.drop (↑i).succ l)).prod) x
• hasFDerivAt_list_prod_attach' 📋 Mathlib.Analysis.Calculus.FDeriv.Mul
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_5} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] [DecidableEq ι] {l : List ι} {x : { i // i ∈ l } → 𝔸} : HasFDerivAt (fun x => (List.map x l.attach).prod) (∑ i : Fin l.length, (List.map x (List.take (↑i) l.attach)).prod • (ContinuousLinearMap.proj l.attach[Fin.cast ⋯ i]).smulRight (List.map x (List.drop (↑i).succ l.attach)).prod) x
• hasStrictFDerivAt_list_prod_attach' 📋 Mathlib.Analysis.Calculus.FDeriv.Mul
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_5} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] [DecidableEq ι] {l : List ι} {x : { i // i ∈ l } → 𝔸} : HasStrictFDerivAt (fun x => (List.map x l.attach).prod) (∑ i : Fin l.length, (List.map x (List.take (↑i) l.attach)).prod • (ContinuousLinearMap.proj l.attach[Fin.cast ⋯ i]).smulRight (List.map x (List.drop (↑i).succ l.attach)).prod) x
• YoungDiagram.rowLen_ofRowLens 📋 Mathlib.Combinatorics.Young.YoungDiagram
  {w : List ℕ} {hw : List.Sorted (fun x1 x2 => x1 ≥ x2) w} (i : Fin w.length) : (YoungDiagram.ofRowLens w hw).rowLen ↑i = w[i]
• Primrec.list_ofFn 📋 Mathlib.Computability.Primrec
  {α : Type u_1} {σ : Type u_3} [Primcodable α] [Primcodable σ] {n : ℕ} {f : Fin n → α → σ} : (∀ (i : Fin n), Primrec (f i)) → Primrec fun a => List.ofFn fun i => f i a
• List.mapIdx_eq_ofFn 📋 Mathlib.Data.List.Indexes
  {α : Type u} {β : Type v} (l : List α) (f : ℕ → α → β) : List.mapIdx f l = List.ofFn fun i => f (↑i) (l.get i)
• Computable.list_ofFn 📋 Mathlib.Computability.Partrec
  {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {n : ℕ} {f : Fin n → α → σ} : (∀ (i : Fin n), Computable (f i)) → Computable fun a => List.ofFn fun i => f i a
• Turing.ToPartrec.Code.exists_code.comp 📋 Mathlib.Computability.TMToPartrec
  {m n : ℕ} {f : Mathlib.Vector ℕ n →. ℕ} {g : Fin n → Mathlib.Vector ℕ m →. ℕ} (hf : ∃ c, ∀ (v : Mathlib.Vector ℕ n), c.eval ↑v = pure <$> f v) (hg : ∀ (i : Fin n), ∃ c, ∀ (v : Mathlib.Vector ℕ m), c.eval ↑v = pure <$> g i v) : ∃ c, ∀ (v : Mathlib.Vector ℕ m), c.eval ↑v = pure <$> ((Mathlib.Vector.mOfFn fun i => g i v) >>= f)
• Fin.ofFn_take_eq_take_ofFn 📋 Mathlib.Data.Fin.Tuple.Take
  {n : ℕ} {α : Type u_2} {m : ℕ} (h : m ≤ n) (v : Fin n → α) : List.ofFn (Fin.take m h v) = List.take m (List.ofFn v)
• Fin.ofFn_take_get 📋 Mathlib.Data.Fin.Tuple.Take
  {α : Type u_2} {m : ℕ} (l : List α) (h : m ≤ l.length) : List.ofFn (Fin.take m h l.get) = List.take m l

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 2d53f5f