-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Monadic.lean
theorem forIn'_congr [Monad m] [LawfulMonad m] {as bs : Option α} (w : as = bs)
    {b b' : β} (hb : b = b')
    {f : (a' : α) → a' ∈ as → β → m (ForInStep β)}
    {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)}
    (h : ∀ a m b, f a (by simpa [w] using m) b = g a m b) :
    forIn' as b f = forIn' bs b' g

Proof state:
case some.none
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
b b' : β
hb : b = b'
val✝ : α
f : (a' : α) → a' ∈ some val✝ → β → m (ForInStep β)
g : (a' : α) → a' ∈ none → β → m (ForInStep β)
w : some val✝ = none
h : ∀ (a : α) (m_1 : a ∈ none) (b : β), f a ⋯ b = g a m_1 b
⊢ forIn' (some val✝) b f = forIn' none b' g

Tactic:
simp at w

Result:
no goals

Proof state:
m✝ : Type ?u.940 → Type ?u.851
α : Type ?u.867
β : Type ?u.940
inst✝¹ : Monad m✝
inst✝ : LawfulMonad m✝
as bs : Option α
w : as = bs
b✝ b' : β
hb : b✝ = b'
f : (a' : α) → a' ∈ as → β → m✝ (ForInStep β)
g : (a' : α) → a' ∈ bs → β → m✝ (ForInStep β)
a : α
m : a ∈ bs
b : β
⊢ a ∈ as

Tactic:
simpa [w] using m

Result:
no goals

Proof state:
case none.some
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
b b' : β
hb : b = b'
f : (a' : α) → a' ∈ none → β → m (ForInStep β)
val✝ : α
g : (a' : α) → a' ∈ some val✝ → β → m (ForInStep β)
w : none = some val✝
h : ∀ (a : α) (m_1 : a ∈ some val✝) (b : β), f a ⋯ b = g a m_1 b
⊢ forIn' none b f = forIn' (some val✝) b' g

Tactic:
simp at w

Result:
no goals

Proof state:
case none.none
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
b b' : β
hb : b = b'
f g : (a' : α) → a' ∈ none → β → m (ForInStep β)
w : none = none
h : ∀ (a : α) (m_1 : a ∈ none) (b : β), f a ⋯ b = g a m_1 b
⊢ forIn' none b f = forIn' none b' g

Tactic:
simp [hb]

Result:
no goals

Proof state:
case some.some
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
b b' : β
hb : b = b'
val✝¹ : α
f : (a' : α) → a' ∈ some val✝¹ → β → m (ForInStep β)
val✝ : α
g : (a' : α) → a' ∈ some val✝ → β → m (ForInStep β)
w✝ : some val✝¹ = some val✝
h : ∀ (a : α) (m_1 : a ∈ some val✝) (b : β), f a ⋯ b = g a m_1 b
w : val✝¹ = val✝
⊢ forIn' (some val✝¹) b f = forIn' (some val✝) b' g

Tactic:
subst w

Result:
case some.some
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
b b' : β
hb : b = b'
val✝ : α
f g : (a' : α) → a' ∈ some val✝ → β → m (ForInStep β)
w : some val✝ = some val✝
h : ∀ (a : α) (m_1 : a ∈ some val✝) (b : β), f a ⋯ b = g a m_1 b
⊢ forIn' (some val✝) b f = forIn' (some val✝) b' g

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as bs : Option α
w : as = bs
b b' : β
hb : b = b'
f : (a' : α) → a' ∈ as → β → m (ForInStep β)
g : (a' : α) → a' ∈ bs → β → m (ForInStep β)
h : ∀ (a : α) (m_1 : a ∈ bs) (b : β), f a ⋯ b = g a m_1 b
⊢ forIn' as b f = forIn' bs b' g

Tactic:
cases as <;> cases bs

Result:
case none.none
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
b b' : β
hb : b = b'
f g : (a' : α) → a' ∈ none → β → m (ForInStep β)
w : none = none
h : ∀ (a : α) (m_1 : a ∈ none) (b : β), f a ⋯ b = g a m_1 b
⊢ forIn' none b f = forIn' none b' g

case none.some
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
b b' : β
hb : b = b'
f : (a' : α) → a' ∈ none → β → m (ForInStep β)
val✝ : α
g : (a' : α) → a' ∈ some val✝ → β → m (ForInStep β)
w : none = some val✝
h : ∀ (a : α) (m_1 : a ∈ some val✝) (b : β), f a ⋯ b = g a m_1 b
⊢ forIn' none b f = forIn' (some val✝) b' g

case some.none
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
b b' : β
hb : b = b'
val✝ : α
f : (a' : α) → a' ∈ some val✝ → β → m (ForInStep β)
g : (a' : α) → a' ∈ none → β → m (ForInStep β)
w : some val✝ = none
h : ∀ (a : α) (m_1 : a ∈ none) (b : β), f a ⋯ b = g a m_1 b
⊢ forIn' (some val✝) b f = forIn' none b' g

case some.some
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
b b' : β
hb : b = b'
val✝¹ : α
f : (a' : α) → a' ∈ some val✝¹ → β → m (ForInStep β)
val✝ : α
g : (a' : α) → a' ∈ some val✝ → β → m (ForInStep β)
w : some val✝¹ = some val✝
h : ∀ (a : α) (m_1 : a ∈ some val✝) (b : β), f a ⋯ b = g a m_1 b
⊢ forIn' (some val✝¹) b f = forIn' (some val✝) b' g

Proof state:
case some.some
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
b b' : β
hb : b = b'
val✝¹ : α
f : (a' : α) → a' ∈ some val✝¹ → β → m (ForInStep β)
val✝ : α
g : (a' : α) → a' ∈ some val✝ → β → m (ForInStep β)
w : some val✝¹ = some val✝
h : ∀ (a : α) (m_1 : a ∈ some val✝) (b : β), f a ⋯ b = g a m_1 b
⊢ forIn' (some val✝¹) b f = forIn' (some val✝) b' g

Tactic:
simp only [some.injEq] at w

Result:
case some.some
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
b b' : β
hb : b = b'
val✝¹ : α
f : (a' : α) → a' ∈ some val✝¹ → β → m (ForInStep β)
val✝ : α
g : (a' : α) → a' ∈ some val✝ → β → m (ForInStep β)
w✝ : some val✝¹ = some val✝
h : ∀ (a : α) (m_1 : a ∈ some val✝) (b : β), f a ⋯ b = g a m_1 b
w : val✝¹ = val✝
⊢ forIn' (some val✝¹) b f = forIn' (some val✝) b' g

Proof state:
case some.some
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
b b' : β
hb : b = b'
val✝ : α
f g : (a' : α) → a' ∈ some val✝ → β → m (ForInStep β)
w : some val✝ = some val✝
h : ∀ (a : α) (m_1 : a ∈ some val✝) (b : β), f a ⋯ b = g a m_1 b
⊢ forIn' (some val✝) b f = forIn' (some val✝) b' g

Tactic:
simp [hb, h]

Result:
no goals