Loogle!

Result

Found 266 declarations 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.ofFn 📋 Init.Data.List.OfFn
  {α : Type u_1} {n : ℕ} (f : Fin n → α) : List α
• List.ofFnM 📋 Init.Data.List.OfFn
  {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [Monad m] (f : Fin n → m α) : m (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.idRun_ofFnM 📋 Init.Data.List.OfFn
  {n : ℕ} {α : Type u_1} {f : Fin n → Id α} : (List.ofFnM f).run = List.ofFn fun i => (f i).run
• List.mem_ofFn 📋 Init.Data.List.OfFn
  {α : Type u_1} {n : ℕ} {f : Fin n → α} {a : α} : a ∈ List.ofFn f ↔ ∃ i, f i = a
• Fin.foldr_cons_eq_append 📋 Init.Data.List.OfFn
  {n : ℕ} {α : Type u_1} {f : Fin n → α} {xs : List α} : Fin.foldr n (fun i xs => f i :: xs) xs = List.ofFn f ++ xs
• List.ofFnM_zero 📋 Init.Data.List.OfFn
  {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [LawfulMonad m] {f : Fin 0 → m α} : List.ofFnM f = pure []
• Fin.foldl_cons_eq_append 📋 Init.Data.List.OfFn
  {n : ℕ} {α : Type u_1} {f : Fin n → α} {xs : List α} : Fin.foldl n (fun xs i => f i :: xs) xs = (List.ofFn f).reverse ++ xs
• List.ofFnM_pure 📋 Init.Data.List.OfFn
  {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [LawfulMonad m] {n : ℕ} {f : Fin n → α} : (List.ofFnM fun i => pure (f i)) = pure (List.ofFn f)
• List.ofFnM_pure_comp 📋 Init.Data.List.OfFn
  {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [LawfulMonad m] {n : ℕ} {f : Fin n → α} : List.ofFnM (pure ∘ f) = pure (List.ofFn f)
• List.getElem_ofFn 📋 Init.Data.List.OfFn
  {n : ℕ} {α : Type u_1} {i : ℕ} {f : Fin n → α} (h : i < (List.ofFn f).length) : (List.ofFn f)[i] = f ⟨i, ⋯⟩
• List.getElem?_ofFn 📋 Init.Data.List.OfFn
  {n : ℕ} {α : Type u_1} {i : ℕ} {f : Fin n → α} : (List.ofFn f)[i]? = if h : i < n then some (f ⟨i, h⟩) else none
• List.ofFn_succ_last 📋 Init.Data.List.OfFn
  {α : Type u_1} {n : ℕ} {f : Fin (n + 1) → α} : List.ofFn f = (List.ofFn fun i => f i.castSucc) ++ [f (Fin.last n)]
• List.ofFn_add 📋 Init.Data.List.OfFn
  {α : Type u_1} {n m : ℕ} {f : Fin (n + m) → α} : List.ofFn f = (List.ofFn fun i => f (Fin.castLE ⋯ i)) ++ List.ofFn fun i => f (Fin.natAdd n i)
• 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.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.ofFnM_succ_last 📋 Init.Data.List.OfFn
  {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} : List.ofFnM f = do let as ← List.ofFnM fun i => f i.castSucc let a ← f (Fin.last n) pure (as ++ [a])
• List.ofFnM_add 📋 Init.Data.List.OfFn
  {k : ℕ} {α : Type u_1} {n : ℕ} {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] {f : Fin (n + k) → m α} : List.ofFnM f = do let as ← List.ofFnM fun i => f (Fin.castLE ⋯ i) let bs ← List.ofFnM fun i => f (Fin.natAdd n i) pure (as ++ bs)
• List.isSome_findFinIdx? 📋 Init.Data.List.Find
  {α : Type u_1} {l : List α} {p : α → Bool} : (List.findFinIdx? p l).isSome = l.any p
• List.finIdxOf?.eq_1 📋 Init.Data.List.Find
  {α : Type u} [BEq α] (a : α) : List.finIdxOf? a = List.findFinIdx? fun x => x == a
• List.isSome_finIdxOf? 📋 Init.Data.List.Find
  {α : Type u_1} [BEq α] [PartialEquivBEq α] {l : List α} {a : α} : (List.finIdxOf? a l).isSome = l.contains a
• List.isNone_finIdxOf? 📋 Init.Data.List.Find
  {α : Type u_1} [BEq α] [PartialEquivBEq α] {l : List α} {a : α} : (List.finIdxOf? a l).isNone = !l.contains 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.isNone_findFinIdx? 📋 Init.Data.List.Find
  {α : Type u_1} {l : List α} {p : α → Bool} : (List.findFinIdx? p l).isNone = l.all fun x => decide ¬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?_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.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?.go.congr_simp 📋 Init.Data.List.Find
  {α : Type u} (p p✝ : α → Bool) (e_p : p = p✝) (l l' l'✝ : List α) (e_l' : l' = l'✝) (i i✝ : ℕ) (e_i : i = i✝) (h : l'.length + i = l.length) : List.findFinIdx?.go p l l' i h = List.findFinIdx?.go p✝ l l'✝ i✝ ⋯
• 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?_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?_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_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?.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?_append 📋 Init.Data.List.Find
  {α : Type u_1} {xs ys : List α} {p : α → Bool} : List.findFinIdx? p (xs ++ ys) = (Option.map (Fin.castLE ⋯) (List.findFinIdx? p xs)).or (Option.map (Fin.cast ⋯) (Option.map (Fin.natAdd xs.length) (List.findFinIdx? p ys)))
• 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.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]
• List.finRange 📋 Init.Data.List.FinRange
  (n : ℕ) : List (Fin n)
• 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.ofFnM_succ 📋 Init.Data.List.FinRange
  {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α} : List.ofFnM f = do let a ← f 0 let as ← List.ofFnM fun i => f i.succ pure (a :: as)
• List.finRange_succ_last 📋 Init.Data.List.FinRange
  {n : ℕ} : List.finRange (n + 1) = List.map Fin.castSucc (List.finRange n) ++ [Fin.last n]
• Array.toList_ofFn 📋 Init.Data.Array.OfFn
  {n : ℕ} {α : Type u_1} {f : Fin n → α} : (Array.ofFn f).toList = List.ofFn f
• Array.toList_ofFnM 📋 Init.Data.Array.OfFn
  {m : Type u_1 → Type u_2} {n : ℕ} {α : Type u_1} [Monad m] [LawfulMonad m] {f : Fin n → m α} : Array.toList <$> Array.ofFnM f = List.ofFnM f
• 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] ⋯
• 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
• Vector.toList_ofFn 📋 Init.Data.Vector.Lemmas
  {n : ℕ} {α : Type u_1} {f : Fin n → α} : (Vector.ofFn f).toList = List.ofFn f
• Vector.toList_ofFnM 📋 Init.Data.Vector.OfFn
  {m : Type u_1 → Type u_2} {n : ℕ} {α : Type u_1} [Monad m] [LawfulMonad m] {f : Fin n → m α} : Vector.toList <$> Vector.ofFnM f = List.ofFnM 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'
• Batteries.Linter.UnnecessarySeqFocus.getPath 📋 Batteries.Linter.UnnecessarySeqFocus
  : Lean.Elab.Info → Lean.PersistentArray Lean.Elab.InfoTree → List ((n : ℕ) × Fin n) → Option Lean.Elab.Info
• 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.finRange.eq_1 📋 Batteries.Data.Char.Basic
  (n : ℕ) : List.finRange n = List.ofFn fun i => i
• List.mem_finRange 📋 Batteries.Data.Char.Basic
  {n : ℕ} (a : Fin n) : a ∈ List.finRange n
• 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_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_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_bijective_iff 📋 Mathlib.Data.List.Nodup
  {α : Type u} {l : List α} [DecidableEq α] : Function.Bijective l.get ↔ ∀ (a : α), List.count a l = 1
• 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.getElem_bijective_iff 📋 Mathlib.Data.List.Nodup
  {α : Type u} {l : List α} [DecidableEq α] : (Function.Bijective fun n => l[n]) ↔ ∀ (a : α), List.count a l = 1
• Set.range_list_get 📋 Mathlib.Data.Set.List
  {α : Type u_1} (l : List α) : Set.range l.get = {x | x ∈ 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.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.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_comp' 📋 Mathlib.Data.List.OfFn
  {α : Type u} {β : Type u_1} {n : ℕ} (f : Fin n → α) (g : α → β) : (List.ofFn fun i => g (f i)) = List.map g (List.ofFn f)
• 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.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.ofFn_getElem 📋 Mathlib.Data.List.OfFn
  {α : Type u} (l : List α) : (List.ofFn fun i => l[↑i]) = l
• 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_apply_fst 📋 Mathlib.Data.List.OfFn
  {α : Type u} (l : List α) : (List.equivSigmaTuple l).fst = l.length
• 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_apply_snd 📋 Mathlib.Data.List.OfFn
  {α : Type u} (l : List α) (a✝ : Fin l.length) : (List.equivSigmaTuple l).snd a✝ = l.get a✝
• List.equivSigmaTuple_symm_apply 📋 Mathlib.Data.List.OfFn
  {α : Type u} (f : (n : ℕ) × (Fin n → α)) : List.equivSigmaTuple.symm f = List.ofFn f.snd
• 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.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.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.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.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.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.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.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.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.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) = (↑v).insertIdx (↑i) a
• Fin.prod_univ_get 📋 Mathlib.Algebra.BigOperators.Fin
  {M : Type u_2} [CommMonoid M] (l : List M) : ∏ i, l[↑i] = l.prod
• Fin.prod_univ_getElem 📋 Mathlib.Algebra.BigOperators.Fin
  {M : Type u_2} [CommMonoid M] (l : List M) : ∏ i, l[↑i] = l.prod
• Fin.sum_univ_get 📋 Mathlib.Algebra.BigOperators.Fin
  {M : Type u_2} [AddCommMonoid M] (l : List M) : ∑ i, l[↑i] = l.sum
• Fin.sum_univ_getElem 📋 Mathlib.Algebra.BigOperators.Fin
  {M : Type u_2} [AddCommMonoid M] (l : List M) : ∑ i, l[↑i] = l.sum
• Fin.prod_univ_fun_getElem 📋 Mathlib.Algebra.BigOperators.Fin
  {ι : Type u_1} {M : Type u_2} [CommMonoid M] (l : List ι) (f : ι → M) : ∏ i, f l[↑i] = (List.map f l).prod
• Fin.prod_univ_get' 📋 Mathlib.Algebra.BigOperators.Fin
  {ι : Type u_1} {M : Type u_2} [CommMonoid M] (l : List ι) (f : ι → M) : ∏ i, f l[↑i] = (List.map f l).prod
• Fin.sum_univ_fun_getElem 📋 Mathlib.Algebra.BigOperators.Fin
  {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (l : List ι) (f : ι → M) : ∑ i, f l[↑i] = (List.map f l).sum
• Fin.sum_univ_get' 📋 Mathlib.Algebra.BigOperators.Fin
  {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (l : List ι) (f : ι → M) : ∑ i, f l[↑i] = (List.map f l).sum
• List.alternatingProd_eq_finset_prod 📋 Mathlib.Algebra.BigOperators.Fin
  {G : Type u_3} [DivisionCommMonoid G] (L : List G) : L.alternatingProd = ∏ i, L[i] ^ (-1) ^ ↑i
• List.alternatingSum_eq_finset_sum 📋 Mathlib.Algebra.BigOperators.Fin
  {G : Type u_3} [SubtractionCommMonoid 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.fromListIsChain_toFun 📋 Mathlib.Order.RelSeries
  {α : Type u_1} {r : SetRel α α} (x : List α) (x_ne_nil : x ≠ []) (hx : List.IsChain (fun x1 x2 => (x1, x2) ∈ r) x) (i : Fin (x.length - 1 + 1)) : (RelSeries.fromListIsChain x x_ne_nil hx).toFun i = x[Fin.cast ⋯ i]
• RelSeries.toList_getElem_eq_apply 📋 Mathlib.Order.RelSeries
  {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin (p.length + 1)) : p.toList[↑i] = p.toFun i
• RelSeries.getLast_toList 📋 Mathlib.Order.RelSeries
  {α : Type u_1} {r : SetRel α α} (p : RelSeries r) : p.toList.getLast ⋯ = p.last
• 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
• 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]
• SimplexCategoryGenRel.IsAdmissible.head 📋 Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
  {m : ℕ} (a : ℕ) (L : List ℕ) (hl : SimplexCategoryGenRel.IsAdmissible m (a :: L)) : Fin (m + 1)
• SimplexCategoryGenRel.IsAdmissible.getElemAsFin 📋 Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
  {m : ℕ} {L : List ℕ} (hl : SimplexCategoryGenRel.IsAdmissible m L) (k : ℕ) (hK : k < L.length) : Fin (m + k + 1)
• SimplexCategoryGenRel.IsAdmissible.head.congr_simp 📋 Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
  {m : ℕ} (a a✝ : ℕ) (e_a : a = a✝) (L L✝ : List ℕ) (e_L : L = L✝) (hl : SimplexCategoryGenRel.IsAdmissible m (a :: L)) : SimplexCategoryGenRel.IsAdmissible.head a L hl = SimplexCategoryGenRel.IsAdmissible.head a✝ L✝ ⋯
• SimplexCategoryGenRel.simplicialEvalσ_of_isAdmissible 📋 Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
  (L : List ℕ) (m₁ m₂ : ℕ) (hL : SimplexCategoryGenRel.IsAdmissible m₂ L) (hk : m₂ + L.length = m₁) (j : ℕ) (hj : j < m₁ + 1) : ↑((SimplexCategory.Hom.toOrderHom (SimplexCategoryGenRel.toSimplexCategory.map (SimplexCategoryGenRel.standardσ L hk))) ⟨j, hj⟩) = SimplexCategoryGenRel.simplicialEvalσ L j

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 ee8c038 serving mathlib revision 3aa3aca