case refine'_1
σ : Type u_1
f : σ → Option σ
a b : σ
h : b ∈ eval f a
⊢ Reaches f a b ∧ f b = none

case refine'_2
σ : Type u_1
f : σ → Option σ
a b : σ
x✝ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
⊢ b ∈ eval f a
σ : Type u_1
f : σ → Option σ
a b : σ
⊢ b ∈ eval f a ↔ Reaches f a b ∧ f b = none
refine' ⟨fun h ↦ _, fun ⟨h₁, h₂⟩ ↦ _⟩
case refine'_1
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → (fun a => Reaches f a b ∧ f b = none) a'
⊢ (fun a => Reaches f a b ∧ f b = none) a
case refine'_1
σ : Type u_1
f : σ → Option σ
a b : σ
h : b ∈ eval f a
⊢ Reaches f a b ∧ f b = none
refine' @evalInduction _ _ _ (fun a ↦ Reaches f a b ∧ f b = none) _ h fun a h IH ↦ _
case refine'_1.none
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → (fun a => Reaches f a b ∧ f b = none) a'
e : f a = none
⊢ Reaches f a b ∧ f b = none

case refine'_1.some
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → (fun a => Reaches f a b ∧ f b = none) a'
a' : σ
e : f a = some a'
⊢ Reaches f a b ∧ f b = none
case refine'_1
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → (fun a => Reaches f a b ∧ f b = none) a'
⊢ (fun a => Reaches f a b ∧ f b = none) a
cases' e : f a with a'
case refine'_1.none
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → (fun a => Reaches f a b ∧ f b = none) a'
e : f a = none
⊢ Reaches f a a ∧ f a = none
case refine'_1.none
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → (fun a => Reaches f a b ∧ f b = none) a'
e : f a = none
⊢ Reaches f a b ∧ f b = none
rw [Part.mem_unique h
    (PFun.mem_fix_iff.2 <| Or.inl <| Part.mem_some_iff.2 <| by rw [e] <;> rfl)]
no goals
case refine'_1.none
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → (fun a => Reaches f a b ∧ f b = none) a'
e : f a = none
⊢ Reaches f a a ∧ f a = none
exact ⟨ReflTransGen.refl, e⟩
no goals
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → (fun a => Reaches f a b ∧ f b = none) a'
e : f a = none
⊢ Sum.inl ?m.65549 = Option.elim (f a) (Sum.inl a) Sum.inr
rw [e] <;> rfl
case refine'_1.some.inr.intro.intro.refl
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝¹ : b ∈ eval f a✝
a : σ
h✝ : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → (fun a => Reaches f a b ∧ f b = none) a'
a' : σ
e : f a = some a'
h : Sum.inr a' ∈ Part.some (Option.elim (some a') (Sum.inl a) Sum.inr)
right✝ : b ∈ PFun.fix (fun s => Part.some (Option.elim (f s) (Sum.inl s) Sum.inr)) a'
⊢ Reaches f a b ∧ f b = none
case refine'_1.some
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → (fun a => Reaches f a b ∧ f b = none) a'
a' : σ
e : f a = some a'
⊢ Reaches f a b ∧ f b = none
rcases PFun.mem_fix_iff.1 h with (h | ⟨_, h, _⟩) <;> rw [e] at h <;>
  cases Part.mem_some_iff.1 h
case refine'_1.some.inr.intro.intro.refl.intro
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝¹ : b ∈ eval f a✝
a : σ
h✝ : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → (fun a => Reaches f a b ∧ f b = none) a'
a' : σ
e : f a = some a'
h : Sum.inr a' ∈ Part.some (Option.elim (some a') (Sum.inl a) Sum.inr)
right✝ : b ∈ PFun.fix (fun s => Part.some (Option.elim (f s) (Sum.inl s) Sum.inr)) a'
h₁ : Reaches f a' b
h₂ : f b = none
⊢ Reaches f a b ∧ f b = none
case refine'_1.some.inr.intro.intro.refl
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝¹ : b ∈ eval f a✝
a : σ
h✝ : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → (fun a => Reaches f a b ∧ f b = none) a'
a' : σ
e : f a = some a'
h : Sum.inr a' ∈ Part.some (Option.elim (some a') (Sum.inl a) Sum.inr)
right✝ : b ∈ PFun.fix (fun s => Part.some (Option.elim (f s) (Sum.inl s) Sum.inr)) a'
⊢ Reaches f a b ∧ f b = none
cases' IH a' e with h₁ h₂
no goals
case refine'_1.some.inr.intro.intro.refl.intro
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝¹ : b ∈ eval f a✝
a : σ
h✝ : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → (fun a => Reaches f a b ∧ f b = none) a'
a' : σ
e : f a = some a'
h : Sum.inr a' ∈ Part.some (Option.elim (some a') (Sum.inl a) Sum.inr)
right✝ : b ∈ PFun.fix (fun s => Part.some (Option.elim (f s) (Sum.inl s) Sum.inr)) a'
h₁ : Reaches f a' b
h₂ : f b = none
⊢ Reaches f a b ∧ f b = none
exact ⟨ReflTransGen.head e h₁, h₂⟩
case refine'_2.refine'_1
σ : Type u_1
f : σ → Option σ
a b : σ
x✝ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
⊢ b ∈ eval f b

case refine'_2.refine'_2
σ : Type u_1
f : σ → Option σ
a b : σ
x✝¹ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
a✝ c✝ : σ
h : c✝ ∈ f a✝
x✝ : ReflTransGen (fun a b => b ∈ f a) c✝ b
IH : b ∈ eval f c✝
⊢ b ∈ eval f a✝
case refine'_2
σ : Type u_1
f : σ → Option σ
a b : σ
x✝ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
⊢ b ∈ eval f a
refine' ReflTransGen.head_induction_on h₁ _ fun h _ IH ↦ _
case refine'_2.refine'_1
σ : Type u_1
f : σ → Option σ
a b : σ
x✝ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
⊢ Sum.inl b ∈ Part.some (Option.elim (f b) (Sum.inl b) Sum.inr)
case refine'_2.refine'_1
σ : Type u_1
f : σ → Option σ
a b : σ
x✝ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
⊢ b ∈ eval f b
refine' PFun.mem_fix_iff.2 (Or.inl _)
case refine'_2.refine'_1
σ : Type u_1
f : σ → Option σ
a b : σ
x✝ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
⊢ Sum.inl b ∈ Part.some (Option.elim none (Sum.inl b) Sum.inr)
case refine'_2.refine'_1
σ : Type u_1
f : σ → Option σ
a b : σ
x✝ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
⊢ Sum.inl b ∈ Part.some (Option.elim (f b) (Sum.inl b) Sum.inr)
rw [h₂]
no goals
case refine'_2.refine'_1
σ : Type u_1
f : σ → Option σ
a b : σ
x✝ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
⊢ Sum.inl b ∈ Part.some (Option.elim none (Sum.inl b) Sum.inr)
apply Part.mem_some
case refine'_2.refine'_2
σ : Type u_1
f : σ → Option σ
a b : σ
x✝¹ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
a✝ c✝ : σ
h : c✝ ∈ f a✝
x✝ : ReflTransGen (fun a b => b ∈ f a) c✝ b
IH : b ∈ eval f c✝
⊢ Sum.inr c✝ ∈ Part.some (Option.elim (f a✝) (Sum.inl a✝) Sum.inr)
case refine'_2.refine'_2
σ : Type u_1
f : σ → Option σ
a b : σ
x✝¹ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
a✝ c✝ : σ
h : c✝ ∈ f a✝
x✝ : ReflTransGen (fun a b => b ∈ f a) c✝ b
IH : b ∈ eval f c✝
⊢ b ∈ eval f a✝
refine' PFun.mem_fix_iff.2 (Or.inr ⟨_, _, IH⟩)
case refine'_2.refine'_2
σ : Type u_1
f : σ → Option σ
a b : σ
x✝¹ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
a✝ c✝ : σ
h : c✝ ∈ f a✝
x✝ : ReflTransGen (fun a b => b ∈ f a) c✝ b
IH : b ∈ eval f c✝
⊢ Sum.inr c✝ ∈ Part.some (Option.elim (some c✝) (Sum.inl a✝) Sum.inr)
case refine'_2.refine'_2
σ : Type u_1
f : σ → Option σ
a b : σ
x✝¹ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
a✝ c✝ : σ
h : c✝ ∈ f a✝
x✝ : ReflTransGen (fun a b => b ∈ f a) c✝ b
IH : b ∈ eval f c✝
⊢ Sum.inr c✝ ∈ Part.some (Option.elim (f a✝) (Sum.inl a✝) Sum.inr)
rw [h]
no goals
case refine'_2.refine'_2
σ : Type u_1
f : σ → Option σ
a b : σ
x✝¹ : Reaches f a b ∧ f b = none
h₁ : Reaches f a b
h₂ : f b = none
a✝ c✝ : σ
h : c✝ ∈ f a✝
x✝ : ReflTransGen (fun a b => b ∈ f a) c✝ b
IH : b ∈ eval f c✝
⊢ Sum.inr c✝ ∈ Part.some (Option.elim (some c✝) (Sum.inl a✝) Sum.inr)
apply Part.mem_some