Loogle!

Result

Found 1992 declarations mentioning inferInstance. Of these, only the first 200 are shown.

• inferInstance 📋 Init.Prelude
  {α : Sort u} [i : α] : α
• Array.instForIn'InferInstanceMembershipOfMonad 📋 Init.Data.Array.Basic
  {α : Type u} {m : Type u_1 → Type u_2} [Monad m] : ForIn' m (Array α) α inferInstance
• List.instForIn'InferInstanceMembershipOfMonad 📋 Init.Data.List.Control
  {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] : ForIn' m (List α) α inferInstance
• List.forIn_nil 📋 Init.Data.List.Control
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {f : α → β → m (ForInStep β)} {b : β} : forIn [] b f = pure b
• Option.instForIn'InferInstanceMembershipOfMonad 📋 Init.Data.Option.Instances
  {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] : ForIn' m (Option α) α inferInstance
• List.idRun_forIn_yield_eq_foldl 📋 Init.Data.List.Monadic
  {α : Type u_1} {β : Type u_2} (l : List α) (f : α → β → Id β) (init : β) : (forIn l init fun a b => ForInStep.yield <$> f a b).run = List.foldl (fun b a => (f a b).run) init l
• List.forIn_pure_yield_eq_foldl 📋 Init.Data.List.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {l : List α} (f : α → β → β) (init : β) : (forIn l init fun a b => pure (ForInStep.yield (f a b))) = pure (List.foldl (fun b a => f a b) init l)
• List.forIn_map 📋 Init.Data.List.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {init : γ} [Monad m] [LawfulMonad m] {l : List α} {g : α → β} {f : β → γ → m (ForInStep γ)} : forIn (List.map g l) init f = forIn l init fun a y => f (g a) y
• List.forIn_yield_eq_foldlM 📋 Init.Data.List.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β γ : Type u_1} [Monad m] [LawfulMonad m] {l : List α} (f : α → β → m γ) (g : α → β → γ → β) (init : β) : (forIn l init fun a b => (fun c => ForInStep.yield (g a b c)) <$> f a b) = List.foldlM (fun b a => g a b <$> f a b) init l
• List.forIn_eq_foldlM 📋 Init.Data.List.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {l : List α} (f : α → β → m (ForInStep β)) (init : β) : forIn l init f = ForInStep.value <$> List.foldlM (fun b a => match b with | ForInStep.yield b => f a b | ForInStep.done b => pure (ForInStep.done b)) (ForInStep.yield init) l
• List.forIn_cons 📋 Init.Data.List.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m (ForInStep β)) (a : α) (as : List α) (b : β) : forIn (a :: as) b f = do let x ← f a b match x with | ForInStep.done b => pure b | ForInStep.yield b => forIn as b f
• List.forIn_toArray 📋 Init.Data.List.ToArray
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (l : List α) (b : β) (f : α → β → m (ForInStep β)) : forIn l.toArray b f = forIn l b f
• List.forIn'_loop_toArray 📋 Init.Data.List.ToArray
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (i : ℕ) (h : i ≤ l.length) (b : β) : Array.forIn'.loop l.toArray f i h b = forIn' (List.drop (l.length - i) l) b fun a m b => f a ⋯ b
• Array.forIn_toList 📋 Init.Data.Array.Lemmas
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {xs : Array α} {b : β} {f : α → β → m (ForInStep β)} : forIn xs.toList b f = forIn xs b f
• Std.IterM.forIn_toArray 📋 Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
  {m : Type w → Type u_1} {γ α β : Type w} [Monad m] [LawfulMonad m] [Std.Iterator α Id β] [Std.Iterators.Finite α Id] [Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {it : Std.IterM Id β} {f : β → γ → m (ForInStep γ)} {init : γ} : forIn it.toArray.run init f = forIn it init f
• Std.IterM.forIn_toList 📋 Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
  {m : Type w → Type u_1} {γ α β : Type w} [Monad m] [LawfulMonad m] [Std.Iterator α Id β] [Std.Iterators.Finite α Id] [Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {it : Std.IterM Id β} {f : β → γ → m (ForInStep γ)} {init : γ} : forIn it.toList.run init f = forIn it init f
• Option.forIn_toList 📋 Init.Data.Option.List
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (o : Option α) (b : β) (f : α → β → m (ForInStep β)) : forIn o.toList b f = forIn o b f
• Option.forIn'_toList 📋 Init.Data.Option.List
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (o : Option α) (b : β) (f : (a : α) → a ∈ o.toList → β → m (ForInStep β)) : forIn' o.toList b f = forIn' o b fun a m b => f a ⋯ b
• Option.forIn_toArray 📋 Init.Data.Option.Array
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (o : Option α) (b : β) (f : α → β → m (ForInStep β)) : forIn o.toArray b f = forIn o b f
• Option.forIn'_toArray 📋 Init.Data.Option.Array
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (o : Option α) (b : β) (f : (a : α) → a ∈ o.toArray → β → m (ForInStep β)) : forIn' o.toArray b f = forIn' o b fun a m b => f a ⋯ b
• Array.idRun_forIn_yield_eq_foldl 📋 Init.Data.Array.Monadic
  {α : Type u_1} {β : Type u_2} {xs : Array α} (f : α → β → Id β) (init : β) : (forIn xs init fun a b => ForInStep.yield <$> f a b).run = Array.foldl (fun b a => (f a b).run) init xs
• Array.forIn_map 📋 Init.Data.Array.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {init : γ} [Monad m] [LawfulMonad m] {xs : Array α} {g : α → β} {f : β → γ → m (ForInStep γ)} : forIn (Array.map g xs) init f = forIn xs init fun a y => f (g a) y
• Array.forIn_pure_yield_eq_foldl 📋 Init.Data.Array.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Array α} (f : α → β → β) (init : β) : (forIn xs init fun a b => pure (ForInStep.yield (f a b))) = pure (Array.foldl (fun b a => f a b) init xs)
• Array.forIn_yield_eq_foldlM 📋 Init.Data.Array.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β γ : Type u_1} [Monad m] [LawfulMonad m] {xs : Array α} (f : α → β → m γ) (g : α → β → γ → β) (init : β) : (forIn xs init fun a b => (fun c => ForInStep.yield (g a b c)) <$> f a b) = Array.foldlM (fun b a => g a b <$> f a b) init xs
• Array.forIn_eq_foldlM 📋 Init.Data.Array.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Array α} (f : α → β → m (ForInStep β)) (init : β) : forIn xs init f = ForInStep.value <$> Array.foldlM (fun b a => match b with | ForInStep.yield b => f a b | ForInStep.done b => pure (ForInStep.done b)) (ForInStep.yield init) xs
• Std.Rii.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLeast?OfMonadOfFiniteIteratorId 📋 Init.Data.Range.Polymorphic.Iterators
  {α : Type u} {m : Type u → Type u_1} [Std.PRange.UpwardEnumerable α] [Std.PRange.Least? α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLeast? α] [Monad m] [Std.Iterators.Finite (Std.Rxi.Iterator α) Id] : ForIn' m (Std.Rii α) α inferInstance
• Std.Rci.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLEOfMonadOfFiniteIteratorId 📋 Init.Data.Range.Polymorphic.Iterators
  {α : Type u} {m : Type u → Type u_1} [Std.PRange.UpwardEnumerable α] [LE α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Monad m] [Std.Iterators.Finite (Std.Rxi.Iterator α) Id] : ForIn' m (Std.Rci α) α inferInstance
• Std.Roi.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLTOfMonadOfFiniteIteratorId 📋 Init.Data.Range.Polymorphic.Iterators
  {α : Type u} {m : Type u → Type u_1} [Std.PRange.UpwardEnumerable α] [LT α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Monad m] [Std.Iterators.Finite (Std.Rxi.Iterator α) Id] : ForIn' m (Std.Roi α) α inferInstance
• Std.Rcc.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLEOfMonadOfFiniteIteratorId 📋 Init.Data.Range.Polymorphic.Iterators
  {α : Type u} {m : Type u → Type u_1} [Std.PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Monad m] [Std.Iterators.Finite (Std.Rxc.Iterator α) Id] : ForIn' m (Std.Rcc α) α inferInstance
• Std.Roo.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLTOfMonadOfFiniteIteratorId 📋 Init.Data.Range.Polymorphic.Iterators
  {α : Type u} {m : Type u → Type u_1} [Std.PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Monad m] [Std.Iterators.Finite (Std.Rxo.Iterator α) Id] : ForIn' m (Std.Roo α) α inferInstance
• Std.Ric.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLEOfLawfulUpwardEnumerableLeast?OfMonadOfFiniteIteratorId 📋 Init.Data.Range.Polymorphic.Iterators
  {α : Type u} {m : Type u → Type u_1} [Std.PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [Std.PRange.Least? α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLeast? α] [Monad m] [Std.Iterators.Finite (Std.Rxc.Iterator α) Id] : ForIn' m (Std.Ric α) α inferInstance
• Std.Rio.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLTOfLawfulUpwardEnumerableLeast?OfMonadOfFiniteIteratorId 📋 Init.Data.Range.Polymorphic.Iterators
  {α : Type u} {m : Type u → Type u_1} [Std.PRange.UpwardEnumerable α] [LT α] [DecidableLT α] [Std.PRange.Least? α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLeast? α] [Monad m] [Std.Iterators.Finite (Std.Rxo.Iterator α) Id] : ForIn' m (Std.Rio α) α inferInstance
• Std.Rco.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLEOfLawfulUpwardEnumerableLTOfMonadOfFiniteIteratorId 📋 Init.Data.Range.Polymorphic.Iterators
  {α : Type u} {m : Type u → Type u_1} [Std.PRange.UpwardEnumerable α] [LE α] [LT α] [DecidableLT α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α] [Monad m] [Std.Iterators.Finite (Std.Rxo.Iterator α) Id] : ForIn' m (Std.Rco α) α inferInstance
• Std.Roc.instForIn'InferInstanceMembershipOfLawfulUpwardEnumerableOfLawfulUpwardEnumerableLEOfLawfulUpwardEnumerableLTOfMonadOfFiniteIteratorId 📋 Init.Data.Range.Polymorphic.Iterators
  {α : Type u} {m : Type u → Type u_1} [Std.PRange.UpwardEnumerable α] [LE α] [DecidableLE α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [LT α] [Std.PRange.LawfulUpwardEnumerableLT α] [Monad m] [Std.Iterators.Finite (Std.Rxc.Iterator α) Id] : ForIn' m (Std.Roc α) α inferInstance
• Vector.instForIn'InferInstanceMembershipOfMonad 📋 Init.Data.Vector.Basic
  {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} [Monad m] : ForIn' m (Vector α n) α inferInstance
• Std.Iter.forIn_toArray 📋 Init.Data.Iterators.Lemmas.Consumers.Loop
  {α β : Type w} [Std.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m] [Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {γ : Type x} {it : Std.Iter β} {init : γ} {f : β → γ → m (ForInStep γ)} : forIn it.toArray init f = forIn it init f
• Std.Iter.forIn_toList 📋 Init.Data.Iterators.Lemmas.Consumers.Loop
  {α β : Type w} [Std.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m] [Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {γ : Type x} {it : Std.Iter β} {init : γ} {f : β → γ → m (ForInStep γ)} : forIn it.toList init f = forIn it init f
• Std.Iter.forIn'_toArray 📋 Init.Data.Iterators.Lemmas.Consumers.Loop
  {α β : Type w} [Std.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m] [Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] [Std.LawfulDeterministicIterator α Id] {γ : Type x} {it : Std.Iter β} {init : γ} {f : (out : β) → out ∈ it.toArray → γ → m (ForInStep γ)} : forIn' it.toArray init f = forIn' it init fun out h acc => f out ⋯ acc
• Std.Iter.forIn'_toList 📋 Init.Data.Iterators.Lemmas.Consumers.Loop
  {α β : Type w} [Std.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type x → Type x'} [Monad m] [LawfulMonad m] [Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] [Std.LawfulDeterministicIterator α Id] {γ : Type x} {it : Std.Iter β} {init : γ} {f : (out : β) → out ∈ it.toList → γ → m (ForInStep γ)} : forIn' it.toList init f = forIn' it init fun out h acc => f out ⋯ acc
• String.forIn_eq_forIn_toList 📋 Init.Data.String.Lemmas.Iterate
  {β : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] {s : String} {b : β} {f : Char → β → m (ForInStep β)} : forIn s b f = forIn s.toList b f
• String.Slice.forIn_eq_forIn_toList 📋 Init.Data.String.Lemmas.Iterate
  {β : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] {s : String.Slice} {b : β} {f : Char → β → m (ForInStep β)} : forIn s b f = forIn s.copy.toList b f
• Vector.forIn_mk 📋 Init.Data.Vector.Lemmas
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [Monad m] {f : α → β → m (ForInStep β)} {xs : Array α} (h : xs.size = n) {b : β} : forIn (Vector.mk xs h) b f = forIn xs b f
• Vector.forIn'_mk 📋 Init.Data.Vector.Lemmas
  {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [Monad m] {xs : Array α} (h : xs.size = n) {b : β} {f : (a : α) → a ∈ Vector.mk xs h → β → m (ForInStep β)} : forIn' (Vector.mk xs h) b f = forIn' xs b fun a m b => f a ⋯ b
• Std.Legacy.Range.instForIn'NatInferInstanceMembershipOfMonad 📋 Init.Data.Range.Basic
  {m : Type u_1 → Type u_2} [Monad m] : ForIn' m Std.Legacy.Range ℕ inferInstance
• Std.Legacy.Range.forIn_eq_forIn_range' 📋 Init.Data.Range.Lemmas
  {m : Type u_1 → Type u_2} {β : Type u_1} [Monad m] (r : Std.Legacy.Range) (init : β) (f : ℕ → β → m (ForInStep β)) : forIn r init f = forIn (List.range' r.start r.size r.step) init f
• Std.Rii.forIn'_eq_forIn'_toArray 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Rii α} [Std.PRange.Least? α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLeast? α] [Std.Rxi.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' r.toArray init fun a x acc => f a ⋯ acc
• Std.Rii.forIn'_eq_forIn'_toList 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Rii α} [Std.PRange.Least? α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLeast? α] [Std.Rxi.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' r.toList init fun a x acc => f a ⋯ acc
• Std.Rci.forIn'_toArray_eq_forIn' 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Rci α} [LE α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.Rxi.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)} : forIn' r.toArray init f = forIn' r init fun a ha acc => f a ⋯ acc
• Std.Rci.forIn'_toList_eq_forIn' 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Rci α} [LE α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.Rxi.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)} : forIn' r.toList init f = forIn' r init fun a ha acc => f a ⋯ acc
• Std.Roi.forIn'_toArray_eq_forIn' 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Roi α} [LT α] [DecidableLT α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxi.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)} : forIn' r.toArray init f = forIn' r init fun a ha acc => f a ⋯ acc
• Std.Roi.forIn'_toList_eq_forIn' 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Roi α} [LT α] [DecidableLT α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxi.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)} : forIn' r.toList init f = forIn' r init fun a ha acc => f a ⋯ acc
• Std.Rii.forIn'_toArray_eq_forIn' 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Rii α} [LT α] [Std.PRange.Least? α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLeast? α] [Std.Rxi.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)} : forIn' r.toArray init f = forIn' r init fun a x acc => f a ⋯ acc
• Std.Rii.forIn'_toList_eq_forIn' 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Rii α} [LT α] [Std.PRange.Least? α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLeast? α] [Std.Rxi.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)} : forIn' r.toList init f = forIn' r init fun a x acc => f a ⋯ acc
• Std.Rii.forIn'_eq_match_rci 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Rii α} [LE α] [Std.PRange.Least? α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLeast? α] [Std.Rxi.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = match Std.PRange.least? with | none => pure init | some next => forIn' next...* init fun a x acc => f a ⋯ acc
• Std.Rcc.forIn'_toArray_eq_forIn' 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Rcc α} [LE α] [DecidableLE α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.Rxc.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)} : forIn' r.toArray init f = forIn' r init fun a ha acc => f a ⋯ acc
• Std.Rcc.forIn'_toList_eq_forIn' 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Rcc α} [LE α] [DecidableLE α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.Rxc.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)} : forIn' r.toList init f = forIn' r init fun a ha acc => f a ⋯ acc
• Std.Roo.forIn'_toArray_eq_forIn' 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Roo α} [LT α] [DecidableLT α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxo.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)} : forIn' r.toArray init f = forIn' r init fun a ha acc => f a ⋯ acc
• Std.Roo.forIn'_toList_eq_forIn' 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Roo α} [LT α] [DecidableLT α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxo.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)} : forIn' r.toList init f = forIn' r init fun a ha acc => f a ⋯ acc
• Std.Rco.forIn'_toArray_eq_forIn' 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Rco α} [LE α] [LT α] [DecidableLT α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxo.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)} : forIn' r.toArray init f = forIn' r init fun a ha acc => f a ⋯ acc
• Std.Rco.forIn'_toList_eq_forIn' 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Rco α} [LE α] [LT α] [DecidableLT α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxo.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)} : forIn' r.toList init f = forIn' r init fun a ha acc => f a ⋯ acc
• Std.Ric.forIn'_toArray_eq_forIn' 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Ric α} [LE α] [DecidableLE α] [Std.PRange.Least? α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLeast? α] [Std.Rxc.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)} : forIn' r.toArray init f = forIn' r init fun a ha acc => f a ⋯ acc
• Std.Ric.forIn'_toList_eq_forIn' 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Ric α} [LE α] [DecidableLE α] [Std.PRange.Least? α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLeast? α] [Std.Rxc.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)} : forIn' r.toList init f = forIn' r init fun a ha acc => f a ⋯ acc
• Std.Rio.forIn'_toArray_eq_forIn' 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Rio α} [LT α] [DecidableLT α] [Std.PRange.Least? α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLeast? α] [Std.Rxo.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)} : forIn' r.toArray init f = forIn' r init fun a ha acc => f a ⋯ acc
• Std.Rio.forIn'_toList_eq_forIn' 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Rio α} [LT α] [DecidableLT α] [Std.PRange.Least? α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLeast? α] [Std.Rxo.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)} : forIn' r.toList init f = forIn' r init fun a ha acc => f a ⋯ acc
• Std.Roc.forIn'_toArray_eq_forIn' 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Roc α} [LE α] [DecidableLE α] [LT α] [DecidableLT α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxc.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toArray → γ → m (ForInStep γ)} : forIn' r.toArray init f = forIn' r init fun a ha acc => f a ⋯ acc
• Std.Roc.forIn'_toList_eq_forIn' 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Roc α} [LE α] [DecidableLE α] [LT α] [DecidableLT α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxc.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [Monad m] [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)} : forIn' r.toList init f = forIn' r init fun a ha acc => f a ⋯ acc
• Std.Ric.forIn'_eq_forIn'_rcc 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Ric α} [LE α] [DecidableLE α] [Std.PRange.Least? α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLeast? α] [Std.Rxc.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' (Std.PRange.UpwardEnumerable.least...=r.upper) init fun a ha acc => f a ⋯ acc
• Std.Rcc.forIn'_congr 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} [LE α] [DecidableLE α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.Rxc.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] {γ : Type u} {init init' : γ} {r r' : Std.Rcc α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)} (hr : r = r') (hi : init = init') (h : ∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) : forIn' r init f = forIn' r' init' f'
• Std.Rii.forIn'_congr 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} [Std.PRange.UpwardEnumerable α] [Std.PRange.Least? α] [Std.Rxi.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLeast? α] {m : Type u → Type w} [Monad m] {γ : Type u} {init init' : γ} {r r' : Std.Rii α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)} (hr : r = r') (hi : init = init') (h : ∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) : forIn' r init f = forIn' r' init' f'
• Std.Rio.forIn'_eq_forIn'_rco 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Rio α} [LE α] [LT α] [DecidableLT α] [Std.PRange.Least? α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLeast? α] [Std.Rxo.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = forIn' (Std.PRange.UpwardEnumerable.least...r.upper) init fun a ha acc => f a ⋯ acc
• Std.Rii.forIn'_eq_match_roi 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Rii α} {hu : True} [LT α] [Std.PRange.Least? α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLeast? α] [Std.Rxi.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = match Std.PRange.least? with | none => pure init | some next => do let __do_lift ← f next hu init match __do_lift with | ForInStep.yield c => forIn' next<...* c fun a x acc => f a ⋯ acc | ForInStep.done c => pure c
• Std.Rci.forIn'_congr 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} [LE α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.Rxi.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] {γ : Type u} {init init' : γ} {r r' : Std.Rci α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)} (hr : r = r') (hi : init = init') (h : ∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) : forIn' r init f = forIn' r' init' f'
• Std.Roi.forIn'_congr 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} [LT α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxi.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] {γ : Type u} {init init' : γ} {r r' : Std.Roi α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)} (hr : r = r') (hi : init = init') (h : ∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) : forIn' r init f = forIn' r' init' f'
• Std.Rco.forIn'_congr 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} [LE α] [LT α] [DecidableLT α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxo.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] {γ : Type u} {init init' : γ} {r r' : Std.Rco α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)} (hr : r = r') (hi : init = init') (h : ∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) : forIn' r init f = forIn' r' init' f'
• Std.Roc.forIn'_congr 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} [LE α] [LT α] [DecidableLE α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxc.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] {γ : Type u} {init init' : γ} {r r' : Std.Roc α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)} (hr : r = r') (hi : init = init') (h : ∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) : forIn' r init f = forIn' r' init' f'
• Std.Rci.forIn'_eq_match 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Rci α} [LE α] [DecidableLE α] [LT α] [DecidableLT α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.Rxi.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = have hle := ⋯; do let __do_lift ← f r.lower hle init match __do_lift with | ForInStep.yield c => forIn' r.lower<...* c fun a ha acc => f a ⋯ acc | ForInStep.done c => pure c
• Std.Roo.forIn'_congr 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} [LT α] [DecidableLT α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxo.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] {γ : Type u} {init init' : γ} {r r' : Std.Roo α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)} (hr : r = r') (hi : init = init') (h : ∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) : forIn' r init f = forIn' r' init' f'
• Std.Ric.forIn'_congr 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} [LE α] [DecidableLE α] [Std.PRange.Least? α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLeast? α] [Std.Rxc.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] {γ : Type u} {init init' : γ} {r r' : Std.Ric α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)} (hr : r = r') (hi : init = init') (h : ∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) : forIn' r init f = forIn' r' init' f'
• Std.Rio.forIn'_congr 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} [LT α] [DecidableLT α] [Std.PRange.Least? α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLeast? α] [Std.Rxo.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] {γ : Type u} {init init' : γ} {r r' : Std.Rio α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)} (hr : r = r') (hi : init = init') (h : ∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) : forIn' r init f = forIn' r' init' f'
• Std.Rcc.forIn'_eq_if 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Rcc α} [LE α] [DecidableLE α] [LT α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.Rxc.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = if hu : r.lower ≤ r.upper then have hle := ⋯; do let __do_lift ← f r.lower ⋯ init match __do_lift with | ForInStep.yield c => forIn' (r.lower<...=r.upper) c fun a ha acc => f a ⋯ acc | ForInStep.done c => pure c else pure init
• Std.Rco.forIn'_eq_if 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Rco α} [LE α] [DecidableLE α] [LT α] [DecidableLT α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.Rxo.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = if hu : r.lower < r.upper then have hle := ⋯; do let __do_lift ← f r.lower ⋯ init match __do_lift with | ForInStep.yield c => forIn' (r.lower<...r.upper) c fun a ha acc => f a ⋯ acc | ForInStep.done c => pure c else pure init
• Std.Rio.forIn'_eq_if_roo 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Rio α} [LT α] [DecidableLT α] [Std.PRange.Least? α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLeast? α] [Std.Rxo.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = if hu : Std.PRange.UpwardEnumerable.least < r.upper then do let __do_lift ← f Std.PRange.UpwardEnumerable.least hu init match __do_lift with | ForInStep.yield c => forIn' (Std.PRange.UpwardEnumerable.least<...r.upper) c fun a ha acc => f a ⋯ acc | ForInStep.done c => pure c else pure init
• Std.Ric.forIn'_eq_if_roc 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Ric α} [LE α] [DecidableLE α] [LT α] [Std.PRange.Least? α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLeast? α] [Std.Rxc.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = if hu : Std.PRange.UpwardEnumerable.least ≤ r.upper then do let __do_lift ← f Std.PRange.UpwardEnumerable.least hu init match __do_lift with | ForInStep.yield c => forIn' (Std.PRange.UpwardEnumerable.least<...=r.upper) c fun a ha acc => f a ⋯ acc | ForInStep.done c => pure c else pure init
• Std.Roi.forIn'_eq_match 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Roi α} [LT α] [DecidableLT α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxi.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = match hs : Std.PRange.succ? r.lower with | none => pure init | some next => have hlt := ⋯; have hle := ⋯; do let __do_lift ← f next hlt init match __do_lift with | ForInStep.yield c => forIn' next<...* c fun a ha acc => f a ⋯ acc | ForInStep.done c => pure c
• Std.Roo.forIn'_eq_match 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Roo α} [LT α] [DecidableLT α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxo.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = match hs : Std.PRange.succ? r.lower with | none => pure init | some next => if hu : next < r.upper then have hlt := ⋯; have hle := ⋯; do let __do_lift ← f next ⋯ init match __do_lift with | ForInStep.yield c => forIn' (next<...r.upper) c fun a ha acc => f a ⋯ acc | ForInStep.done c => pure c else pure init
• Std.Roc.forIn'_eq_match 📋 Init.Data.Range.Polymorphic.Lemmas
  {α : Type u} {r : Std.Roc α} [LE α] [DecidableLE α] [LT α] [DecidableLT α] [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.Rxc.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [Monad m] [LawfulMonad m] {γ : Type u} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} : forIn' r init f = match hs : Std.PRange.succ? r.lower with | none => pure init | some next => if hu : next ≤ r.upper then have hlt := ⋯; do let __do_lift ← f next ⋯ init match __do_lift with | ForInStep.yield c => forIn' (next<...=r.upper) c fun a ha acc => f a ⋯ acc | ForInStep.done c => pure c else pure init
• Std.Slice.forIn_toArray 📋 Init.Data.Slice.Lemmas
  {α : Type v} {γ : Type u} {β : Type v} {m : Type w → Type x} [Monad m] [LawfulMonad m] {δ : Type w} [Std.ToIterator (Std.Slice γ) Id α β] [Std.Iterator α Id β] [Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] [Std.Iterators.Finite α Id] {s : Std.Slice γ} {init : δ} {f : β → δ → m (ForInStep δ)} : forIn s.toArray init f = forIn s init f
• Std.Slice.forIn_toList 📋 Init.Data.Slice.Lemmas
  {α : Type v} {γ : Type u} {β : Type v} {m : Type w → Type x} [Monad m] [LawfulMonad m] {δ : Type w} [Std.ToIterator (Std.Slice γ) Id α β] [Std.Iterator α Id β] [Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] [Std.Iterators.Finite α Id] {s : Std.Slice γ} {init : δ} {f : β → δ → m (ForInStep δ)} : forIn s.toList init f = forIn s init f
• Subarray.forIn_eq_forIn_toList 📋 Init.Data.Slice.Array.Lemmas
  {α : Type u} {s : Subarray α} {m : Type v → Type w} [Monad m] [LawfulMonad m] {γ : Type v} {init : γ} {f : α → γ → m (ForInStep γ)} : forIn s init f = forIn (Std.Slice.toList s) init f
• Subarray.forIn_toArray 📋 Init.Data.Slice.Array.Lemmas
  {α : Type u} {s : Subarray α} {m : Type v → Type w} [Monad m] [LawfulMonad m] {γ : Type v} {init : γ} {f : α → γ → m (ForInStep γ)} : forIn (Std.Slice.toArray s) init f = forIn s init f
• Subarray.forIn_toList 📋 Init.Data.Slice.Array.Lemmas
  {α : Type u} {s : Subarray α} {m : Type v → Type w} [Monad m] [LawfulMonad m] {γ : Type v} {init : γ} {f : α → γ → m (ForInStep γ)} : forIn (Std.Slice.toList s) init f = forIn s init f
• Option.forIn_none 📋 Init.Data.Option.Monadic
  {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] (b : β) (f : α → β → m (ForInStep β)) : forIn none b f = pure b
• Option.idRun_forIn_yield_eq_elim 📋 Init.Data.Option.Monadic
  {α : Type u_1} {β : Type u_2} (o : Option α) (f : α → β → Id β) (b : β) : (forIn o b fun a b => ForInStep.yield <$> f a b).run = o.elim b fun a => (f a b).run
• Option.forIn_some 📋 Init.Data.Option.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (a : α) (b : β) (f : α → β → m (ForInStep β)) : forIn (some a) b f = do let r ← f a b pure r.value
• Option.forIn_eq_elim 📋 Init.Data.Option.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (o : Option α) (f : α → β → m (ForInStep β)) (b : β) : forIn o b f = o.elim (pure b) fun a => ForInStep.value <$> f a b
• Option.forIn_pure_yield_eq_elim 📋 Init.Data.Option.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] (o : Option α) (f : α → β → β) (b : β) : (forIn o b fun a b => pure (ForInStep.yield (f a b))) = pure (o.elim b fun a => f a b)
• Option.forIn_map 📋 Init.Data.Option.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {init : γ} [Monad m] [LawfulMonad m] (o : Option α) (g : α → β) (f : β → γ → m (ForInStep γ)) : forIn (Option.map g o) init f = forIn o init fun a y => f (g a) y
• Option.forIn_yield_eq_elim 📋 Init.Data.Option.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β γ : Type u_1} [Monad m] [LawfulMonad m] (o : Option α) (f : α → β → m γ) (g : α → β → γ → β) (b : β) : (forIn o b fun a b => (fun c => ForInStep.yield (g a b c)) <$> f a b) = o.elim (pure b) fun a => g a b <$> f a b
• Option.forIn_join 📋 Init.Data.Option.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} [Monad m] [LawfulMonad m] (o : Option (Option α)) (f : α → β → m (ForInStep β)) : forIn o.join init f = forIn o init fun o' b => ForInStep.yield <$> forIn o' b f
• Option.forIn'_join 📋 Init.Data.Option.Monadic
  {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] [LawfulMonad m] (b : β) (o : Option (Option α)) (f : (a : α) → a ∈ o.join → β → m (ForInStep β)) : forIn' o.join b f = forIn' o b fun o' ho' b => ForInStep.yield <$> forIn' o' b fun a ha b' => f a ⋯ b'
• Vector.idRun_forIn_yield_eq_foldl 📋 Init.Data.Vector.Monadic
  {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} (f : α → β → Id β) (init : β) : (forIn xs init fun a b => ForInStep.yield <$> f a b).run = Vector.foldl (fun b a => (f a b).run) init xs
• Vector.forIn_pure_yield_eq_foldl 📋 Init.Data.Vector.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Vector α n} (f : α → β → β) (init : β) : (forIn xs init fun a b => pure (ForInStep.yield (f a b))) = pure (Vector.foldl (fun b a => f a b) init xs)
• Vector.forIn_map 📋 Init.Data.Vector.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_4} {γ : Type u_1} {init : γ} [Monad m] [LawfulMonad m] {xs : Vector α n} (g : α → β) (f : β → γ → m (ForInStep γ)) : forIn (Vector.map g xs) init f = forIn xs init fun a y => f (g a) y
• Vector.forIn_yield_eq_foldlM 📋 Init.Data.Vector.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β γ : Type u_1} [Monad m] [LawfulMonad m] {xs : Vector α n} (f : α → β → m γ) (g : α → β → γ → β) (init : β) : (forIn xs init fun a b => (fun c => ForInStep.yield (g a b c)) <$> f a b) = Vector.foldlM (fun b a => g a b <$> f a b) init xs
• Vector.forIn_eq_foldlM 📋 Init.Data.Vector.Monadic
  {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [Monad m] [LawfulMonad m] {xs : Vector α n} (f : α → β → m (ForInStep β)) (init : β) : forIn xs init f = ForInStep.value <$> Vector.foldlM (fun b a => match b with | ForInStep.yield b => f a b | ForInStep.done b => pure (ForInStep.done b)) (ForInStep.yield init) xs
• Lean.Order.Array.monotone_forIn 📋 Init.Internal.Order.Lemmas
  {m : Type u → Type v} [Monad m] [(α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m] {β : Type u} {γ : Type w} [Lean.Order.PartialOrder γ] {α : Type uu} (as : Array α) (init : β) (f : γ → α → β → m (ForInStep β)) (hmono : Lean.Order.monotone f) : Lean.Order.monotone fun x => forIn as init (f x)
• Lean.Order.List.monotone_forIn 📋 Init.Internal.Order.Lemmas
  {m : Type u → Type v} [Monad m] [(α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m] {β : Type u} {γ : Type w} [Lean.Order.PartialOrder γ] {α : Type uu} (as : List α) (init : β) (f : γ → α → β → m (ForInStep β)) (hmono : Lean.Order.monotone f) : Lean.Order.monotone fun x => forIn as init (f x)
• Std.DHashMap.Internal.Raw.Const.unitOfArray_eq 📋 Std.Data.DHashMap.Internal.Raw
  {α : Type u} [BEq α] [Hashable α] {a : Array α} : Std.DHashMap.Raw.Const.unitOfArray a = ↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity a)
• Std.DHashMap.Internal.Raw.Const.unitOfList_eq 📋 Std.Data.DHashMap.Internal.Raw
  {α : Type u} [BEq α] [Hashable α] {l : List α} : Std.DHashMap.Raw.Const.unitOfList l = ↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)
• Std.DHashMap.Internal.Raw.Const.ofArray_eq 📋 Std.Data.DHashMap.Internal.Raw
  {α : Type u} {β : Type v} [BEq α] [Hashable α] {a : Array (α × β)} : Std.DHashMap.Raw.Const.ofArray a = ↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity a)
• Std.DHashMap.Internal.Raw.Const.ofList_eq 📋 Std.Data.DHashMap.Internal.Raw
  {α : Type u} {β : Type v} [BEq α] [Hashable α] {l : List (α × β)} : Std.DHashMap.Raw.Const.ofList l = ↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)
• Std.DHashMap.Internal.Raw.ofArray_eq 📋 Std.Data.DHashMap.Internal.Raw
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {a : Array ((a : α) × β a)} : Std.DHashMap.Raw.ofArray a = ↑↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany a)
• Std.DHashMap.Internal.Raw.ofList_eq 📋 Std.Data.DHashMap.Internal.Raw
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {l : List ((a : α) × β a)} : Std.DHashMap.Raw.ofList l = ↑↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)
• Std.Internal.List.forIn_eq_forIn_keys 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : α → Type v} {δ : Type w} {m' : Type w → Type w'} [Monad m'] [LawfulMonad m'] {f : α → δ → m' (ForInStep δ)} {init : δ} {l : List ((a : α) × β a)} : (forIn l init fun a d => f a.fst d) = forIn (Std.Internal.List.keys l) init f
• Std.Internal.List.forIn_eq_forIn_toProd 📋 Std.Data.Internal.List.Associative
  {α : Type u} {β : Type v} {δ : Type w} {m' : Type w → Type w'} [Monad m'] [LawfulMonad m'] {l : List ((_ : α) × β)} {f : α → β → δ → m' (ForInStep δ)} {init : δ} : (forIn l init fun a d => f a.fst a.snd d) = forIn (List.map (fun x => (x.fst, x.snd)) l) init fun a d => f a.1 a.2 d
• Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_eq_insertListIfNewUnitₘ 📋 Std.Data.DHashMap.Internal.Model
  {α : Type u} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) (l : List α) : ↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l) = Std.DHashMap.Internal.Raw₀.Const.insertListIfNewUnitₘ m l
• Std.DHashMap.Internal.Raw₀.Const.insertMany_eq_insertListₘ 📋 Std.Data.DHashMap.Internal.Model
  {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (l : List (α × β)) : ↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l) = Std.DHashMap.Internal.Raw₀.Const.insertListₘ m l
• Std.DHashMap.Internal.Raw₀.insertManyIfNew_eq_insertListIfNewₘ 📋 Std.Data.DHashMap.Internal.Model
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (l : List ((a : α) × β a)) : ↑(m.insertManyIfNew l) = m.insertListIfNewₘ l
• Std.DHashMap.Internal.Raw₀.insertMany_eq_insertListₘ 📋 Std.Data.DHashMap.Internal.Model
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (l : List ((a : α) × β a)) : ↑(m.insertMany l) = m.insertListₘ l
• Std.DHashMap.Internal.Raw₀.eraseManyEntries_eq_eraseListₘ 📋 Std.Data.DHashMap.Internal.Model
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (l : List ((a : α) × β a)) : ↑(m.eraseManyEntries l) = m.eraseListₘ (List.map (fun x => x.fst) l)
• Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_array_eq_insertManyIfNewUnit_toList 📋 Std.Data.DHashMap.Internal.WF
  {α : Type u} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) (a : Array α) : Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m a = Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m a.toList
• Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_list_eq_foldl 📋 Std.Data.DHashMap.Internal.WF
  {α : Type u} [BEq α] [Hashable α] {m : Std.DHashMap.Internal.Raw₀ α fun x => Unit} {l : List α} : ↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l) = List.foldl (fun a b => a.insertIfNew b ()) m l
• Std.DHashMap.Internal.Raw.forIn_eq_forIn_toListModel 📋 Std.Data.DHashMap.Internal.WF
  {α : Type u} {β : α → Type v} {δ : Type w} {l : Std.DHashMap.Raw α β} {m : Type w → Type w'} [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m (ForInStep δ)} {init : δ} : Std.DHashMap.Raw.forIn f init l = forIn (Std.DHashMap.Internal.toListModel l.buckets) init fun a d => f a.fst a.snd d
• Std.DHashMap.Internal.Raw₀.Const.insertMany_list_eq_foldl 📋 Std.Data.DHashMap.Internal.WF
  {α : Type u} {β : Type v} [BEq α] [Hashable α] {m : Std.DHashMap.Internal.Raw₀ α fun x => β} {l : List (α × β)} : ↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l) = List.foldl (fun a b => a.insert b.1 b.2) m l
• Std.DHashMap.Internal.Raw₀.Const.insertMany_array_eq_insertMany_toList 📋 Std.Data.DHashMap.Internal.WF
  {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (a : Array (α × β)) : Std.DHashMap.Internal.Raw₀.Const.insertMany m a = Std.DHashMap.Internal.Raw₀.Const.insertMany m a.toList
• Std.DHashMap.Internal.Raw₀.insertManyIfNew_list_eq_foldl 📋 Std.Data.DHashMap.Internal.WF
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Std.DHashMap.Internal.Raw₀ α β} {l : List ((a : α) × β a)} : ↑(m.insertManyIfNew l) = List.foldl (fun a b => a.insertIfNew b.fst b.snd) m l
• Std.DHashMap.Internal.Raw₀.insertMany_list_eq_foldl 📋 Std.Data.DHashMap.Internal.WF
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {m : Std.DHashMap.Internal.Raw₀ α β} {l : List ((a : α) × β a)} : ↑(m.insertMany l) = List.foldl (fun a b => a.insert b.fst b.snd) m l
• Std.DHashMap.Internal.Raw₀.insertMany_array_eq_insertMany_toList 📋 Std.Data.DHashMap.Internal.WF
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : Array ((k : α) × β k)) : m.insertMany a = m.insertMany a.toList
• Std.DHashMap.Internal.Raw₀.Const.toListModel_insertManyIfNewUnit_list 📋 Std.Data.DHashMap.Internal.WF
  {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Std.DHashMap.Internal.Raw₀ α fun x => Unit} {l : List α} (h : Std.DHashMap.Internal.Raw.WFImp ↑m) : (Std.DHashMap.Internal.toListModel (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).buckets).Perm (Std.Internal.List.insertListIfNewUnit (Std.DHashMap.Internal.toListModel (↑m).buckets) l)
• Std.DHashMap.Internal.Raw₀.toListModel_insertManyIfNew_list 📋 Std.Data.DHashMap.Internal.WF
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Std.DHashMap.Internal.Raw₀ α β} {l : List ((a : α) × β a)} (h : Std.DHashMap.Internal.Raw.WFImp ↑m) : (Std.DHashMap.Internal.toListModel (↑↑(m.insertManyIfNew l)).buckets).Perm (Std.Internal.List.insertListIfNew (Std.DHashMap.Internal.toListModel (↑m).buckets) l)
• Std.DHashMap.Internal.Raw₀.toListModel_insertMany_list 📋 Std.Data.DHashMap.Internal.WF
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Std.DHashMap.Internal.Raw₀ α β} {l : List ((a : α) × β a)} (h : Std.DHashMap.Internal.Raw.WFImp ↑m) : (Std.DHashMap.Internal.toListModel (↑↑(m.insertMany l)).buckets).Perm (Std.Internal.List.insertList (Std.DHashMap.Internal.toListModel (↑m).buckets) l)
• Std.DHashMap.Internal.Raw₀.Const.toListModel_insertMany_list 📋 Std.Data.DHashMap.Internal.WF
  {α : Type u} {β : Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Std.DHashMap.Internal.Raw₀ α fun x => β} {l : List (α × β)} (h : Std.DHashMap.Internal.Raw.WFImp ↑m) : (Std.DHashMap.Internal.toListModel (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).buckets).Perm (Std.Internal.List.insertListConst (Std.DHashMap.Internal.toListModel (↑m).buckets) l)
• Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_nil 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) : ↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m []) = m
• Std.DHashMap.Internal.Raw₀.Const.get!_insertManyIfNewUnit_list 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) {l : List α} {k : α} : Std.DHashMap.Internal.Raw₀.Const.get! (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)) k = ()
• Std.DHashMap.Internal.Raw₀.Const.getD_insertManyIfNewUnit_list 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) {l : List α} {k : α} {fallback : Unit} : Std.DHashMap.Internal.Raw₀.Const.getD (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)) k fallback = ()
• Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_list_singleton 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) {k : α} : ↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m [k]) = m.insertIfNew k ()
• Std.DHashMap.Internal.Raw₀.Const.get!_insertManyIfNewUnit_emptyWithCapacity_list 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {l : List α} {k : α} : Std.DHashMap.Internal.Raw₀.Const.get! (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)) k = ()
• Std.DHashMap.Internal.Raw₀.Const.insertMany_nil 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) : ↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m []) = m
• Std.DHashMap.Internal.Raw₀.Const.getD_insertManyIfNewUnit_emptyWithCapacity_list 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {l : List α} {k : α} {fallback : Unit} : Std.DHashMap.Internal.Raw₀.Const.getD (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)) k fallback = ()
• Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_nil 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] : ↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity []) = Std.DHashMap.Internal.Raw₀.emptyWithCapacity
• Std.DHashMap.Internal.Raw₀.insertMany_nil 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] : ↑(m.insertMany []) = m
• Std.DHashMap.Internal.Raw₀.Const.contains_insertManyIfNewUnit_emptyWithCapacity_list 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).contains k = l.contains k
• Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_singleton 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {k : α} : ↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity [k]) = Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertIfNew k ()
• Std.DHashMap.Internal.Raw₀.Const.getKey?_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} (h' : l.contains k = false) : (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).getKey? k = none
• Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α} (h' : l.contains k = false) : (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).getKeyD k fallback = fallback
• Std.DHashMap.Internal.Raw₀.forIn_eq_forIn_keys 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {m' : Type w → Type w'} [Monad m'] [LawfulMonad m'] {f : α → δ → m' (ForInStep δ)} {init : δ} : Std.DHashMap.Raw.forIn (fun a x d => f a d) init ↑m = forIn (↑m).keys init f
• Std.DHashMap.Internal.Raw₀.forIn_eq_forIn_keysArray 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {m' : Type w → Type w'} [Monad m'] [LawfulMonad m'] {f : α → δ → m' (ForInStep δ)} {init : δ} : Std.DHashMap.Raw.forIn (fun a x d => f a d) init ↑m = forIn (↑m).keysArray init f
• Std.DHashMap.Internal.Raw₀.Const.insertMany_list_singleton 📋 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.insertMany m [(k, v)]) = m.insert k v
• Std.DHashMap.Internal.Raw₀.Const.getKey!_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k : α} (h' : l.contains k = false) : (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).getKey! k = default
• Std.DHashMap.Internal.Raw₀.Const.insertMany_emptyWithCapacity_list_nil 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} : ↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity []) = Std.DHashMap.Internal.Raw₀.emptyWithCapacity
• Std.DHashMap.Internal.Raw₀.insertMany_emptyWithCapacity_list_nil 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] : ↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany []) = Std.DHashMap.Internal.Raw₀.emptyWithCapacity
• Std.DHashMap.Internal.Raw₀.Const.get?_insertManyIfNewUnit_emptyWithCapacity_list 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : Std.DHashMap.Internal.Raw₀.Const.get? (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)) k = if l.contains k = true then some () else none
• Std.DHashMap.Internal.Raw₀.Const.isEmpty_insertManyIfNewUnit_emptyWithCapacity_list 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} : (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).isEmpty = l.isEmpty
• Std.DHashMap.Internal.Raw₀.Const.size_insertManyIfNewUnit_emptyWithCapacity_list_le 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} : (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).size ≤ l.length
• Std.DHashMap.Internal.Raw₀.insertMany_list_singleton 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [BEq α] [Hashable α] {k : α} {v : β k} : ↑(m.insertMany [⟨k, v⟩]) = m.insert k v
• Std.DHashMap.Internal.Raw₀.Const.contains_insertMany_emptyWithCapacity_list 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} : (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).contains k = (List.map Prod.fst l).contains k
• Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertManyIfNewUnit_emptyWithCapacity_list_of_mem 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k k' fallback : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun a b => (a == b) = false) l) (mem : k ∈ l) : (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).getKeyD k' fallback = k
• Std.DHashMap.Internal.Raw₀.Const.insertMany_emptyWithCapacity_list_singleton 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} {k : α} {v : β} : ↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity [(k, v)]) = Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insert k v
• Std.DHashMap.Internal.Raw₀.Const.getKey!_insertManyIfNewUnit_emptyWithCapacity_list_of_mem 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List α} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun a b => (a == b) = false) l) (mem : k ∈ l) : (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).getKey! k' = k
• Std.DHashMap.Internal.Raw₀.Const.getKey?_insertManyIfNewUnit_emptyWithCapacity_list_of_mem 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α} (k_beq : (k == k') = true) (distinct : List.Pairwise (fun a b => (a == b) = false) l) (mem : k ∈ l) : (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).getKey? k' = some k
• Std.DHashMap.Internal.Raw₀.Const.contains_insertManyIfNewUnit_list 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {l : List α} {k : α} : (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).contains k = (m.contains k || l.contains k)
• Std.DHashMap.Internal.Raw₀.Const.get?_insertMany_emptyWithCapacity_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (h : (List.map Prod.fst l).contains k = false) : Std.DHashMap.Internal.Raw₀.Const.get? (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)) k = none
• Std.DHashMap.Internal.Raw₀.Const.getD_insertMany_emptyWithCapacity_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} {fallback : β} (contains_eq_false : (List.map Prod.fst l).contains k = false) : Std.DHashMap.Internal.Raw₀.Const.getD (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)) k fallback = fallback
• Std.DHashMap.Internal.Raw₀.Const.getKey?_insertMany_emptyWithCapacity_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} (h : (List.map Prod.fst l).contains k = false) : (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).getKey? k = none
• Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertMany_emptyWithCapacity_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k fallback : α} (h : (List.map Prod.fst l).contains k = false) : (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).getKeyD k fallback = fallback
• Std.DHashMap.Internal.Raw₀.Const.get!_insertMany_emptyWithCapacity_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α} [Inhabited β] (h : (List.map Prod.fst l).contains k = false) : Std.DHashMap.Internal.Raw₀.Const.get! (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)) k = default
• Std.DHashMap.Internal.Raw₀.Const.size_insertManyIfNewUnit_emptyWithCapacity_list 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} (distinct : List.Pairwise (fun a b => (a == b) = false) l) : (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).size = l.length
• Std.DHashMap.Internal.Raw₀.Const.getKey!_insertMany_emptyWithCapacity_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List (α × β)} {k : α} (h : (List.map Prod.fst l).contains k = false) : (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).getKey! k = default
• Std.DHashMap.Internal.Raw₀.Const.contains_of_contains_insertManyIfNewUnit_list 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {l : List α} {k : α} (h₂ : l.contains k = false) : (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).contains k = true → m.contains k = true
• Std.DHashMap.Internal.Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {l : List α} {k : α} : m.contains k = true → (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).getKey? k = m.getKey? k
• Std.DHashMap.Internal.Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {l : List α} {k : α} : m.contains k = false → l.contains k = false → (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).getKey? k = none
• Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {l : List α} {k fallback : α} : m.contains k = true → (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).getKeyD k fallback = m.getKeyD k fallback
• Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {l : List α} {k fallback : α} : m.contains k = false → l.contains k = false → (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).getKeyD k fallback = fallback
• Std.DHashMap.Internal.Raw₀.contains_insertMany_emptyWithCapacity_list 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k : α} : (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).contains k = (List.map Sigma.fst l).contains k
• Std.DHashMap.Internal.Raw₀.Const.forIn_eq_forIn_toArray 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {δ : Type w} {m' : Type w → Type w'} {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [Monad m'] [LawfulMonad m'] {f : α → β → δ → m' (ForInStep δ)} {init : δ} : Std.DHashMap.Raw.forIn f init ↑m = forIn (Std.DHashMap.Raw.Const.toArray ↑m) init fun a b => f a.1 a.2 b
• Std.DHashMap.Internal.Raw₀.Const.forIn_eq_forIn_toList 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {δ : Type w} {m' : Type w → Type w'} {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [Monad m'] [LawfulMonad m'] {f : α → β → δ → m' (ForInStep δ)} {init : δ} : Std.DHashMap.Raw.forIn f init ↑m = forIn (Std.DHashMap.Raw.Const.toList ↑m) init fun a b => f a.1 a.2 b
• Std.DHashMap.Internal.Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : (↑m).WF) {l : List α} {k : α} : m.contains k = true → (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).getKey! k = m.getKey! k
• Std.DHashMap.Internal.Raw₀.insertMany_emptyWithCapacity_list_singleton 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {k : α} {v : β k} : ↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany [⟨k, v⟩]) = Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insert k v
• Std.DHashMap.Internal.Raw₀.Const.isEmpty_insertMany_emptyWithCapacity_list 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} : (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).isEmpty = l.isEmpty
• Std.DHashMap.Internal.Raw₀.Const.getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : (↑m).WF) {l : List α} {k : α} : m.contains k = false → l.contains k = false → (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).getKey! k = default
• Std.DHashMap.Internal.Raw₀.Const.size_insertMany_emptyWithCapacity_list_le 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} : (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).size ≤ l.length
• Std.DHashMap.Internal.Raw₀.get?_insertMany_emptyWithCapacity_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} (h : (List.map Sigma.fst l).contains k = false) : (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).get? k = none
• Std.DHashMap.Internal.Raw₀.getD_insertMany_emptyWithCapacity_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} {fallback : β k} (contains_eq_false : (List.map Sigma.fst l).contains k = false) : (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).getD k fallback = fallback
• Std.DHashMap.Internal.Raw₀.getKey?_insertMany_emptyWithCapacity_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k : α} (h : (List.map Sigma.fst l).contains k = false) : (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).getKey? k = none
• Std.DHashMap.Internal.Raw₀.getKeyD_insertMany_emptyWithCapacity_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} {k fallback : α} (h : (List.map Sigma.fst l).contains k = false) : (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).getKeyD k fallback = fallback
• Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_list_equiv_foldl 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] (m₁ : Std.DHashMap.Internal.Raw₀ α fun x => Unit) {l : List α} : (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m₁ l)).Equiv (List.foldl (fun acc a => acc.insertIfNew a ()) (↑m₁) l)
• Std.DHashMap.Internal.Raw₀.Const.get_insertManyIfNewUnit_list 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) {l : List α} {k : α} {h : (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).contains k = true} : Std.DHashMap.Internal.Raw₀.Const.get (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)) k h = ()
• Std.DHashMap.Internal.Raw₀.get!_insertMany_emptyWithCapacity_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] (h : (List.map Sigma.fst l).contains k = false) : (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).get! k = default
• Std.DHashMap.Internal.Raw₀.getKey!_insertMany_emptyWithCapacity_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] [Inhabited α] {l : List ((a : α) × β a)} {k : α} (h : (List.map Sigma.fst l).contains k = false) : (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).getKey! k = default
• Std.DHashMap.Internal.Raw₀.isEmpty_insertMany_emptyWithCapacity_list 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} : (↑↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).isEmpty = l.isEmpty
• Std.DHashMap.Internal.Raw₀.size_insertMany_emptyWithCapacity_list_le 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} : (↑↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).size ≤ l.length
• Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_cons 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) {l : List α} {k : α} : ↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m (k :: l)) = ↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit (m.insertIfNew k ()) l)
• Std.DHashMap.Internal.Raw₀.forIn_eq_forIn_toArray 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {m' : Type w → Type w'} [Monad m'] [LawfulMonad m'] {f : (a : α) → β a → δ → m' (ForInStep δ)} {init : δ} : Std.DHashMap.Raw.forIn f init ↑m = forIn (↑m).toArray init fun a b => f a.fst a.snd b
• Std.DHashMap.Internal.Raw₀.forIn_eq_forIn_toList 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {m' : Type w → Type w'} [Monad m'] [LawfulMonad m'] {f : (a : α) → β a → δ → m' (ForInStep δ)} {init : δ} : Std.DHashMap.Raw.forIn f init ↑m = forIn (↑m).toList init fun a b => f a.fst a.snd b
• Std.DHashMap.Internal.Raw₀.Const.contains_insertMany_list 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {l : List (α × β)} {k : α} : (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).contains k = (m.contains k || (List.map Prod.fst l).contains k)
• Std.DHashMap.Internal.Raw₀.Const.get?_insertMany_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {l : List (α × β)} {k : α} (h' : (List.map Prod.fst l).contains k = false) : Std.DHashMap.Internal.Raw₀.Const.get? (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)) k = Std.DHashMap.Internal.Raw₀.Const.get? m k
• Std.DHashMap.Internal.Raw₀.Const.getD_insertMany_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {l : List (α × β)} {k : α} {fallback : β} (h' : (List.map Prod.fst l).contains k = false) : Std.DHashMap.Internal.Raw₀.Const.getD (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)) k fallback = Std.DHashMap.Internal.Raw₀.Const.getD m k fallback
• Std.DHashMap.Internal.Raw₀.Const.getKey?_insertMany_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {l : List (α × β)} {k : α} (h' : (List.map Prod.fst l).contains k = false) : (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).getKey? k = m.getKey? k
• Std.DHashMap.Internal.Raw₀.Const.get!_insertMany_list_of_contains_eq_false 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : (↑m).WF) {l : List (α × β)} {k : α} (h' : (List.map Prod.fst l).contains k = false) : Std.DHashMap.Internal.Raw₀.Const.get! (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)) k = Std.DHashMap.Internal.Raw₀.Const.get! m k
• Std.DHashMap.Internal.Raw₀.Const.getKeyD_insertManyIfNewUnit_list_of_contains_eq_false_of_mem 📋 Std.Data.DHashMap.Internal.RawLemmas
  {α : Type u} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α] [LawfulHashable α] (h : (↑m).WF) {l : List α} {k k' fallback : α} (k_beq : (k == k') = true) : m.contains k = false → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).getKeyD k' fallback = k

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. 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.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

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. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 01cceef