case refine'_1
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x✝ : σ
h : x✝ ∈ eval f a
⊢ x✝ ∈ eval f b

case refine'_2
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x✝ : σ
h : x✝ ∈ eval f b
⊢ x✝ ∈ eval f a
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
⊢ eval f a = eval f b
refine' Part.ext fun _ ↦ ⟨fun h ↦ _, fun h ↦ _⟩
case refine'_1
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x✝ : σ
h : x✝ ∈ eval f a
ac : Reaches f a x✝
c0 : f x✝ = none
⊢ x✝ ∈ eval f b
case refine'_1
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x✝ : σ
h : x✝ ∈ eval f a
⊢ x✝ ∈ eval f b
have ⟨ac, c0⟩ := mem_eval.1 h
no goals
case refine'_1
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x✝ : σ
h : x✝ ∈ eval f a
ac : Reaches f a x✝
c0 : f x✝ = none
⊢ x✝ ∈ eval f b
exact mem_eval.2 ⟨(or_iff_left_of_imp fun cb ↦ (eval_maximal h).1 cb ▸ ReflTransGen.refl).1
  (reaches_total ab ac), c0⟩
case refine'_2
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x✝ : σ
h : x✝ ∈ eval f b
bc : Reaches f b x✝
c0 : f x✝ = none
⊢ x✝ ∈ eval f a
case refine'_2
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x✝ : σ
h : x✝ ∈ eval f b
⊢ x✝ ∈ eval f a
have ⟨bc, c0⟩ := mem_eval.1 h
no goals
case refine'_2
σ : Type u_1
f : σ → Option σ
a b : σ
ab : Reaches f a b
x✝ : σ
h : x✝ ∈ eval f b
bc : Reaches f b x✝
c0 : f x✝ = none
⊢ x✝ ∈ eval f a
exact mem_eval.2 ⟨ab.trans bc, c0⟩