-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Basic.lean
theorem forIn'_eq_forIn [d : Membership α ρ] [ForIn' m ρ α d] {β} [Monad m] (x : ρ) (b : β)
    (f : (a : α) → a ∈ x → β → m (ForInStep β)) (g : (a : α) → β → m (ForInStep β))
    (h : ∀ a m b, f a m b = g a b) :
    forIn' x b f = forIn x b g

Proof state:
case e_f.h
α : Type u_1
ρ : Type u_2
m : Type u_3 → Type u_4
d : Membership α ρ
inst✝¹ : ForIn' m ρ α d
β : Type u_3
inst✝ : Monad m
x : ρ
b : β
f : (a : α) → a ∈ x → β → m (ForInStep β)
g : α → β → m (ForInStep β)
h : ∀ (a : α) (m_1 : a ∈ x) (b : β), f a m_1 b = g a b
a : α
⊢ f a = fun x => g a

Tactic:
apply funext

Result:
case e_f.h.h
α : Type u_1
ρ : Type u_2
m : Type u_3 → Type u_4
d : Membership α ρ
inst✝¹ : ForIn' m ρ α d
β : Type u_3
inst✝ : Monad m
x : ρ
b : β
f : (a : α) → a ∈ x → β → m (ForInStep β)
g : α → β → m (ForInStep β)
h : ∀ (a : α) (m_1 : a ∈ x) (b : β), f a m_1 b = g a b
a : α
⊢ ∀ (x : a ∈ x), f a x = g a

Proof state:
case e_f.h.h.h
α : Type u_1
ρ : Type u_2
m✝ : Type u_3 → Type u_4
d : Membership α ρ
inst✝¹ : ForIn' m✝ ρ α d
β : Type u_3
inst✝ : Monad m✝
x : ρ
b✝ : β
f : (a : α) → a ∈ x → β → m✝ (ForInStep β)
g : α → β → m✝ (ForInStep β)
h : ∀ (a : α) (m : a ∈ x) (b : β), f a m b = g a b
a : α
m : a ∈ x
b : β
⊢ f a m b = g a b

Tactic:
simp [h]

Result:
case e_f.h.h.h
α : Type u_1
ρ : Type u_2
m✝ : Type u_3 → Type u_4
d : Membership α ρ
inst✝¹ : ForIn' m✝ ρ α d
β : Type u_3
inst✝ : Monad m✝
x : ρ
b✝ : β
f : (a : α) → a ∈ x → β → m✝ (ForInStep β)
g : α → β → m✝ (ForInStep β)
h : ∀ (a : α) (m : a ∈ x) (b : β), f a m b = g a b
a : α
m : a ∈ x
b : β
⊢ g a b = g a b

Proof state:
case e_f.h.h.h
α : Type u_1
ρ : Type u_2
m✝ : Type u_3 → Type u_4
d : Membership α ρ
inst✝¹ : ForIn' m✝ ρ α d
β : Type u_3
inst✝ : Monad m✝
x : ρ
b✝ : β
f : (a : α) → a ∈ x → β → m✝ (ForInStep β)
g : α → β → m✝ (ForInStep β)
h : ∀ (a : α) (m : a ∈ x) (b : β), f a m b = g a b
a : α
m : a ∈ x
b : β
⊢ g a b = g a b

Tactic:
rfl

Result:
no goals

Proof state:
case e_f.h.h
α : Type u_1
ρ : Type u_2
m : Type u_3 → Type u_4
d : Membership α ρ
inst✝¹ : ForIn' m ρ α d
β : Type u_3
inst✝ : Monad m
x : ρ
b : β
f : (a : α) → a ∈ x → β → m (ForInStep β)
g : α → β → m (ForInStep β)
h : ∀ (a : α) (m_1 : a ∈ x) (b : β), f a m_1 b = g a b
a : α
⊢ ∀ (x : a ∈ x), f a x = g a

Tactic:
intro m

Result:
case e_f.h.h
α : Type u_1
ρ : Type u_2
m✝ : Type u_3 → Type u_4
d : Membership α ρ
inst✝¹ : ForIn' m✝ ρ α d
β : Type u_3
inst✝ : Monad m✝
x : ρ
b : β
f : (a : α) → a ∈ x → β → m✝ (ForInStep β)
g : α → β → m✝ (ForInStep β)
h : ∀ (a : α) (m : a ∈ x) (b : β), f a m b = g a b
a : α
m : a ∈ x
⊢ f a m = g a

Proof state:
case e_f.h
α : Type u_1
ρ : Type u_2
m : Type u_3 → Type u_4
d : Membership α ρ
inst✝¹ : ForIn' m ρ α d
β : Type u_3
inst✝ : Monad m
x : ρ
b : β
f : (a : α) → a ∈ x → β → m (ForInStep β)
g : α → β → m (ForInStep β)
h : ∀ (a : α) (m_1 : a ∈ x) (b : β), f a m_1 b = g a b
⊢ ∀ (x_1 : α), f x_1 = fun x => g x_1

Tactic:
intro a

Result:
case e_f.h
α : Type u_1
ρ : Type u_2
m : Type u_3 → Type u_4
d : Membership α ρ
inst✝¹ : ForIn' m ρ α d
β : Type u_3
inst✝ : Monad m
x : ρ
b : β
f : (a : α) → a ∈ x → β → m (ForInStep β)
g : α → β → m (ForInStep β)
h : ∀ (a : α) (m_1 : a ∈ x) (b : β), f a m_1 b = g a b
a : α
⊢ f a = fun x => g a

Proof state:
α : Type u_1
ρ : Type u_2
m : Type u_3 → Type u_4
d : Membership α ρ
inst✝¹ : ForIn' m ρ α d
β : Type u_3
inst✝ : Monad m
x : ρ
b : β
f : (a : α) → a ∈ x → β → m (ForInStep β)
g : α → β → m (ForInStep β)
h : ∀ (a : α) (m_1 : a ∈ x) (b : β), f a m_1 b = g a b
⊢ forIn' x b f = forIn x b g

Tactic:
simp [instForInOfForIn']

Result:
α : Type u_1
ρ : Type u_2
m : Type u_3 → Type u_4
d : Membership α ρ
inst✝¹ : ForIn' m ρ α d
β : Type u_3
inst✝ : Monad m
x : ρ
b : β
f : (a : α) → a ∈ x → β → m (ForInStep β)
g : α → β → m (ForInStep β)
h : ∀ (a : α) (m_1 : a ∈ x) (b : β), f a m_1 b = g a b
⊢ forIn' x b f = forIn' x b fun a x => g a

Proof state:
case e_f
α : Type u_1
ρ : Type u_2
m : Type u_3 → Type u_4
d : Membership α ρ
inst✝¹ : ForIn' m ρ α d
β : Type u_3
inst✝ : Monad m
x : ρ
b : β
f : (a : α) → a ∈ x → β → m (ForInStep β)
g : α → β → m (ForInStep β)
h : ∀ (a : α) (m_1 : a ∈ x) (b : β), f a m_1 b = g a b
⊢ f = fun a x => g a

Tactic:
apply funext

Result:
case e_f.h
α : Type u_1
ρ : Type u_2
m : Type u_3 → Type u_4
d : Membership α ρ
inst✝¹ : ForIn' m ρ α d
β : Type u_3
inst✝ : Monad m
x : ρ
b : β
f : (a : α) → a ∈ x → β → m (ForInStep β)
g : α → β → m (ForInStep β)
h : ∀ (a : α) (m_1 : a ∈ x) (b : β), f a m_1 b = g a b
⊢ ∀ (x_1 : α), f x_1 = fun x => g x_1

Proof state:
case e_f.h.h.h
α : Type u_1
ρ : Type u_2
m✝ : Type u_3 → Type u_4
d : Membership α ρ
inst✝¹ : ForIn' m✝ ρ α d
β : Type u_3
inst✝ : Monad m✝
x : ρ
b : β
f : (a : α) → a ∈ x → β → m✝ (ForInStep β)
g : α → β → m✝ (ForInStep β)
h : ∀ (a : α) (m : a ∈ x) (b : β), f a m b = g a b
a : α
m : a ∈ x
⊢ ∀ (x : β), f a m x = g a x

Tactic:
intro b

Result:
case e_f.h.h.h
α : Type u_1
ρ : Type u_2
m✝ : Type u_3 → Type u_4
d : Membership α ρ
inst✝¹ : ForIn' m✝ ρ α d
β : Type u_3
inst✝ : Monad m✝
x : ρ
b✝ : β
f : (a : α) → a ∈ x → β → m✝ (ForInStep β)
g : α → β → m✝ (ForInStep β)
h : ∀ (a : α) (m : a ∈ x) (b : β), f a m b = g a b
a : α
m : a ∈ x
b : β
⊢ f a m b = g a b

Proof state:
α : Type u_1
ρ : Type u_2
m : Type u_3 → Type u_4
d : Membership α ρ
inst✝¹ : ForIn' m ρ α d
β : Type u_3
inst✝ : Monad m
x : ρ
b : β
f : (a : α) → a ∈ x → β → m (ForInStep β)
g : α → β → m (ForInStep β)
h : ∀ (a : α) (m_1 : a ∈ x) (b : β), f a m_1 b = g a b
⊢ forIn' x b f = forIn' x b fun a x => g a

Tactic:
congr

Result:
case e_f
α : Type u_1
ρ : Type u_2
m : Type u_3 → Type u_4
d : Membership α ρ
inst✝¹ : ForIn' m ρ α d
β : Type u_3
inst✝ : Monad m
x : ρ
b : β
f : (a : α) → a ∈ x → β → m (ForInStep β)
g : α → β → m (ForInStep β)
h : ∀ (a : α) (m_1 : a ∈ x) (b : β), f a m_1 b = g a b
⊢ f = fun a x => g a

Proof state:
case e_f.h.h
α : Type u_1
ρ : Type u_2
m✝ : Type u_3 → Type u_4
d : Membership α ρ
inst✝¹ : ForIn' m✝ ρ α d
β : Type u_3
inst✝ : Monad m✝
x : ρ
b : β
f : (a : α) → a ∈ x → β → m✝ (ForInStep β)
g : α → β → m✝ (ForInStep β)
h : ∀ (a : α) (m : a ∈ x) (b : β), f a m b = g a b
a : α
m : a ∈ x
⊢ f a m = g a

Tactic:
apply funext

Result:
case e_f.h.h.h
α : Type u_1
ρ : Type u_2
m✝ : Type u_3 → Type u_4
d : Membership α ρ
inst✝¹ : ForIn' m✝ ρ α d
β : Type u_3
inst✝ : Monad m✝
x : ρ
b : β
f : (a : α) → a ∈ x → β → m✝ (ForInStep β)
g : α → β → m✝ (ForInStep β)
h : ∀ (a : α) (m : a ∈ x) (b : β), f a m b = g a b
a : α
m : a ∈ x
⊢ ∀ (x : β), f a m x = g a x