Loogle!

Result

Found 5048 declarations mentioning Prod.fst. Of these, 475 have a name containing "_fst". Of these, only the first 200 are shown.

• Prod.map_fst 📋 Init.Core
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α × γ) : (Prod.map f g x).1 = f x.1
• Lean.Omega.Int.ofNat_fst_mk 📋 Init.Omega.Int
  {β : Type u_1} {x : ℕ} {y : β} : ↑(x, y).1 = ↑x
• List.unzip_fst 📋 Init.Data.List.Zip
  {α✝ : Type u_1} {β✝ : Type u_2} {l : List (α✝ × β✝)} : l.unzip.1 = List.map Prod.fst l
• List.map_fst_zip 📋 Init.Data.List.Zip
  {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} : l₁.length ≤ l₂.length → List.map Prod.fst (l₁.zip l₂) = l₁
• List.tail_zip_fst 📋 Init.Data.List.Zip
  {α : Type u_1} {β : Type u_2} {l : List (α × β)} : l.unzip.1.tail = l.tail.unzip.1
• List.zipIdx_map_fst 📋 Init.Data.List.Range
  {α : Type u_1} (i : ℕ) (l : List α) : List.map Prod.fst (l.zipIdx i) = l
• Array.toList_fst_unzip 📋 Init.Data.Array.Lemmas
  {α : Type u_1} {β : Type u_2} {xs : Array (α × β)} : xs.unzip.1.toList = xs.toList.unzip.1
• Array.map_fst_zip 📋 Init.Data.Array.Zip
  {α : Type u_1} {β : Type u_2} {as : Array α} {bs : Array β} (h : as.size ≤ bs.size) : Array.map Prod.fst (as.zip bs) = as
• Array.zipIdx_map_fst 📋 Init.Data.Array.Range
  {α : Type u_1} (i : ℕ) (xs : Array α) : Array.map Prod.fst (xs.zipIdx i) = xs
• List.MergeSort.Internal.splitInTwo_fst_pairwise 📋 Init.Data.List.Sort.Lemmas
  {α : Type u_1} {n : ℕ} {le : α → α → Prop} (l : { l // l.length = n }) (h : List.Pairwise le ↑l) : List.Pairwise le ↑(List.MergeSort.Internal.splitInTwo l).1
• List.MergeSort.Internal.splitInTwo_fst_sorted 📋 Init.Data.List.Sort.Lemmas
  {α : Type u_1} {n : ℕ} {le : α → α → Prop} (l : { l // l.length = n }) (h : List.Pairwise le ↑l) : List.Pairwise le ↑(List.MergeSort.Internal.splitInTwo l).1
• List.MergeSort.Internal.splitInTwo_fst 📋 Init.Data.List.Sort.Lemmas
  {α : Type u_1} {n : ℕ} (l : { l // l.length = n }) : (List.MergeSort.Internal.splitInTwo l).1 = ⟨List.take ((n + 1) / 2) ↑l, ⋯⟩
• List.MergeSort.Internal.splitInTwo_fst_append_splitInTwo_snd 📋 Init.Data.List.Sort.Lemmas
  {α : Type u_1} {n : ℕ} (l : { l // l.length = n }) : ↑(List.MergeSort.Internal.splitInTwo l).1 ++ ↑(List.MergeSort.Internal.splitInTwo l).2 = ↑l
• List.MergeSort.Internal.splitInTwo_fst_le_splitInTwo_snd 📋 Init.Data.List.Sort.Lemmas
  {α : Type u_1} {n : ℕ} {le : α → α → Prop} {l : { l // l.length = n }} (h : List.Pairwise le ↑l) (a b : α) : a ∈ ↑(List.MergeSort.Internal.splitInTwo l).1 → b ∈ ↑(List.MergeSort.Internal.splitInTwo l).2 → le a b
• List.MergeSort.Internal.splitInTwo_cons_cons_zipIdx_fst 📋 Init.Data.List.Sort.Lemmas
  {α : Type u_1} {a b : α} (i : ℕ) (l : List α) : ↑(List.MergeSort.Internal.splitInTwo ⟨(a, i) :: (b, i + 1) :: l.zipIdx (i + 2), ⋯⟩).1 = (↑(List.MergeSort.Internal.splitInTwo ⟨a :: b :: l, ⋯⟩).1).zipIdx i
• List.MergeSort.Internal.splitRevInTwo'_fst 📋 Init.Data.List.Sort.Impl
  {α : Type u_1} {n : ℕ} (l : { l // l.length = n }) : (List.MergeSort.Internal.splitRevInTwo' l).1 = ⟨↑(List.MergeSort.Internal.splitInTwo ⟨(↑l).reverse, ⋯⟩).2, ⋯⟩
• List.MergeSort.Internal.splitRevInTwo_fst 📋 Init.Data.List.Sort.Impl
  {α : Type u_1} {n : ℕ} (l : { l // l.length = n }) : (List.MergeSort.Internal.splitRevInTwo l).1 = ⟨(↑(List.MergeSort.Internal.splitInTwo l).1).reverse, ⋯⟩
• Vector.map_fst_zip 📋 Init.Data.Vector.Zip
  {α : Type u_1} {n : ℕ} {β : Type u_2} (as : Vector α n) {bs : Vector β n} : Vector.map Prod.fst (as.zip bs) = as
• Vector.unzip_fst 📋 Init.Data.Vector.Zip
  {α✝ : Type u_1} {β✝ : Type u_2} {n✝ : ℕ} {xs : Vector (α✝ × β✝) n✝} : xs.unzip.1 = Vector.map Prod.fst xs
• Vector.zipIdx_map_fst 📋 Init.Data.Vector.Range
  {α : Type u_1} {n : ℕ} (i : ℕ) (xs : Vector α n) : Vector.map Prod.fst (xs.zipIdx i) = xs
• Std.DHashMap.Internal.Raw.containsThenInsertIfNew_fst_eq 📋 Std.Data.DHashMap.Internal.Raw
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α β} (h : m.WF) {a : α} {b : β a} : (m.containsThenInsertIfNew a b).1 = (Std.DHashMap.Internal.Raw₀.containsThenInsertIfNew ⟨m, ⋯⟩ a b).1
• Std.DHashMap.Internal.Raw.containsThenInsert_fst_eq 📋 Std.Data.DHashMap.Internal.Raw
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α β} (h : m.WF) {a : α} {b : β a} : (m.containsThenInsert a b).1 = (Std.DHashMap.Internal.Raw₀.containsThenInsert ⟨m, ⋯⟩ a b).1
• Std.DHashMap.Internal.Raw.Const.getThenInsertIfNew?_fst_eq 📋 Std.Data.DHashMap.Internal.Raw
  {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.DHashMap.Raw α fun x => β} (h : m.WF) {a : α} {b : β} : (Std.DHashMap.Raw.Const.getThenInsertIfNew? m a b).1 = (Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? ⟨m, ⋯⟩ a b).1
• Std.DHashMap.Internal.Raw.getThenInsertIfNew?_fst_eq 📋 Std.Data.DHashMap.Internal.Raw
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {m : Std.DHashMap.Raw α β} (h : m.WF) {a : α} {b : β a} : (m.getThenInsertIfNew? a b).1 = (Std.DHashMap.Internal.Raw₀.getThenInsertIfNew? ⟨m, ⋯⟩ a b).1
• Std.Internal.List.map_fst_map_toProd_eq_keys 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} {l : List ((_ : α) × β)} : List.map Prod.fst (List.map (fun x => (x.fst, x.snd)) l) = Std.Internal.List.keys l
• Std.Internal.List.pairwise_fst_eq_false_map_toProd 📋 Std.Data.Internal.List.Associative
  {α : Type u} [BEq α] {β : Type v} {l : List ((_ : α) × β)} (h : Std.Internal.List.DistinctKeys l) : List.Pairwise (fun a b => (a.1 == b.1) = false) (List.map (fun x => (x.fst, x.snd)) l)
• Std.DHashMap.Internal.Raw₀.containsThenInsertIfNew_fst 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] {k : α} {v : β k} : (m.containsThenInsertIfNew k v).1 = m.contains k
• Std.DHashMap.Internal.Raw₀.containsThenInsert_fst 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] {k : α} {v : β k} : (m.containsThenInsert k v).1 = m.contains k
• Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew?_fst 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) {k : α} {v : β} : (Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? m k v).1 = Std.DHashMap.Internal.Raw₀.Const.get? m k
• Std.DHashMap.Internal.Raw₀.getThenInsertIfNew?_fst 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] [LawfulBEq α] {k : α} {v : β k} : (m.getThenInsertIfNew? k v).1 = m.get? k
• Std.DHashMap.Internal.Raw₀.Const.map_fst_toArray_eq_keysArray 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] : Array.map Prod.fst (Std.DHashMap.Raw.Const.toArray ↑m) = (↑m).keysArray
• Std.DHashMap.Internal.Raw₀.Const.map_fst_toList_eq_keys 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] : List.map Prod.fst (Std.DHashMap.Raw.Const.toList ↑m) = (↑m).keys
• Std.DHashMap.containsThenInsertIfNew_fst 📋 Std.Data.DHashMap.Lemmas
  {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} {k : α} {v : β k} : (m.containsThenInsertIfNew k v).1 = m.contains k
• Std.DHashMap.containsThenInsert_fst 📋 Std.Data.DHashMap.Lemmas
  {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} {k : α} {v : β k} : (m.containsThenInsert k v).1 = m.contains k
• Std.DHashMap.Const.getThenInsertIfNew?_fst 📋 Std.Data.DHashMap.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} {k : α} {v : β} : (Std.DHashMap.Const.getThenInsertIfNew? m k v).1 = Std.DHashMap.Const.get? m k
• Std.DHashMap.Const.map_fst_toArray_eq_keysArray 📋 Std.Data.DHashMap.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] : Array.map Prod.fst (Std.DHashMap.Const.toArray m) = m.keysArray
• Std.DHashMap.Const.map_fst_toList_eq_keys 📋 Std.Data.DHashMap.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] : List.map Prod.fst (Std.DHashMap.Const.toList m) = m.keys
• Std.DHashMap.getThenInsertIfNew?_fst 📋 Std.Data.DHashMap.Lemmas
  {α : Type u} {β : α → Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.DHashMap α β} [LawfulBEq α] {k : α} {v : β k} : (m.getThenInsertIfNew? k v).1 = m.get? k
• Std.DHashMap.Raw.containsThenInsertIfNew_fst 📋 Std.Data.DHashMap.RawLemmas
  {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [BEq α] [Hashable α] (h : m.WF) {k : α} {v : β k} : (m.containsThenInsertIfNew k v).1 = m.contains k
• Std.DHashMap.Raw.containsThenInsert_fst 📋 Std.Data.DHashMap.RawLemmas
  {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [BEq α] [Hashable α] (h : m.WF) {k : α} {v : β k} : (m.containsThenInsert k v).1 = m.contains k
• Std.DHashMap.Raw.Const.getThenInsertIfNew?_fst 📋 Std.Data.DHashMap.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} (h : m.WF) {k : α} {v : β} : (Std.DHashMap.Raw.Const.getThenInsertIfNew? m k v).1 = Std.DHashMap.Raw.Const.get? m k
• Std.DHashMap.Raw.Const.map_fst_toArray_eq_keysArray 📋 Std.Data.DHashMap.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) : Array.map Prod.fst (Std.DHashMap.Raw.Const.toArray m) = m.keysArray
• Std.DHashMap.Raw.Const.map_fst_toList_eq_keys 📋 Std.Data.DHashMap.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α] [LawfulHashable α] (h : m.WF) : List.map Prod.fst (Std.DHashMap.Raw.Const.toList m) = m.keys
• Std.DHashMap.Raw.getThenInsertIfNew?_fst 📋 Std.Data.DHashMap.RawLemmas
  {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [BEq α] [Hashable α] [LawfulBEq α] (h : m.WF) {k : α} {v : β k} : (m.getThenInsertIfNew? k v).1 = m.get? k
• Std.HashMap.containsThenInsertIfNew_fst 📋 Std.Data.HashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} {k : α} {v : β} : (m.containsThenInsertIfNew k v).1 = m.contains k
• Std.HashMap.containsThenInsert_fst 📋 Std.Data.HashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} {k : α} {v : β} : (m.containsThenInsert k v).1 = m.contains k
• Std.HashMap.map_fst_toArray_eq_keysArray 📋 Std.Data.HashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] : Array.map Prod.fst m.toArray = m.keysArray
• Std.HashMap.map_fst_toList_eq_keys 📋 Std.Data.HashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] : List.map Prod.fst m.toList = m.keys
• Std.HashMap.getThenInsertIfNew?_fst 📋 Std.Data.HashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashMap α β} {k : α} {v : β} : (m.getThenInsertIfNew? k v).1 = m[k]?
• Std.HashMap.Raw.containsThenInsertIfNew_fst 📋 Std.Data.HashMap.RawLemmas
  {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [BEq α] [Hashable α] (h : m.WF) {k : α} {v : β} : (m.containsThenInsertIfNew k v).1 = m.contains k
• Std.HashMap.Raw.containsThenInsert_fst 📋 Std.Data.HashMap.RawLemmas
  {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [BEq α] [Hashable α] (h : m.WF) {k : α} {v : β} : (m.containsThenInsert k v).1 = m.contains k
• Std.HashMap.Raw.map_fst_toArray_eq_keysArray 📋 Std.Data.HashMap.RawLemmas
  {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) : Array.map Prod.fst m.toArray = m.keysArray
• Std.HashMap.Raw.map_fst_toList_eq_keys 📋 Std.Data.HashMap.RawLemmas
  {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (h : m.WF) : List.map Prod.fst m.toList = m.keys
• Std.HashMap.Raw.getThenInsertIfNew?_fst 📋 Std.Data.HashMap.RawLemmas
  {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [BEq α] [Hashable α] (h : m.WF) {k : α} {v : β} : (m.getThenInsertIfNew? k v).1 = m[k]?
• Std.HashSet.containsThenInsert_fst 📋 Std.Data.HashSet.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.HashSet α} {k : α} : (m.containsThenInsert k).1 = m.contains k
• Std.HashSet.Raw.containsThenInsert_fst 📋 Std.Data.HashSet.RawLemmas
  {α : Type u} {m : Std.HashSet.Raw α} [BEq α] [Hashable α] (h : m.WF) {k : α} : (m.containsThenInsert k).1 = m.contains k
• Std.DTreeMap.Internal.Impl.containsThenInsertIfNew!_fst_eq_containsₘ 📋 Std.Data.DTreeMap.Internal.Model
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α β) (a : α) (b : β a) : (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew! a b t).1 = t.containsₘ a
• Std.DTreeMap.Internal.Impl.containsThenInsertIfNew_fst_eq_containsₘ 📋 Std.Data.DTreeMap.Internal.Model
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α β) (htb : t.Balanced) (a : α) (b : β a) : (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew a b t htb).1 = t.containsₘ a
• Std.DTreeMap.Internal.Impl.containsThenInsert!_fst_eq_containsThenInsert_fst 📋 Std.Data.DTreeMap.Internal.Model
  {α : Type u} {β : α → Type v} [Ord α] (t : Std.DTreeMap.Internal.Impl α β) (htb : t.Balanced) (a : α) (b : β a) : (Std.DTreeMap.Internal.Impl.containsThenInsert! a b t).1 = (Std.DTreeMap.Internal.Impl.containsThenInsert a b t htb).1
• Std.DTreeMap.Internal.Impl.containsThenInsertIfNew!_fst_eq_containsThenInsertIfNew_fst 📋 Std.Data.DTreeMap.Internal.Model
  {α : Type u} {β : α → Type v} [Ord α] (t : Std.DTreeMap.Internal.Impl α β) (htb : t.Balanced) (a : α) (b : β a) : (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew! a b t).1 = (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew a b t htb).1
• Std.DTreeMap.Internal.Impl.containsThenInsert_fst_eq_containsₘ 📋 Std.Data.DTreeMap.Internal.WF.Lemmas
  {α : Type u} {β : α → Type v} [Ord α] [Std.TransOrd α] [BEq α] [Std.LawfulBEqOrd α] (t : Std.DTreeMap.Internal.Impl α β) (htb : t.Balanced) (ho : t.Ordered) (a : α) (b : β a) : (Std.DTreeMap.Internal.Impl.containsThenInsert a b t htb).1 = t.containsₘ a
• Std.DTreeMap.Internal.Impl.Const.map_fst_toList_eq_keys 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} : List.map Prod.fst (Std.DTreeMap.Internal.Impl.Const.toList t) = t.keys
• Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?!_fst 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] {k : α} {v : β} : (Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?! t k v).1 = Std.DTreeMap.Internal.Impl.Const.get? t k
• Std.DTreeMap.Internal.Impl.containsThenInsert!_fst 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF) {k : α} {v : β k} : (Std.DTreeMap.Internal.Impl.containsThenInsert! k v t).1 = Std.DTreeMap.Internal.Impl.contains k t
• Std.DTreeMap.Internal.Impl.containsThenInsertIfNew!_fst 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF) {k : α} {v : β k} : (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew! k v t).1 = Std.DTreeMap.Internal.Impl.contains k t
• Std.DTreeMap.Internal.Impl.getThenInsertIfNew?!_fst 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [Std.LawfulEqOrd α] {k : α} {v : β k} : (t.getThenInsertIfNew?! k v).1 = t.get? k
• Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?_fst 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF) {k : α} {v : β} : (Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew? t k v ⋯).1 = Std.DTreeMap.Internal.Impl.Const.get? t k
• Std.DTreeMap.Internal.Impl.getThenInsertIfNew?_fst 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [Std.LawfulEqOrd α] (h : t.WF) {k : α} {v : β k} : (t.getThenInsertIfNew? k v ⋯).1 = t.get? k
• Std.DTreeMap.Internal.Impl.containsThenInsertIfNew_fst 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF) {k : α} {v : β k} : (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew k v t ⋯).1 = Std.DTreeMap.Internal.Impl.contains k t
• Std.DTreeMap.Internal.Impl.containsThenInsert_fst 📋 Std.Data.DTreeMap.Internal.Lemmas
  {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF) {k : α} {v : β k} : (Std.DTreeMap.Internal.Impl.containsThenInsert k v t ⋯).1 = Std.DTreeMap.Internal.Impl.contains k t
• Std.DTreeMap.Const.map_fst_toList_eq_keys 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} : List.map Prod.fst (Std.DTreeMap.Const.toList t) = t.keys
• Std.DTreeMap.containsThenInsertIfNew_fst 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β k} : (t.containsThenInsertIfNew k v).1 = t.contains k
• Std.DTreeMap.containsThenInsert_fst 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β k} : (t.containsThenInsert k v).1 = t.contains k
• Std.DTreeMap.Const.getThenInsertIfNew?_fst 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α} {v : β} : (Std.DTreeMap.Const.getThenInsertIfNew? t k v).1 = Std.DTreeMap.Const.get? t k
• Std.DTreeMap.getThenInsertIfNew?_fst 📋 Std.Data.DTreeMap.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {k : α} {v : β k} : (t.getThenInsertIfNew? k v).1 = t.get? k
• Std.DTreeMap.Raw.Const.map_fst_toList_eq_keys 📋 Std.Data.DTreeMap.Raw.Lemmas
  {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} : List.map Prod.fst (Std.DTreeMap.Raw.Const.toList t) = t.keys
• Std.DTreeMap.Raw.containsThenInsertIfNew_fst 📋 Std.Data.DTreeMap.Raw.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] (h : t.WF) {k : α} {v : β k} : (t.containsThenInsertIfNew k v).1 = t.contains k
• Std.DTreeMap.Raw.containsThenInsert_fst 📋 Std.Data.DTreeMap.Raw.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] (h : t.WF) {k : α} {v : β k} : (t.containsThenInsert k v).1 = t.contains k
• Std.DTreeMap.Raw.Const.getThenInsertIfNew?_fst 📋 Std.Data.DTreeMap.Raw.Lemmas
  {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp] : t.WF → ∀ {k : α} {v : β}, (Std.DTreeMap.Raw.Const.getThenInsertIfNew? t k v).1 = Std.DTreeMap.Raw.Const.get? t k
• Std.DTreeMap.Raw.getThenInsertIfNew?_fst 📋 Std.Data.DTreeMap.Raw.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] : t.WF → ∀ {k : α} {v : β k}, (t.getThenInsertIfNew? k v).1 = t.get? k
• Std.DTreeMap.Raw.WF.partition_fst 📋 Std.Data.DTreeMap.Raw.WF
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {f : (a : α) → β a → Bool} : (Std.DTreeMap.Raw.partition f t).1.WF
• Std.TreeMap.map_fst_toList_eq_keys 📋 Std.Data.TreeMap.Lemmas
  {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} : List.map Prod.fst t.toList = t.keys
• Std.TreeMap.containsThenInsertIfNew_fst 📋 Std.Data.TreeMap.Lemmas
  {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β} : (t.containsThenInsertIfNew k v).1 = t.contains k
• Std.TreeMap.containsThenInsert_fst 📋 Std.Data.TreeMap.Lemmas
  {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β} : (t.containsThenInsert k v).1 = t.contains k
• Std.TreeMap.getThenInsertIfNew?_fst 📋 Std.Data.TreeMap.Lemmas
  {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β} : (t.getThenInsertIfNew? k v).1 = t[k]?
• Std.TreeSet.containsThenInsert_fst 📋 Std.Data.TreeSet.Lemmas
  {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α} : (t.containsThenInsert k).1 = t.contains k
• Std.ExtDHashMap.getThenInsertIfNew?_fst 📋 Std.Data.ExtDHashMap.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [LawfulBEq α] {k : α} {v : β k} : (m.getThenInsertIfNew? k v).1 = m.get? k
• Std.ExtDHashMap.containsThenInsertIfNew_fst 📋 Std.Data.ExtDHashMap.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} : (m.containsThenInsertIfNew k v).1 = m.contains k
• Std.ExtDHashMap.containsThenInsert_fst 📋 Std.Data.ExtDHashMap.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} : (m.containsThenInsert k v).1 = m.contains k
• Std.ExtDHashMap.Const.getThenInsertIfNew?_fst 📋 Std.Data.ExtDHashMap.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : (Std.ExtDHashMap.Const.getThenInsertIfNew? m k v).1 = Std.ExtDHashMap.Const.get? m k
• Std.ExtHashMap.containsThenInsertIfNew_fst 📋 Std.Data.ExtHashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : (m.containsThenInsertIfNew k v).1 = m.contains k
• Std.ExtHashMap.containsThenInsert_fst 📋 Std.Data.ExtHashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : (m.containsThenInsert k v).1 = m.contains k
• Std.ExtHashMap.getThenInsertIfNew?_fst 📋 Std.Data.ExtHashMap.Lemmas
  {α : Type u} {β : Type v} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.ExtHashMap α β} [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : (m.getThenInsertIfNew? k v).1 = m.get? k
• Std.ExtHashSet.containsThenInsert_fst 📋 Std.Data.ExtHashSet.Lemmas
  {α : Type u} {x✝ : BEq α} {x✝¹ : Hashable α} {m : Std.ExtHashSet α} [EquivBEq α] [LawfulHashable α] {k : α} : (m.containsThenInsert k).1 = m.contains k
• Std.ExtDTreeMap.Const.map_fst_toList_eq_keys 📋 Std.Data.ExtDTreeMap.Lemmas
  {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] : List.map Prod.fst (Std.ExtDTreeMap.Const.toList t) = t.keys
• Std.ExtDTreeMap.containsThenInsertIfNew_fst 📋 Std.Data.ExtDTreeMap.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β k} : (t.containsThenInsertIfNew k v).1 = t.contains k
• Std.ExtDTreeMap.containsThenInsert_fst 📋 Std.Data.ExtDTreeMap.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β k} : (t.containsThenInsert k v).1 = t.contains k
• Std.ExtDTreeMap.Const.getThenInsertIfNew?_fst 📋 Std.Data.ExtDTreeMap.Lemmas
  {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α} {v : β} : (Std.ExtDTreeMap.Const.getThenInsertIfNew? t k v).1 = Std.ExtDTreeMap.Const.get? t k
• Std.ExtDTreeMap.getThenInsertIfNew?_fst 📋 Std.Data.ExtDTreeMap.Lemmas
  {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {k : α} {v : β k} : (t.getThenInsertIfNew? k v).1 = t.get? k
• Std.ExtTreeMap.map_fst_toList_eq_keys 📋 Std.Data.ExtTreeMap.Lemmas
  {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [Std.TransCmp cmp] : List.map Prod.fst t.toList = t.keys
• Std.ExtTreeMap.containsThenInsertIfNew_fst 📋 Std.Data.ExtTreeMap.Lemmas
  {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β} : (t.containsThenInsertIfNew k v).1 = t.contains k
• Std.ExtTreeMap.containsThenInsert_fst 📋 Std.Data.ExtTreeMap.Lemmas
  {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β} : (t.containsThenInsert k v).1 = t.contains k
• Std.ExtTreeMap.getThenInsertIfNew?_fst 📋 Std.Data.ExtTreeMap.Lemmas
  {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β} : (t.getThenInsertIfNew? k v).1 = t[k]?
• Std.ExtTreeSet.containsThenInsert_fst 📋 Std.Data.ExtTreeSet.Lemmas
  {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [Std.TransCmp cmp] {k : α} : (t.containsThenInsert k).1 = t.contains k
• Std.TreeMap.Raw.map_fst_toList_eq_keys 📋 Std.Data.TreeMap.Raw.Lemmas
  {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} : List.map Prod.fst t.toList = t.keys
• Std.TreeMap.Raw.containsThenInsertIfNew_fst 📋 Std.Data.TreeMap.Raw.Lemmas
  {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.containsThenInsertIfNew k v).1 = t.contains k
• Std.TreeMap.Raw.containsThenInsert_fst 📋 Std.Data.TreeMap.Raw.Lemmas
  {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.containsThenInsert k v).1 = t.contains k
• Std.TreeMap.Raw.getThenInsertIfNew?_fst 📋 Std.Data.TreeMap.Raw.Lemmas
  {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.getThenInsertIfNew? k v).1 = t[k]?
• Std.TreeMap.Raw.WF.partition_fst 📋 Std.Data.TreeMap.Raw.WF
  {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {f : α → β → Bool} : (Std.TreeMap.Raw.partition f t).1.WF
• Std.TreeSet.Raw.containsThenInsert_fst 📋 Std.Data.TreeSet.Raw.Lemmas
  {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] (h : t.WF) {k : α} : (t.containsThenInsert k).1 = t.contains k
• Std.TreeSet.Raw.WF.partition_fst 📋 Std.Data.TreeSet.Raw.WF
  {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {f : α → Bool} : (Std.TreeSet.Raw.partition f t).1.WF
• Std.Sat.AIG.relabelNat'_fst_eq_relabelNat 📋 Std.Sat.AIG.RelabelNat
  {α : Type} [DecidableEq α] [Hashable α] {aig : Std.Sat.AIG α} : aig.relabelNat'.1 = aig.relabelNat
• Batteries.BinomialHeap.Imp.Heap.deleteMin_fst 📋 Batteries.Data.BinomialHeap.Lemmas
  {α : Type u_1} {s : Batteries.BinomialHeap.Imp.Heap α} {le : α → α → Bool} : Option.map (fun x => x.1) (Batteries.BinomialHeap.Imp.Heap.deleteMin le s) = Batteries.BinomialHeap.Imp.Heap.head? le s
• Batteries.PairingHeapImp.Heap.deleteMin_fst 📋 Batteries.Data.PairingHeap
  {α : Type u_1} {s : Batteries.PairingHeapImp.Heap α} {le : α → α → Bool} : Option.map (fun x => x.1) (Batteries.PairingHeapImp.Heap.deleteMin le s) = s.head?
• Prod.eq_iff_fst_eq_snd_eq 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} {p q : α × β} : p = q ↔ p.1 = q.1 ∧ p.2 = q.2
• Prod.map_fst' 📋 Mathlib.Data.Prod.Basic
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → γ) (g : β → δ) : Prod.fst ∘ Prod.map f g = f ∘ Prod.fst
• Pi.prod_snd_fst 📋 Mathlib.Algebra.Notation.Pi.Defs
  {α : Type u_2} {β : Type u_3} : Pi.prod Prod.snd Prod.fst = Prod.swap
• Pi.prod_fst_snd 📋 Mathlib.Algebra.Notation.Pi.Defs
  {α : Type u_2} {β : Type u_3} : Pi.prod Prod.fst Prod.snd = id
• monotone_fst 📋 Mathlib.Order.Monotone.Defs
  {α : Type u} {β : Type v} [Preorder α] [Preorder β] : Monotone Prod.fst
• Set.preimage_fst_singleton_eq_range 📋 Mathlib.Data.Set.Insert
  {α : Type u_1} {β : Type u_2} {a : α} : Prod.fst ⁻¹' {a} = Set.range fun x => (a, x)
• Set.Nontrivial.choose_fst_mem 📋 Mathlib.Data.Set.Subsingleton
  {α : Type u} {s : Set α} (hs : s.Nontrivial) : hs.choose.1 ∈ s
• Set.Nontrivial.choose_fst_ne_choose_snd 📋 Mathlib.Data.Set.Subsingleton
  {α : Type u} {s : Set α} (hs : s.Nontrivial) : hs.choose.1 ≠ hs.choose.2
• Equiv.prodCongrRight_apply_fst 📋 Mathlib.Logic.Equiv.Prod
  {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) (ab : α₁ × β₁) : ((Equiv.prodCongrRight e) ab).1 = ab.1
• Equiv.sumArrowEquivProdArrow_apply_fst 📋 Mathlib.Logic.Equiv.Prod
  {α : Type u_9} {β : Type u_10} {γ : Type u_11} (f : α ⊕ β → γ) (a : α) : ((Equiv.sumArrowEquivProdArrow α β γ) f).1 a = f (Sum.inl a)
• Equiv.prodCongrLeft_apply_fst 📋 Mathlib.Logic.Equiv.Prod
  {α₁ : Type u_9} {β₁ : Type u_11} {β₂ : Type u_12} (e : α₁ → β₁ ≃ β₂) (ab : β₁ × α₁) : ((Equiv.prodCongrLeft e) ab).1 = (e ab.2) ab.1
• Equiv.sigmaAssocProd_apply_fst 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} (a✝ : (a : α × β) × γ a.1 a.2) : (Equiv.sigmaAssocProd a✝).fst = ((Equiv.sigmaEquivProd α β).symm.sigmaCongrLeft' a✝).fst.fst
• Equiv.sigmaAssocProd_symm_apply_fst 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} (a✝ : (a : α) × (b : β) × γ a b) : (Equiv.sigmaAssocProd.symm a✝).fst = (((Equiv.sigmaAssoc γ).symm a✝).fst.fst, ((Equiv.sigmaAssoc γ).symm a✝).fst.snd)
• Equiv.sigmaAssocProd_apply_snd_fst 📋 Mathlib.Logic.Equiv.Basic
  {α : Type u_9} {β : Type u_10} {γ : α → β → Type u_11} (a✝ : (a : α × β) × γ a.1 a.2) : (Equiv.sigmaAssocProd a✝).snd.fst = ((Equiv.sigmaEquivProd α β).symm.sigmaCongrLeft' a✝).fst.snd
• bihimp_fst 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} {β : Type u_3} [GeneralizedHeytingAlgebra α] [GeneralizedHeytingAlgebra β] (a b : α × β) : (bihimp a b).1 = bihimp a.1 b.1
• symmDiff_fst 📋 Mathlib.Order.SymmDiff
  {α : Type u_2} {β : Type u_3} [GeneralizedCoheytingAlgebra α] [GeneralizedCoheytingAlgebra β] (a b : α × β) : (symmDiff a b).1 = symmDiff a.1 b.1
• Prod.range_fst 📋 Mathlib.Data.Set.Image
  {α : Type u_1} {β : Type u_2} [Nonempty β] : Set.range Prod.fst = Set.univ
• Set.image_fst_graphOn 📋 Mathlib.Data.Set.Prod
  {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) : Prod.fst '' Set.graphOn f s = s
• Set.mapsTo_fst_prod 📋 Mathlib.Data.Set.Prod
  {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} : Set.MapsTo Prod.fst (s ×ˢ t) s
• Set.prod_subset_preimage_fst 📋 Mathlib.Data.Set.Prod
  {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β) : s ×ˢ t ⊆ Prod.fst ⁻¹' s
• Set.subset_fst_image_prod_snd_image 📋 Mathlib.Data.Set.Prod
  {α : Type u_1} {β : Type u_2} {s : Set (α × β)} : s ⊆ (Prod.fst '' s) ×ˢ (Prod.snd '' s)
• Set.exists_eq_graphOn_image_fst 📋 Mathlib.Data.Set.Function
  {α : Type u_1} {β : Type u_2} [Nonempty β] {s : Set (α × β)} : (∃ f, s = Set.graphOn f (Prod.fst '' s)) ↔ Set.InjOn Prod.fst s
• Prod.pow_fst 📋 Mathlib.Algebra.Notation.Prod
  {E : Type u_8} {α : Type u_9} {β : Type u_10} [Pow α E] [Pow β E] (p : α × β) (c : E) : (p ^ c).1 = p.1 ^ c
• Prod.smul_fst 📋 Mathlib.Algebra.Notation.Prod
  {M : Type u_8} {α : Type u_9} {β : Type u_10} [SMul M α] [SMul M β] (a : M) (x : α × β) : (a • x).1 = a • x.1
• Prod.vadd_fst 📋 Mathlib.Algebra.Notation.Prod
  {M : Type u_8} {α : Type u_9} {β : Type u_10} [VAdd M α] [VAdd M β] (a : M) (x : α × β) : (a +ᵥ x).1 = a +ᵥ x.1
• AddHom.coe_fst 📋 Mathlib.Algebra.Group.Prod
  {M : Type u_3} {N : Type u_4} [Add M] [Add N] : ⇑(AddHom.fst M N) = Prod.fst
• MulHom.coe_fst 📋 Mathlib.Algebra.Group.Prod
  {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] : ⇑(MulHom.fst M N) = Prod.fst
• AddMonoidHom.coe_fst 📋 Mathlib.Algebra.Group.Prod
  {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] : ⇑(AddMonoidHom.fst M N) = Prod.fst
• MonoidHom.coe_fst 📋 Mathlib.Algebra.Group.Prod
  {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] : ⇑(MonoidHom.fst M N) = Prod.fst
• Nat.xgcdAux_fst 📋 Mathlib.Data.Int.GCD
  (x y : ℕ) (s t s' t' : ℤ) : (x.xgcdAux s t y s' t').1 = x.gcd y
• DirectedOn.isCofinalFor_fst_image_prod_snd_image 📋 Mathlib.Order.Bounds.Basic
  {α : Type u_1} [Preorder α] {β : Type u_4} [Preorder β] {s : Set (α × β)} (hs : DirectedOn (fun x1 x2 => x1 ≤ x2) s) : IsCofinalFor ((Prod.fst '' s) ×ˢ (Prod.snd '' s)) s
• Finset.insertPiProd_fst 📋 Mathlib.Data.Finset.Insert
  {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (f : α → Type u_3) (x : (i : α) → i ∈ insert a s → f i) : (Finset.insertPiProd f x).1 = x a ⋯
• Finset.consPiProd_fst 📋 Mathlib.Data.Finset.Insert
  {α : Type u_1} {s : Finset α} {a : α} (f : α → Type u_3) (has : a ∉ s) (x : (i : α) → i ∈ Finset.cons a s has → f i) : (Finset.consPiProd f has x).1 = x a ⋯
• Finset.subset_product_image_fst 📋 Mathlib.Data.Finset.Prod
  {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} [DecidableEq α] : Finset.image Prod.fst (s ×ˢ t) ⊆ s
• Finset.product_image_fst 📋 Mathlib.Data.Finset.Prod
  {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} [DecidableEq α] (ht : t.Nonempty) : Finset.image Prod.fst (s ×ˢ t) = s
• Set.finite_image_fst_and_snd_iff 📋 Mathlib.Data.Finite.Prod
  {α : Type u_1} {β : Type u_2} {s : Set (α × β)} : (Prod.fst '' s).Finite ∧ (Prod.snd '' s).Finite ↔ s.Finite
• Prod.Lex.monotone_fst_ofLex 📋 Mathlib.Data.Prod.Lex
  {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] : Monotone fun x => (ofLex x).1
• Prod.Lex.monotone_fst 📋 Mathlib.Data.Prod.Lex
  {α : Type u_1} {β : Type u_2} [Preorder α] [LE β] (t c : Lex (α × β)) (h : t ≤ c) : (ofLex t).1 ≤ (ofLex c).1
• Finset.sumEquiv_apply_fst 📋 Mathlib.Data.Finset.Sum
  {α : Type u_4} {β : Type u_5} (s : Finset (α ⊕ β)) : (Finset.sumEquiv s).1 = s.toLeft
• LatticeHom.coe_fst 📋 Mathlib.Order.Hom.Lattice
  {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] : ⇑LatticeHom.fst = Prod.fst
• List.revzip_map_fst 📋 Mathlib.Data.List.Zip
  {α : Type u} (l : List α) : List.map Prod.fst l.revzip = l
• NonUnitalRingHom.coe_fst 📋 Mathlib.Algebra.Ring.Prod
  {R : Type u_1} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] : ⇑(NonUnitalRingHom.fst R S) = Prod.fst
• RingHom.coe_fst 📋 Mathlib.Algebra.Ring.Prod
  {R : Type u_1} {S : Type u_3} [NonAssocSemiring R] [NonAssocSemiring S] : ⇑(RingHom.fst R S) = Prod.fst
• Prod.ωSupImpl_fst 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α × β)) : (Prod.ωSupImpl c).1 = OmegaCompletePartialOrder.ωSup (c.map OrderHom.fst)
• Prod.ωSup_fst 📋 Mathlib.Order.OmegaCompletePartialOrder
  {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α × β)) : (OmegaCompletePartialOrder.ωSup c).1 = OmegaCompletePartialOrder.ωSup (c.map OrderHom.fst)
• Multiset.antidiagonal_map_fst 📋 Mathlib.Data.Multiset.Antidiagonal
  {α : Type u_1} (s : Multiset α) : Multiset.map Prod.fst s.antidiagonal = s.powerset
• Finsupp.image_fst_graph 📋 Mathlib.Data.Finsupp.Basic
  {α : Type u_1} {M : Type u_5} [Zero M] [DecidableEq α] (f : α →₀ M) : Finset.image Prod.fst f.graph = f.support
• LinearMap.coe_fst 📋 Mathlib.LinearAlgebra.Prod
  {R : Type u} {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] : ⇑(LinearMap.fst R M M₂) = Prod.fst
• LinearEquiv.sumArrowLequivProdArrow_apply_fst 📋 Mathlib.LinearAlgebra.Pi
  {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_5} {β : Type u_6} (f : α ⊕ β → M) (a : α) : ((LinearEquiv.sumArrowLequivProdArrow α β R M) f).1 a = f (Sum.inl a)
• Finset.filter_fst_eq_antidiagonal 📋 Mathlib.Algebra.Order.Antidiag.Prod
  {A : Type u_1} [AddCommMonoid A] [PartialOrder A] [CanonicallyOrderedAdd A] [Sub A] [OrderedSub A] [AddLeftReflectLE A] [Finset.HasAntidiagonal A] (n m : A) [DecidablePred fun x => x = m] [Decidable (m ≤ n)] : {x ∈ Finset.antidiagonal n | x.1 = m} = if m ≤ n then {(m, n - m)} else ∅
• Finset.sigmaAntidiagonalEquivProd_symm_apply_fst 📋 Mathlib.Algebra.Order.Antidiag.Prod
  {A : Type u_1} [AddMonoid A] [Finset.HasAntidiagonal A] (x : A × A) : (Finset.sigmaAntidiagonalEquivProd.symm x).fst = x.1 + x.2
• Finset.Nat.antidiagonal_filter_le_fst_of_le 📋 Mathlib.Data.Finset.NatAntidiagonal
  {n k : ℕ} (h : k ≤ n) : {a ∈ Finset.antidiagonal n | k ≤ a.1} = Finset.map ({ toFun := fun x => x + k, inj' := ⋯ }.prodMap (Function.Embedding.refl ℕ)) (Finset.antidiagonal (n - k))
• Finset.Nat.antidiagonal_filter_fst_le_of_le 📋 Mathlib.Data.Finset.NatAntidiagonal
  {n k : ℕ} (h : k ≤ n) : {a ∈ Finset.antidiagonal n | a.1 ≤ k} = Finset.map ((Function.Embedding.refl ℕ).prodMap { toFun := fun x => x + (n - k), inj' := ⋯ }) (Finset.antidiagonal k)
• Filter.comap_fst_neBot 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} [Nonempty β] {f : Filter α} [f.NeBot] : (Filter.comap Prod.fst f).NeBot
• Filter.comap_fst_neBot_iff 📋 Mathlib.Order.Filter.Map
  {α : Type u_1} {β : Type u_2} {f : Filter α} : (Filter.comap Prod.fst f).NeBot ↔ f.NeBot ∧ Nonempty β
• Submodule.prodEquivOfIsCompl_symm_apply_fst_eq_zero 📋 Mathlib.LinearAlgebra.Projection
  {R : Type u_1} [Ring R] {E : Type u_2} [AddCommGroup E] [Module R E] (p q : Submodule R E) (h : IsCompl p q) {x : E} : ((p.prodEquivOfIsCompl q h).symm x).1 = 0 ↔ x ∈ q
• EuclideanDomain.xgcdAux_fst 📋 Mathlib.Algebra.EuclideanDomain.Basic
  {R : Type u} [EuclideanDomain R] [DecidableEq R] (x y s t s' t' : R) : (EuclideanDomain.xgcdAux x s t y s' t').1 = EuclideanDomain.gcd x y
• Module.Basis.prod_apply_inr_fst 📋 Mathlib.LinearAlgebra.Basis.Prod
  {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Module.Basis ι R M) (b' : Module.Basis ι' R M') (i : ι') : ((b.prod b') (Sum.inr i)).1 = 0
• Module.Basis.prod_apply_inl_fst 📋 Mathlib.LinearAlgebra.Basis.Prod
  {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {M' : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Module.Basis ι R M) (b' : Module.Basis ι' R M') (i : ι) : ((b.prod b') (Sum.inl i)).1 = b i
• Ideal.quotientInfEquivQuotientProd_fst 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u_2} [CommRing R] (I J : Ideal R) (coprime : IsCoprime I J) (x : R ⧸ I ⊓ J) : ((I.quotientInfEquivQuotientProd J coprime) x).1 = (Ideal.Quotient.factor ⋯) x
• Ideal.quotientMulEquivQuotientProd_fst 📋 Mathlib.RingTheory.Ideal.Quotient.Operations
  {R : Type u_2} [CommRing R] (I J : Ideal R) (coprime : IsCoprime I J) (x : R ⧸ I * J) : ((I.quotientMulEquivQuotientProd J coprime) x).1 = (Ideal.Quotient.factor ⋯) x
• List.permutationsAux2_fst 📋 Mathlib.Data.List.Permutation
  {α : Type u_1} {β : Type u_2} (t : α) (ts : List α) (r : List β) (ys : List α) (f : List α → β) : (List.permutationsAux2 t ts r ys f).1 = ys ++ ts
• Function.minimalPeriod_fst_dvd 📋 Mathlib.Dynamics.PeriodicPts.Lemmas
  {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} {x : α × β} : Function.minimalPeriod f x.1 ∣ Function.minimalPeriod (Prod.map f g) x
• AddAction.orbitRel_le_fst 📋 Mathlib.GroupTheory.GroupAction.Basic
  (G : Type u_1) (α : Type u_2) (β : Type u_3) [AddGroup G] [AddAction G α] [AddAction G β] : AddAction.orbitRel G (α × β) ≤ Setoid.comap Prod.fst (AddAction.orbitRel G α)
• MulAction.orbitRel_le_fst 📋 Mathlib.GroupTheory.GroupAction.Basic
  (G : Type u_1) (α : Type u_2) (β : Type u_3) [Group G] [MulAction G α] [MulAction G β] : MulAction.orbitRel G (α × β) ≤ Setoid.comap Prod.fst (MulAction.orbitRel G α)
• Nat.sortedLT_map_fst_divisorsAntidiagonalList 📋 Mathlib.NumberTheory.Divisors
  {n : ℕ} : (List.map Prod.fst n.divisorsAntidiagonalList).SortedLT
• Nat.image_fst_divisorsAntidiagonal 📋 Mathlib.NumberTheory.Divisors
  {n : ℕ} : Finset.image Prod.fst n.divisorsAntidiagonal = n.divisors
• Nat.pairwise_divisorsAntidiagonalList_fst 📋 Mathlib.NumberTheory.Divisors
  {n : ℕ} : List.Pairwise (fun x1 x2 => x1.1 < x2.1) n.divisorsAntidiagonalList
• Nat.sorted_divisorsAntidiagonalList_fst 📋 Mathlib.NumberTheory.Divisors
  {n : ℕ} : List.Pairwise (fun x1 x2 => x1.1 < x2.1) n.divisorsAntidiagonalList
• addOrderOf_fst_dvd_addOrderOf 📋 Mathlib.GroupTheory.OrderOfElement
  {α : Type u_4} {β : Type u_5} [AddMonoid α] [AddMonoid β] {x : α × β} : addOrderOf x.1 ∣ addOrderOf x
• orderOf_fst_dvd_orderOf 📋 Mathlib.GroupTheory.OrderOfElement
  {α : Type u_4} {β : Type u_5} [Monoid α] [Monoid β] {x : α × β} : orderOf x.1 ∣ orderOf x
• Submonoid.LocalizationMap.sec_zero_fst 📋 Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
  {M : Type u_1} [CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [CommMonoidWithZero N] {f : S.LocalizationMap N} : f (f.sec 0).1 = 0
• IsLocalization.sec_fst_ne_zero 📋 Mathlib.RingTheory.Localization.Defs
  {R : Type u_1} [CommSemiring R] {M : Submonoid R} {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {x : S} (hx : x ≠ 0) : (IsLocalization.sec M x).1 ≠ 0
• Filter.tendsto_fst 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} : Filter.Tendsto Prod.fst (f ×ˢ g) f
• Filter.map_fst_prod 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Filter β) [g.NeBot] : Filter.map Prod.fst (f ×ˢ g) = f
• Filter.le_prod_map_fst_snd 📋 Mathlib.Order.Filter.Prod
  {α : Type u_1} {β : Type u_2} {f : Filter (α × β)} : f ≤ Filter.map Prod.fst f ×ˢ Filter.map Prod.snd f
• continuous_fst 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : Continuous Prod.fst
• isOpenMap_fst 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] : IsOpenMap Prod.fst
• isQuotientMap_fst 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [Nonempty Y] : Topology.IsQuotientMap Prod.fst
• continuousAt_fst 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {p : X × Y} : ContinuousAt Prod.fst p
• map_fst_nhds 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (x : X × Y) : Filter.map Prod.fst (nhds x) = nhds x.1
• map_fst_nhdsWithin 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (x : X × Y) : Filter.map Prod.fst (nhdsWithin x (Prod.snd ⁻¹' {x.2})) = nhds x.1
• continuousOn_fst 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set (α × β)} : ContinuousOn Prod.fst s
• continuousWithinAt_fst 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set (α × β)} {p : α × β} : ContinuousWithinAt Prod.fst s p
• uniformContinuous_fst 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] : UniformContinuous fun p => p.1
• tendsto_prod_uniformity_fst 📋 Mathlib.Topology.UniformSpace.Basic
  {α : Type ua} {β : Type ub} [UniformSpace α] [UniformSpace β] : Filter.Tendsto (fun p => (p.1.1, p.2.1)) (uniformity (α × β)) (uniformity α)

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 6ff4759 serving mathlib revision ee6d0f1