Theorem: LeanColls.Fold.foldM_eq_foldM_toList (LeanColls/Classes/Ops/Fold.lean)

State before:
C : Type u_3
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
m : Type u_1 → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
c : C
⊢ ∃ L, L.Perm (toList c) ∧ ∀ {β : Type u_1} (f : β → τ → m β) (init : β), foldM c f init = List.foldlM f init L
Tactic:
have ⟨L,perm,h⟩ := ToList.fold_eq_fold_toList c
State after:
C : Type u_3
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
m : Type u_1 → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
c : C
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ ∃ L, L.Perm (toList c) ∧ ∀ {β : Type u_1} (f : β → τ → m β) (init : β), foldM c f init = List.foldlM f init L

State before:
C : Type u_3
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
m : Type u_1 → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
c : C
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ ∃ L, L.Perm (toList c) ∧ ∀ {β : Type u_1} (f : β → τ → m β) (init : β), foldM c f init = List.foldlM f init L
Tactic:
use L
State after:
case h
C : Type u_3
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
m : Type u_1 → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
c : C
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ L.Perm (toList c) ∧ ∀ {β : Type u_1} (f : β → τ → m β) (init : β), foldM c f init = List.foldlM f init L

State before:
case h
C : Type u_3
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
m : Type u_1 → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
c : C
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ L.Perm (toList c) ∧ ∀ {β : Type u_1} (f : β → τ → m β) (init : β), foldM c f init = List.foldlM f init L
Tactic:
refine ⟨perm,?_⟩
State after:
case h
C : Type u_3
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
m : Type u_1 → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
c : C
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ ∀ {β : Type u_1} (f : β → τ → m β) (init : β), foldM c f init = List.foldlM f init L

State before:
case h
C : Type u_3
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
m : Type u_1 → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
c : C
L : List τ
perm : L.Perm (toList c)
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ ∀ {β : Type u_1} (f : β → τ → m β) (init : β), foldM c f init = List.foldlM f init L
Tactic:
clear perm
State after:
case h
C : Type u_3
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
m : Type u_1 → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
c : C
L : List τ
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ ∀ {β : Type u_1} (f : β → τ → m β) (init : β), foldM c f init = List.foldlM f init L

State before:
case h
C : Type u_3
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
m : Type u_1 → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
c : C
L : List τ
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
⊢ ∀ {β : Type u_1} (f : β → τ → m β) (init : β), foldM c f init = List.foldlM f init L
Tactic:
intro β f init
State after:
case h
C : Type u_3
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
m : Type u_1 → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
c : C
L : List τ
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
β : Type u_1
f : β → τ → m β
init : β
⊢ foldM c f init = List.foldlM f init L

State before:
case h
C : Type u_3
τ : Type u_2
inst✝⁴ : Fold C τ
inst✝³ : LeanColls.ToList C τ
inst✝² : ToList C τ
m : Type u_1 → Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
c : C
L : List τ
h : ∀ {β : Type u_1} (f : β → τ → β) (init : β), fold c f init = List.foldl f init L
β : Type u_1
f : β → τ → m β
init : β
⊢ foldM c f init = List.foldlM f init L
Tactic:
rw [ToList.foldM_eq_fold, h, List.foldlM_eq_foldl]
State after:
no goals