From e589d280c4c1016c4a93e0194df01bb7c43bb4f5 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 13 Nov 2024 11:01:31 +1100 Subject: [PATCH] chore: cleanup proof of satisfiesM_foldlM --- Batteries/Data/List/Monadic.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Batteries/Data/List/Monadic.lean b/Batteries/Data/List/Monadic.lean index 00eb213755..f0fa51e370 100644 --- a/Batteries/Data/List/Monadic.lean +++ b/Batteries/Data/List/Monadic.lean @@ -15,15 +15,13 @@ namespace List theorem satisfiesM_foldlM [Monad m] [LawfulMonad m] {f : β → α → m β} (h₀ : motive b) (h₁ : ∀ (b) (_ : motive b) (a : α) (_ : a ∈ l), SatisfiesM motive (f b a)) : SatisfiesM motive (List.foldlM f b l) := by - have g b hb a am := Classical.indefiniteDescription _ (h₁ b hb a am) - clear h₁ induction l generalizing b with | nil => exact SatisfiesM.pure h₀ | cons hd tl ih => simp only [foldlM_cons] apply SatisfiesM.bind_pre - let ⟨q, qh⟩ := g b h₀ hd (mem_cons_self hd tl) - exact ⟨(fun ⟨b, bh⟩ => ⟨b, ih bh (fun b bh a am => g b bh a (mem_cons_of_mem hd am))⟩) <$> q, + let ⟨q, qh⟩ := h₁ b h₀ hd (mem_cons_self hd tl) + exact ⟨(fun ⟨b, bh⟩ => ⟨b, ih bh (fun b bh a am => h₁ b bh a (mem_cons_of_mem hd am))⟩) <$> q, by simpa using qh⟩ theorem satisfiesM_foldrM [Monad m] [LawfulMonad m] {f : α → β → m β} (h₀ : motive b)