Loogle!

Result

Found 250 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.findFinIdx? 📋 Init.Data.List.Basic
  {α : Type u} (p : α → Bool) (l : List α) : Option (Fin l.length)
• List.finIdxOf? 📋 Init.Data.List.Basic
  {α : Type u} [BEq α] (a : α) (l : List α) : Option (Fin l.length)
• List.findFinIdx?.go 📋 Init.Data.List.Basic
  {α : Type u} (p : α → Bool) (l l' : List α) (i : ℕ) (h : l'.length + i = l.length) : Option (Fin l.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_mem 📋 Init.Data.List.Lemmas
  {α : Type u_1} (l : List α) (n : Fin l.length) : l.get n ∈ l
• 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_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_zero 📋 Init.Data.List.Lemmas
  {α✝ : Type u_1} {a : α✝} {l : List α✝} : (a :: l).get 0 = a
• List.get_cons_cons_one 📋 Init.Data.List.Lemmas
  {α✝ : Type u_1} {a₁ a₂ : α✝} {as : List α✝} : (a₁ :: a₂ :: as).get 1 = a₂
• List.finIdxOf?.eq_1 📋 Init.Data.List.Find
  {α : Type u} [BEq α] (a : α) : List.finIdxOf? a = List.findFinIdx? fun x => x == a
• List.findFinIdx?.eq_1 📋 Init.Data.List.Find
  {α : Type u} (p : α → Bool) (l : List α) : List.findFinIdx? p l = List.findFinIdx?.go p l l 0 ⋯
• List.findIdx?_eq_map_findFinIdx?_val 📋 Init.Data.List.Find
  {α : Type u_1} {xs : List α} {p : α → Bool} : List.findIdx? p xs = Option.map (fun x => ↑x) (List.findFinIdx? p xs)
• List.idxOf?_eq_map_finIdxOf?_val 📋 Init.Data.List.Find
  {α : Type u_1} [BEq α] {xs : List α} {a : α} : List.idxOf? a xs = Option.map (fun x => ↑x) (List.finIdxOf? a xs)
• List.finIdxOf?_eq_none_iff 📋 Init.Data.List.Find
  {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} : List.finIdxOf? a l = none ↔ a ∉ l
• List.findFinIdx?_eq_none_iff 📋 Init.Data.List.Find
  {α : Type u_1} {l : List α} {p : α → Bool} : List.findFinIdx? p l = none ↔ ∀ x ∈ l, ¬p x = true
• List.findFinIdx?.go.eq_1 📋 Init.Data.List.Find
  {α : Type u} (p : α → Bool) (l : List α) (x : ℕ) (x_1 : [].length + x = l.length) : List.findFinIdx?.go p l [] x x_1 = none
• List.findIdx?_go_eq_map_findFinIdx?_go_val 📋 Init.Data.List.Find
  {α : Type u_1} {l xs : List α} {p : α → Bool} {i : ℕ} {h : xs.length + i = l.length} : List.findIdx?.go p xs i = Option.map (fun x => ↑x) (List.findFinIdx?.go p l xs i h)
• List.findFinIdx?.go.eq_2 📋 Init.Data.List.Find
  {α : Type u} (p : α → Bool) (l : List α) (x : ℕ) (a : α) (l_1 : List α) (x_1 : (a :: l_1).length + x = l.length) : List.findFinIdx?.go p l (a :: l_1) x x_1 = if p a = true then some ⟨x, ⋯⟩ else List.findFinIdx?.go p l l_1 (x + 1) ⋯
• List.findFinIdx?_cons 📋 Init.Data.List.Find
  {α : Type u_1} {p : α → Bool} {x : α} {xs : List α} : List.findFinIdx? p (x :: xs) = if p x = true then some 0 else Option.map Fin.succ (List.findFinIdx? p xs)
• List.finIdxOf?_cons 📋 Init.Data.List.Find
  {α : Type u_1} {b : α} [BEq α] (a : α) (xs : List α) : List.finIdxOf? b (a :: xs) = if (a == b) = true then some ⟨0, ⋯⟩ else Option.map (fun x => x.succ) (List.finIdxOf? b xs)
• List.findFinIdx?.go.eq_def 📋 Init.Data.List.Find
  {α : Type u} (p : α → Bool) (l x✝ : List α) (x✝¹ : ℕ) (x✝² : x✝.length + x✝¹ = l.length) : List.findFinIdx?.go p l x✝ x✝¹ x✝² = match x✝, x✝¹, x✝² with | [], x, x_1 => none | a :: l_1, i, h => if p a = true then some ⟨i, ⋯⟩ else List.findFinIdx?.go p l l_1 (i + 1) ⋯
• List.findFinIdx?_eq_some_iff 📋 Init.Data.List.Find
  {α : Type u_1} {xs : List α} {p : α → Bool} {i : Fin xs.length} : List.findFinIdx? p xs = some i ↔ p xs[i] = true ∧ ∀ (j : Fin xs.length) (hji : j < i), ¬p xs[j] = true
• List.findFinIdx?_subtype 📋 Init.Data.List.Find
  {α : Type u_1} {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) : List.findFinIdx? f l = Option.map (fun i => Fin.cast ⋯ i) (List.findFinIdx? g l.unattach)
• List.finIdxOf?_eq_some_iff 📋 Init.Data.List.Find
  {α : Type u_1} [BEq α] [LawfulBEq α] {l : List α} {a : α} {i : Fin l.length} : List.finIdxOf? a l = some i ↔ l[i] = a ∧ ∀ j < i, ¬l[j] = a
• List.findFinIdx?_eq_pmap_findIdx? 📋 Init.Data.List.Find
  {α : Type u_1} {xs : List α} {p : α → Bool} : List.findFinIdx? p xs = Option.pmap (fun i m => ⟨i, ⋯⟩) (List.findIdx? p xs) ⋯
• List.ofFn 📋 Init.Data.List.OfFn
  {α : Type u_1} {n : ℕ} (f : Fin n → α) : List α
• List.ofFn_zero 📋 Init.Data.List.OfFn
  {α : Type u_1} (f : Fin 0 → α) : List.ofFn f = []
• List.ofFn_eq_nil_iff 📋 Init.Data.List.OfFn
  {n : ℕ} {α : Type u_1} {f : Fin n → α} : List.ofFn f = [] ↔ n = 0
• List.ofFn.eq_1 📋 Init.Data.List.OfFn
  {α : Type u_1} {n : ℕ} (f : Fin n → α) : List.ofFn f = Fin.foldr n (fun x1 x2 => f x1 :: x2) []
• List.mem_ofFn 📋 Init.Data.List.OfFn
  {α : Type u_1} {n : ℕ} (f : Fin n → α) (a : α) : a ∈ List.ofFn f ↔ ∃ i, f i = a
• List.getElem?_ofFn 📋 Init.Data.List.OfFn
  {n : ℕ} {α : Type u_1} (f : Fin n → α) (i : ℕ) : (List.ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none
• List.head_ofFn 📋 Init.Data.List.OfFn
  {α : Type u_1} {n : ℕ} (f : Fin n → α) (h : List.ofFn f ≠ []) : (List.ofFn f).head h = f ⟨0, ⋯⟩
• List.getLast_ofFn 📋 Init.Data.List.OfFn
  {α : Type u_1} {n : ℕ} (f : Fin n → α) (h : List.ofFn f ≠ []) : (List.ofFn f).getLast h = f ⟨n - 1, ⋯⟩
• List.getElem_ofFn 📋 Init.Data.List.OfFn
  {n : ℕ} {α : Type u_1} (f : Fin n → α) (i : ℕ) (h : i < (List.ofFn f).length) : (List.ofFn f)[i] = f ⟨i, ⋯⟩
• List.ofFn_succ 📋 Init.Data.List.OfFn
  {α : Type u_1} {n : ℕ} (f : Fin (n + 1) → α) : List.ofFn f = f 0 :: List.ofFn fun i => f i.succ
• List.finRange 📋 Init.Data.List.FinRange
  (n : ℕ) : List (Fin n)
• List.finRange.eq_1 📋 Init.Data.List.FinRange
  (n : ℕ) : List.finRange n = List.ofFn fun i => i
• List.finRange_reverse 📋 Init.Data.List.FinRange
  (n : ℕ) : (List.finRange n).reverse = List.map Fin.rev (List.finRange n)
• List.finRange_zero 📋 Init.Data.List.FinRange
  : List.finRange 0 = []
• List.getElem_finRange 📋 Init.Data.List.FinRange
  {n : ℕ} (i : ℕ) (h : i < (List.finRange n).length) : (List.finRange n)[i] = Fin.cast ⋯ ⟨i, h⟩
• List.finRange_succ 📋 Init.Data.List.FinRange
  (n : ℕ) : List.finRange (n + 1) = 0 :: List.map Fin.succ (List.finRange n)
• List.finRange_succ_last 📋 Init.Data.List.FinRange
  (n : ℕ) : List.finRange (n + 1) = List.map Fin.castSucc (List.finRange n) ++ [Fin.last n]
• 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
• List.findFinIdx?_toArray 📋 Init.Data.List.ToArray
  {α : Type u_1} (p : α → Bool) (l : List α) : Array.findFinIdx? p l.toArray = List.findFinIdx? p l
• List.finIdxOf?_toArray 📋 Init.Data.List.ToArray
  {α : Type u_1} [BEq α] (a : α) (l : List α) : l.toArray.finIdxOf? a = List.finIdxOf? a l
• Array.getElem_fin_eq_getElem_toList 📋 Init.Data.Array.Lemmas
  {α : Type u_1} (xs : Array α) (i : Fin xs.size) : xs[i] = xs.toList[i]
• Array.getElem_fin_eq_toList_get 📋 Init.Data.Array.Lemmas
  {α : Type u_1} (xs : Array α) (i : Fin xs.size) : xs[i] = xs.toList[i]
• List.mapFinIdx_eq_ofFn 📋 Init.Data.List.MapIdx
  {α : Type u_1} {β : Type u_2} {as : List α} {f : (i : ℕ) → α → i < as.length → β} : as.mapFinIdx f = List.ofFn fun i => f (↑i) as[i] ⋯
• Array.toList_ofFn 📋 Init.Data.Array.OfFn
  {n : ℕ} {α : Type u_1} (f : Fin n → α) : (Array.ofFn f).toList = List.ofFn f
• Vector.toList_ofFn 📋 Init.Data.Vector.Lemmas
  {n : ℕ} {α : Type u_1} (f : Fin n → α) : (Vector.ofFn f).toList = List.ofFn f
• 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'
• Fin.list 📋 Batteries.Data.Fin.Basic
  (n : ℕ) : List (Fin n)
• List.list_reverse 📋 Batteries.Data.List.FinRange
  (n : ℕ) : (List.finRange n).reverse = List.map Fin.rev (List.finRange n)
• List.list_zero 📋 Batteries.Data.List.FinRange
  : List.finRange 0 = []
• List.getElem_list 📋 Batteries.Data.List.FinRange
  {n : ℕ} (i : ℕ) (h : i < (List.finRange n).length) : (List.finRange n)[i] = Fin.cast ⋯ ⟨i, h⟩
• List.list_succ 📋 Batteries.Data.List.FinRange
  (n : ℕ) : List.finRange (n + 1) = 0 :: List.map Fin.succ (List.finRange n)
• List.list_succ_last 📋 Batteries.Data.List.FinRange
  (n : ℕ) : List.finRange (n + 1) = List.map Fin.castSucc (List.finRange n) ++ [Fin.last n]
• 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)
• Batteries.Linter.UnnecessarySeqFocus.getPath 📋 Batteries.Linter.UnnecessarySeqFocus
  : Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → List ((n : ℕ) × Fin n) → Option Lean.Elab.Info
• 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[i]?.get ⋯
• List.get_eq_getElem? 📋 Mathlib.Data.List.Basic
  {α : Type u} (l : List α) (i : Fin l.length) : l.get i = l[i]?.get ⋯
• List.nodup_iff_injective_get 📋 Mathlib.Data.List.Nodup
  {α : Type u} {l : List α} : l.Nodup ↔ Function.Injective l.get
• List.get_idxOf 📋 Mathlib.Data.List.Nodup
  {α : Type u} [DecidableEq α] {l : List α} (H : l.Nodup) (i : Fin l.length) : List.idxOf (l.get i) l = ↑i
• List.get_indexOf 📋 Mathlib.Data.List.Nodup
  {α : Type u} [DecidableEq α] {l : List α} (H : l.Nodup) (i : Fin l.length) : List.idxOf (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]
• Set.range_list_get 📋 Mathlib.Data.Set.List
  {α : Type u_1} (l : List α) : Set.range l.get = {x | x ∈ l}
• List.cons_get_drop_succ 📋 Mathlib.Data.List.TakeDrop
  {α : Type u} {l : List α} {n : Fin l.length} : l.get n :: List.drop (↑n + 1) l = List.drop (↑n) l
• 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.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_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_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_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_getElem 📋 Mathlib.Data.List.OfFn
  {α : Type u} (l : List α) : (List.ofFn fun i => l[↑i]) = l
• 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_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.get?_ofFn 📋 Mathlib.Data.List.OfFn
  {n : ℕ} {α : Type u_1} (f : Fin n → α) (i : ℕ) : (List.ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none
• List.getLast_ofFn_succ 📋 Mathlib.Data.List.OfFn
  {α : Type u} {n : ℕ} (f : Fin n.succ → α) : (List.ofFn f).getLast ⋯ = f (Fin.last n)
• List.equivSigmaTuple_symm_apply 📋 Mathlib.Data.List.OfFn
  {α : Type u} (f : (n : ℕ) × (Fin n → α)) : List.equivSigmaTuple.symm f = List.ofFn f.snd
• 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.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.mem_finRange 📋 Mathlib.Data.List.FinRange
  {n : ℕ} (a : Fin n) : a ∈ List.finRange n
• List.finRange_eq_nil 📋 Mathlib.Data.List.FinRange
  {n : ℕ} : List.finRange n = [] ↔ n = 0
• 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_map_get 📋 Mathlib.Data.List.FinRange
  {α : Type u} (l : List α) : List.map l.get (List.finRange l.length) = l
• 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_map_getElem 📋 Mathlib.Data.List.FinRange
  {α : Type u} (l : List α) : List.map (fun x => l[↑x]) (List.finRange l.length) = l
• List.finRange_succ_eq_map 📋 Mathlib.Data.List.FinRange
  (n : ℕ) : List.finRange n.succ = 0 :: List.map Fin.succ (List.finRange n)
• List.finRange_eq_pmap_range 📋 Mathlib.Data.List.FinRange
  (n : ℕ) : List.finRange n = List.pmap Fin.mk (List.range 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_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.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.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.idxOf 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.idxOf (↑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.idxOf (↑x) l
• List.Vector.toList_ofFn 📋 Mathlib.Data.Vector.Basic
  {α : Type u_1} {n : ℕ} (f : Fin n → α) : (List.Vector.ofFn f).toList = List.ofFn f
• List.Vector.toList_set 📋 Mathlib.Data.Vector.Basic
  {α : Type u_1} {n : ℕ} (v : List.Vector α n) (i : Fin n) (a : α) : (v.set i a).toList = v.toList.set (↑i) a
• List.Vector.set.eq_1 📋 Mathlib.Data.Vector.Basic
  {α : Type u_1} {n : ℕ} (v : List.Vector α n) (i : Fin n) (a : α) : v.set i a = ⟨(↑v).set (↑i) a, ⋯⟩
• List.Vector.eraseIdx_val 📋 Mathlib.Data.Vector.Basic
  {α : Type u_1} {n : ℕ} {i : Fin n} {v : List.Vector α n} : ↑(List.Vector.eraseIdx i v) = (↑v).eraseIdx ↑i
• List.Vector.eraseNth_val 📋 Mathlib.Data.Vector.Basic
  {α : Type u_1} {n : ℕ} {i : Fin n} {v : List.Vector α n} : ↑(List.Vector.eraseIdx i v) = (↑v).eraseIdx ↑i
• List.Vector.insertIdx_val 📋 Mathlib.Data.Vector.Basic
  {α : Type u_1} {n : ℕ} {a : α} {i : Fin (n + 1)} {v : List.Vector α n} : ↑(List.Vector.insertIdx a i v) = List.insertIdx (↑i) a ↑v
• List.Vector.insertNth_val 📋 Mathlib.Data.Vector.Basic
  {α : Type u_1} {n : ℕ} {a : α} {i : Fin (n + 1)} {v : List.Vector α n} : ↑(List.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, l[↑i] = l.prod
• Fin.sum_univ_get 📋 Mathlib.Algebra.BigOperators.Fin
  {α : Type u_1} [AddCommMonoid α] (l : List α) : ∑ i, l[↑i] = l.sum
• Fin.prod_univ_get' 📋 Mathlib.Algebra.BigOperators.Fin
  {α : Type u_1} {β : Type u_2} [CommMonoid β] (l : List α) (f : α → β) : ∏ i, 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, 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, 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, (-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.listMap_orderEmbOfFin_finRange 📋 Mathlib.Data.Finset.Sort
  {α : Type u_1} [LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k) : List.map (⇑(s.orderEmbOfFin h)) (List.finRange k) = Finset.sort (fun x1 x2 => x1 ≤ x2) s
• 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]
• 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₂
• 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
• 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]
• 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
• 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, 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.flatMap (fun ni => List.map (fun x => Fin.cons ni.1 x) (List.Nat.antidiagonalTuple k ni.2)) (List.Nat.antidiagonal x✝)
• Nat.finMulAntidiag_existsUnique_prime_dvd 📋 Mathlib.Algebra.Order.Antidiag.Nat
  {d n p : ℕ} (hn : Squarefree n) (hp : p ∈ n.primeFactorsList) (f : Fin d → ℕ) (hf : f ∈ d.finMulAntidiag n) : ∃! i, p ∣ f i
• Nat.finMulAntidiag_exists_unique_prime_dvd 📋 Mathlib.Algebra.Order.Antidiag.Nat
  {d n p : ℕ} (hn : Squarefree n) (hp : p ∈ n.primeFactorsList) (f : Fin d → ℕ) (hf : f ∈ d.finMulAntidiag n) : ∃! i, p ∣ f i
• List.toFinsupp_apply_fin 📋 Mathlib.Data.List.ToFinsupp
  {M : Type u_1} [Zero M] (l : List M) [DecidablePred fun x => l.getD x 0 ≠ 0] (n : Fin l.length) : l.toFinsupp ↑n = l[n]
• 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, (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, (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, (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, (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, (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, (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, (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 𝕜 𝔸] {l : List ι} {x : { i // i ∈ l } → 𝔸} : HasFDerivAt (fun x => (List.map x l.attach).prod) (∑ i, (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 𝕜 𝔸] {l : List ι} {x : { i // i ∈ l } → 𝔸} : HasStrictFDerivAt (fun x => (List.map x l.attach).prod) (∑ i, (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

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 d56dbe9 serving mathlib revision 3d845f2