-- Mathlib/Computability/TuringMachine.lean
theorem stmts₁_trans {q₁ q₂ : Stmt Γ Λ σ} : q₁ ∈ stmts₁ q₂ → stmts₁ q₁ ⊆ stmts₁ q₂

Proof state:
case pop
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
k✝ : K
a✝ : σ → Option (Γ k✝) → σ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ insert (pop k✝ a✝ q) (stmts₁ q)
⊢ q₀ ∈ insert (pop k✝ a✝ q) (stmts₁ q)

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton, Finset.mem_union] at h₁₂

Result:
case pop
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
k✝ : K
a✝ : σ → Option (Γ k✝) → σ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ = pop k✝ a✝ q ∨ q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (pop k✝ a✝ q) (stmts₁ q)

Proof state:
case branch
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ = branch f q₁ q₂ ∨ q₁✝ ∈ stmts₁ q₁ ∨ q₁✝ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch f q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Tactic:
rcases h₁₂ with (rfl | h₁₂ | h₁₂)

Result:
case branch.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (branch f q₁ q₂)
IH₁ : branch f q₁ q₂ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : branch f q₁ q₂ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch f q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

case branch.inr.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₁
⊢ q₀ ∈ insert (branch f q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

case branch.inr.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch f q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Proof state:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₂ : Stmt Γ Λ σ
⊢ q₁ ∈ stmts₁ q₂ → stmts₁ q₁ ⊆ stmts₁ q₂

Tactic:
intro h₁₂ q₀ h₀₁

Result:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₂ : Stmt Γ Λ σ
h₁₂ : q₁ ∈ stmts₁ q₂
q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
⊢ q₀ ∈ stmts₁ q₂

Proof state:
case halt
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ halt
⊢ q₀ ∈ {halt}

Tactic:
exact h₀₁

Result:
no goals

Proof state:
case branch.inr.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₁
⊢ q₀ ∈ insert (branch f q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Tactic:
exact Finset.mem_insert_of_mem (Finset.mem_union_left _ (IH₁ h₁₂))

Result:
no goals

Proof state:
case pop
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
k✝ : K
a✝ : σ → Option (Γ k✝) → σ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ (pop k✝ a✝ q)
⊢ q₀ ∈ stmts₁ (pop k✝ a✝ q)

Tactic:
simp only [stmts₁] at h₁₂ ⊢

Result:
case pop
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
k✝ : K
a✝ : σ → Option (Γ k✝) → σ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ insert (pop k✝ a✝ q) (stmts₁ q)
⊢ q₀ ∈ insert (pop k✝ a✝ q) (stmts₁ q)

Proof state:
case halt
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
h₁₂ : q₁ = halt
⊢ q₀ ∈ {halt}

Tactic:
subst h₁₂

Result:
case halt
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ halt
⊢ q₀ ∈ {halt}

Proof state:
case pop.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
k✝ : K
a✝ : σ → Option (Γ k✝) → σ
q : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (pop k✝ a✝ q)
IH : pop k✝ a✝ q ∈ stmts₁ q → q₀ ∈ stmts₁ q
⊢ q₀ ∈ insert (pop k✝ a✝ q) (stmts₁ q)

Tactic:
unfold stmts₁ at h₀₁

Result:
case pop.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
k✝ : K
a✝ : σ → Option (Γ k✝) → σ
q : Stmt Γ Λ σ
IH : pop k✝ a✝ q ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₀₁ : q₀ ∈ insert (pop k✝ a✝ q) (stmts₁ q)
⊢ q₀ ∈ insert (pop k✝ a✝ q) (stmts₁ q)

Proof state:
case branch.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (branch f q₁ q₂)
IH₁ : branch f q₁ q₂ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : branch f q₁ q₂ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch f q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Tactic:
unfold stmts₁ at h₀₁

Result:
case branch.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : branch f q₁ q₂ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : branch f q₁ q₂ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₀₁ : q₀ ∈ insert (branch f q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
⊢ q₀ ∈ insert (branch f q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Proof state:
case goto
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
l : σ → Λ
h₀₁ : q₀ ∈ stmts₁ (goto l)
⊢ q₀ ∈ {goto l}

Tactic:
exact h₀₁

Result:
no goals

Proof state:
case pop.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
k✝ : K
a✝ : σ → Option (Γ k✝) → σ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (pop k✝ a✝ q) (stmts₁ q)

Tactic:
exact Finset.mem_insert_of_mem (IH h₁₂)

Result:
no goals

Proof state:
case pop.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
k✝ : K
a✝ : σ → Option (Γ k✝) → σ
q : Stmt Γ Λ σ
IH : pop k✝ a✝ q ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₀₁ : q₀ ∈ insert (pop k✝ a✝ q) (stmts₁ q)
⊢ q₀ ∈ insert (pop k✝ a✝ q) (stmts₁ q)

Tactic:
exact h₀₁

Result:
no goals

Proof state:
case goto
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
l : σ → Λ
h₁₂ : q₁ = goto l
⊢ q₀ ∈ {goto l}

Tactic:
subst h₁₂

Result:
case goto
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
l : σ → Λ
h₀₁ : q₀ ∈ stmts₁ (goto l)
⊢ q₀ ∈ {goto l}

Proof state:
case branch.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : branch f q₁ q₂ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : branch f q₁ q₂ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₀₁ : q₀ ∈ insert (branch f q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)
⊢ q₀ ∈ insert (branch f q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Tactic:
exact h₀₁

Result:
no goals

Proof state:
case branch.inr.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁✝ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁✝
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → q₀ ∈ stmts₁ q₁
IH₂ : q₁✝ ∈ stmts₁ q₂ → q₀ ∈ stmts₁ q₂
h₁₂ : q₁✝ ∈ stmts₁ q₂
⊢ q₀ ∈ insert (branch f q₁ q₂) (stmts₁ q₁ ∪ stmts₁ q₂)

Tactic:
exact Finset.mem_insert_of_mem (Finset.mem_union_right _ (IH₂ h₁₂))

Result:
no goals

Proof state:
case pop
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
k✝ : K
a✝ : σ → Option (Γ k✝) → σ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ = pop k✝ a✝ q ∨ q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (pop k✝ a✝ q) (stmts₁ q)

Tactic:
rcases h₁₂ with (rfl | h₁₂)

Result:
case pop.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₀ : Stmt Γ Λ σ
k✝ : K
a✝ : σ → Option (Γ k✝) → σ
q : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ (pop k✝ a✝ q)
IH : pop k✝ a✝ q ∈ stmts₁ q → q₀ ∈ stmts₁ q
⊢ q₀ ∈ insert (pop k✝ a✝ q) (stmts₁ q)

case pop.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
q₁ q₀ : Stmt Γ Λ σ
h₀₁ : q₀ ∈ stmts₁ q₁
k✝ : K
a✝ : σ → Option (Γ k✝) → σ
q : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ q → q₀ ∈ stmts₁ q
h₁₂ : q₁ ∈ stmts₁ q
⊢ q₀ ∈ insert (pop k✝ a✝ q) (stmts₁ q)