-- Mathlib/Computability/TuringMachine.lean
theorem stmts₁_supportsStmt_mono {S : Finset Λ} {q₁ q₂ : Stmt Γ Λ σ} (h : q₁ ∈ stmts₁ q₂)
    (hs : SupportsStmt S q₂) : SupportsStmt S q₁

Proof state:
case pop
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁ : Stmt Γ Λ σ
k✝ : K
a✝¹ : σ → Option (Γ k✝) → σ
a✝ : Stmt Γ Λ σ
IH : q₁ ∈ stmts₁ a✝ → SupportsStmt S a✝ → SupportsStmt S q₁
hs : SupportsStmt S a✝
h : q₁ = pop k✝ a✝¹ a✝ ∨ q₁ ∈ stmts₁ a✝
⊢ SupportsStmt S q₁

Tactic:
rcases h with (rfl | h) <;> [exact hs; exact IH h hs]

Result:
no goals

Proof state:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁ q₂ : Stmt Γ Λ σ
h : q₁ ∈ stmts₁ q₂
hs : SupportsStmt S q₂
⊢ SupportsStmt S q₁

Tactic:
induction q₂ with
  simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
    at h hs
| branch f q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
| goto l => subst h; exact hs
| halt => subst h; trivial
| load _ _ IH | _ _ _ _ IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]

Result:
no goals

Proof state:
case branch
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁✝ : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S q₁✝
IH₂ : q₁✝ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S q₁✝
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
h : q₁✝ = branch f q₁ q₂ ∨ q₁✝ ∈ stmts₁ q₁ ∨ q₁✝ ∈ stmts₁ q₂
⊢ SupportsStmt S 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
S : Finset Λ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
IH₁ : branch f q₁ q₂ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S (branch f q₁ q₂)
IH₂ : branch f q₁ q₂ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S (branch f q₁ q₂)
⊢ SupportsStmt S (branch f q₁ q₂)

case branch.inr.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁✝ : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S q₁✝
IH₂ : q₁✝ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S q₁✝
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
h : q₁✝ ∈ stmts₁ q₁
⊢ SupportsStmt S q₁✝

case branch.inr.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁✝ : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S q₁✝
IH₂ : q₁✝ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S q₁✝
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
h : q₁✝ ∈ stmts₁ q₂
⊢ SupportsStmt S q₁✝

Proof state:
case halt
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁ : Stmt Γ Λ σ
hs : True
h : q₁ = halt
⊢ SupportsStmt S q₁

Tactic:
subst h

Result:
case halt
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
hs : True
⊢ SupportsStmt S halt

Proof state:
case halt
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
hs : True
⊢ SupportsStmt S halt

Tactic:
trivial

Result:
no goals

Proof state:
case goto
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁ : Stmt Γ Λ σ
l : σ → Λ
hs : ∀ (v : σ), l v ∈ S
h : q₁ = goto l
⊢ SupportsStmt S q₁

Tactic:
subst h

Result:
case goto
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
l : σ → Λ
hs : ∀ (v : σ), l v ∈ S
⊢ SupportsStmt S (goto l)

Proof state:
case goto
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
l : σ → Λ
hs : ∀ (v : σ), l v ∈ S
⊢ SupportsStmt S (goto l)

Tactic:
exact hs

Result:
no goals

Proof state:
case branch.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
IH₁ : branch f q₁ q₂ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S (branch f q₁ q₂)
IH₂ : branch f q₁ q₂ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S (branch f q₁ q₂)
⊢ SupportsStmt S (branch f q₁ q₂)

case branch.inr.inl
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁✝ : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S q₁✝
IH₂ : q₁✝ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S q₁✝
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
h : q₁✝ ∈ stmts₁ q₁
⊢ SupportsStmt S q₁✝

case branch.inr.inr
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
q₁✝ : Stmt Γ Λ σ
f : σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ : q₁✝ ∈ stmts₁ q₁ → SupportsStmt S q₁ → SupportsStmt S q₁✝
IH₂ : q₁✝ ∈ stmts₁ q₂ → SupportsStmt S q₂ → SupportsStmt S q₁✝
hs : SupportsStmt S q₁ ∧ SupportsStmt S q₂
h : q₁✝ ∈ stmts₁ q₂
⊢ SupportsStmt S q₁✝

Tactic:
exacts [hs, IH₁ h hs.1, IH₂ h hs.2]

Result:
no goals