-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem foldrM_subtype [Monad m] [LawfulMonad m]{p : α → Prop} {l : List { x // p x }}
    {f : { x // p x } → β → m β} {g : α → β → m β} {x : β}
    (hf : ∀ x h b, f ⟨x, h⟩ b = g x b) :
    l.foldrM f x = l.unattach.foldrM g x

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
f : { x // p x } → β → m β
g : α → β → m β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
a : { x // p x }
l : List { x // p x }
ih : ∀ {x : β}, foldrM f x l = foldrM g x (map (fun x => x.val) l)
x : β
⊢ foldrM g x l.unattach >>= f a = foldrM g x l.unattach >>= g a.val

Tactic:
congr

Result:
case cons.e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
f : { x // p x } → β → m β
g : α → β → m β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
a : { x // p x }
l : List { x // p x }
ih : ∀ {x : β}, foldrM f x l = foldrM g x (map (fun x => x.val) l)
x : β
⊢ f a = g a.val

Proof state:
case cons.e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
f : { x // p x } → β → m β
g : α → β → m β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
a : { x // p x }
l : List { x // p x }
ih : ∀ {x : β}, foldrM f x l = foldrM g x (map (fun x => x.val) l)
x : β
⊢ f a = g a.val

Tactic:
funext b

Result:
case cons.e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
f : { x // p x } → β → m β
g : α → β → m β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
a : { x // p x }
l : List { x // p x }
ih : ∀ {x : β}, foldrM f x l = foldrM g x (map (fun x => x.val) l)
x b : β
⊢ f a b = g a.val b

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
l : List { x // p x }
f : { x // p x } → β → m β
g : α → β → m β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
⊢ foldrM f x l = foldrM g x l.unattach

Tactic:
unfold unattach

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
l : List { x // p x }
f : { x // p x } → β → m β
g : α → β → m β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
⊢ foldrM f x l = foldrM g x (map (fun x => x.val) l)

Proof state:
case nil
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
f : { x // p x } → β → m β
g : α → β → m β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
x : β
⊢ foldrM f x [] = foldrM g x (map (fun x => x.val) [])

Tactic:
simp

Result:
no goals

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
f : { x // p x } → β → m β
g : α → β → m β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
a : { x // p x }
l : List { x // p x }
ih : ∀ {x : β}, foldrM f x l = foldrM g x (map (fun x => x.val) l)
x : β
⊢ foldrM f x (a :: l) = foldrM g x (map (fun x => x.val) (a :: l))

Tactic:
simp [ih, hf, foldrM_cons]

Result:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
f : { x // p x } → β → m β
g : α → β → m β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
a : { x // p x }
l : List { x // p x }
ih : ∀ {x : β}, foldrM f x l = foldrM g x (map (fun x => x.val) l)
x : β
⊢ foldrM g x l.unattach >>= f a = foldrM g x l.unattach >>= g a.val

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
l : List { x // p x }
f : { x // p x } → β → m β
g : α → β → m β
x : β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
⊢ foldrM f x l = foldrM g x (map (fun x => x.val) l)

Tactic:
induction l generalizing x with
| nil => simp
| cons a l ih =>
  simp [ih, hf, foldrM_cons]
  congr
  funext b
  simp [hf]

Result:
no goals

Proof state:
case cons.e_a.h
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Prop
f : { x // p x } → β → m β
g : α → β → m β
hf : ∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b
a : { x // p x }
l : List { x // p x }
ih : ∀ {x : β}, foldrM f x l = foldrM g x (map (fun x => x.val) l)
x b : β
⊢ f a b = g a.val b

Tactic:
simp [hf]

Result:
no goals