-- Mathlib/Computability/PostTuringMachine.lean
theorem mem_eval {σ} {f : σ → Option σ} {a b} : b ∈ eval f a ↔ Reaches f a b ∧ f b = none

Proof state:
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 (none.elim (Sum.inl b) Sum.inr)

Tactic:
apply Part.mem_some

Result:
no goals

Proof state:
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' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
h : Sum.inr a' ∈ Part.some ((some a').elim (Sum.inl a) Sum.inr)
right✝ : b ∈ PFun.fix (fun s => Part.some ((f s).elim (Sum.inl s) Sum.inr)) a'
h₁ : Reaches f a' b
h₂ : f b = none
⊢ Reaches f a b ∧ f b = none

Tactic:
exact ⟨ReflTransGen.head e h₁, h₂⟩

Result:
no goals

Proof state:
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' → Reaches f a' b ∧ f b = none
e : f a = none
⊢ Reaches f a b ∧ f b = none

Tactic:
rw [Part.mem_unique h
    (PFun.mem_fix_iff.2 <| Or.inl <| Part.mem_some_iff.2 <| by rw [e]; rfl)]

Result:
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' → Reaches f a' b ∧ f b = none
e : f a = none
⊢ Reaches f a a ∧ f a = none

Proof state:
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 ((f a✝).elim (Sum.inl a✝) Sum.inr)

Tactic:
rw [h]

Result:
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 ((some c✝).elim (Sum.inl a✝) Sum.inr)

Proof state:
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' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
h : Sum.inr a' ∈ Part.some ((some a').elim (Sum.inl a) Sum.inr)
right✝ : b ∈ PFun.fix (fun s => Part.some ((f s).elim (Sum.inl s) Sum.inr)) a'
⊢ Reaches f a b ∧ f b = none

Tactic:
obtain ⟨h₁, h₂⟩ := IH a' e

Result:
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' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
h : Sum.inr a' ∈ Part.some ((some a').elim (Sum.inl a) Sum.inr)
right✝ : b ∈ PFun.fix (fun s => Part.some ((f s).elim (Sum.inl s) Sum.inr)) a'
h₁ : Reaches f a' b
h₂ : f b = none
⊢ Reaches f a b ∧ f b = none

Proof state:
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✝

Tactic:
refine PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, IH⟩)

Result:
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 ((f a✝).elim (Sum.inl a✝) Sum.inr)

Proof state:
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

Tactic:
refine PFun.mem_fix_iff.2 (Or.inl ?_)

Result:
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 ((f b).elim (Sum.inl b) Sum.inr)

Proof state:
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' → Reaches f a' b ∧ f b = none
e : f a = none
⊢ Reaches f a a ∧ f a = none

Tactic:
exact ⟨ReflTransGen.refl, e⟩

Result:
no goals

Proof state:
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 ((some c✝).elim (Sum.inl a✝) Sum.inr)

Tactic:
apply Part.mem_some

Result:
no goals

Proof state:
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
e : f a = none
⊢ Sum.inl ?m.2436 = (f a).elim (Sum.inl a) Sum.inr

Tactic:
rw [e]

Result:
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
e : f a = none
⊢ Sum.inl ?m.2436 = none.elim (Sum.inl a) Sum.inr

Proof state:
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

Tactic:
refine ReflTransGen.head_induction_on h₁ ?_ fun h _ IH ↦ ?_

Result:
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✝

Proof state:
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 ((f b).elim (Sum.inl b) Sum.inr)

Tactic:
rw [h₂]

Result:
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 (none.elim (Sum.inl b) Sum.inr)

Proof state:
case refine_1
σ : Type u_1
f : σ → Option σ
a b : σ
h : b ∈ eval f a
⊢ Reaches f a b ∧ f b = none

Tactic:
refine evalInduction h fun a h IH ↦ ?_

Result:
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' → Reaches f a' b ∧ f b = none
⊢ Reaches f a b ∧ f b = none

Proof state:
σ : Type u_1
f : σ → Option σ
a b : σ
⊢ b ∈ eval f a ↔ Reaches f a b ∧ f b = none

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨h₁, h₂⟩ ↦ ?_⟩

Result:
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

Proof state:
σ : Type u_1
f : σ → Option σ
a✝ b : σ
h✝ : b ∈ eval f a✝
a : σ
h : b ∈ eval f a
IH : ∀ (a' : σ), f a = some a' → Reaches f a' b ∧ f b = none
e : f a = none
⊢ Sum.inl ?m.2436 = none.elim (Sum.inl a) Sum.inr

Tactic:
rfl

Result:
no goals

Proof state:
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' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
⊢ Reaches f a b ∧ f b = none

Tactic:
rcases PFun.mem_fix_iff.1 h with (h | ⟨_, h, _⟩) <;> rw [e] at h <;>
  cases Part.mem_some_iff.1 h

Result:
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' → Reaches f a' b ∧ f b = none
a' : σ
e : f a = some a'
h : Sum.inr a' ∈ Part.some ((some a').elim (Sum.inl a) Sum.inr)
right✝ : b ∈ PFun.fix (fun s => Part.some ((f s).elim (Sum.inl s) Sum.inr)) a'
⊢ Reaches f a b ∧ f b = none