-- Mathlib/Computability/PostTuringMachine.lean
theorem tr_supports {S : Finset Λ} (ss : TM1.Supports M S) :
    TM0.Supports (tr M) ↑(trStmts M S)

Proof state:
case right.mk.some.mk.some.move
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
d : Dir
q : TM1.Stmt Γ Λ σ
a_ih✝ :
  ∀ (v : σ),
    some q ∈ TM1.stmts M S →
      some (trAux M a q v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q → some val✝ ∈ TM1.stmts M S
v : σ
h₂ : some (TM1.Stmt.move d q) ∈ TM1.stmts M S
h₁ : some (trAux M a (TM1.Stmt.move d q) v) = some ((some val✝, v'), s)
hs : TM1.SupportsStmt S (TM1.Stmt.move d q)
⊢ some val✝ ∈ TM1.stmts M S

Tactic:
cases h₁

Result:
case right.mk.some.mk.some.move.refl
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
d : Dir
h₂ : some (TM1.Stmt.move d val✝) ∈ TM1.stmts M S
hs : TM1.SupportsStmt S (TM1.Stmt.move d val✝)
a_ih✝ :
  ∀ (v : σ),
    some val✝ ∈ TM1.stmts M S →
      some (trAux M a val✝ v) = some ((some val✝, v'), move d) → TM1.SupportsStmt S val✝ → some val✝ ∈ TM1.stmts M S
⊢ some val✝ ∈ TM1.stmts M S

Proof state:
case right.mk.none
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
q' : Λ' M
s : TM0.Stmt Γ
v : σ
h₁ : (q', s) ∈ tr M (none, v) a
h₂ : (none, v) ∈ ↑(trStmts M S)
⊢ q' ∈ ↑(trStmts M S)

Tactic:
cases h₁

Result:
no goals

Proof state:
case right.mk.some.mk.some.move.refl
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
d : Dir
h₂ : some (TM1.Stmt.move d val✝) ∈ TM1.stmts M S
hs : TM1.SupportsStmt S (TM1.Stmt.move d val✝)
a_ih✝ :
  ∀ (v : σ),
    some val✝ ∈ TM1.stmts M S →
      some (trAux M a val✝ v) = some ((some val✝, v'), move d) → TM1.SupportsStmt S val✝ → some val✝ ∈ TM1.stmts M S
⊢ val✝ ∈ insert (TM1.Stmt.move d val✝) (TM1.stmts₁ val✝)

Tactic:
exact Finset.mem_insert_of_mem TM1.stmts₁_self

Result:
no goals

Proof state:
case right.mk.some.mk.some
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v : σ
q : TM1.Stmt Γ Λ σ
v' : σ
h₂ : some q ∈ TM1.stmts M S
val✝ : TM1.Stmt Γ Λ σ
h₁ : some (trAux M a q v) = some ((some val✝, v'), s)
⊢ some val✝ ∈ TM1.stmts M S

Tactic:
have := TM1.stmts_supportsStmt ss h₂

Result:
case right.mk.some.mk.some
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v : σ
q : TM1.Stmt Γ Λ σ
v' : σ
h₂ : some q ∈ TM1.stmts M S
val✝ : TM1.Stmt Γ Λ σ
h₁ : some (trAux M a q v) = some ((some val✝, v'), s)
this : TM1.SupportsStmt S q
⊢ some val✝ ∈ TM1.stmts M S

Proof state:
case right.mk.some.mk.some.load
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
b : Γ → σ → σ
q : TM1.Stmt Γ Λ σ
IH :
  ∀ (v : σ),
    some q ∈ TM1.stmts M S →
      some (trAux M a q v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q → some val✝ ∈ TM1.stmts M S
v : σ
h₂ : some (TM1.Stmt.load b q) ∈ TM1.stmts M S
h₁ : some (trAux M a (TM1.Stmt.load b q) v) = some ((some val✝, v'), s)
hs : TM1.SupportsStmt S (TM1.Stmt.load b q)
⊢ q ∈ insert (TM1.Stmt.load b q) (TM1.stmts₁ q)

Tactic:
exact Finset.mem_insert_of_mem TM1.stmts₁_self

Result:
no goals

Proof state:
case right.mk.some.mk.some.branch.true
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ),
    some q₁ ∈ TM1.stmts M S →
      some (trAux M a q₁ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₁ → some val✝ ∈ TM1.stmts M S
IH₂ :
  ∀ (v : σ),
    some q₂ ∈ TM1.stmts M S →
      some (trAux M a q₂ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₂ → some val✝ ∈ TM1.stmts M S
v : σ
h₂ : some (TM1.Stmt.branch p q₁ q₂) ∈ TM1.stmts M S
h₁ : some (bif true then trAux M a q₁ v else trAux M a q₂ v) = some ((some val✝, v'), s)
hs : TM1.SupportsStmt S (TM1.Stmt.branch p q₁ q₂)
h : p a v = true
⊢ q₁ ∈ TM1.stmts₁ (TM1.Stmt.branch p q₁ q₂)

Tactic:
unfold TM1.stmts₁

Result:
case right.mk.some.mk.some.branch.true
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ),
    some q₁ ∈ TM1.stmts M S →
      some (trAux M a q₁ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₁ → some val✝ ∈ TM1.stmts M S
IH₂ :
  ∀ (v : σ),
    some q₂ ∈ TM1.stmts M S →
      some (trAux M a q₂ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₂ → some val✝ ∈ TM1.stmts M S
v : σ
h₂ : some (TM1.Stmt.branch p q₁ q₂) ∈ TM1.stmts M S
h₁ : some (bif true then trAux M a q₁ v else trAux M a q₂ v) = some ((some val✝, v'), s)
hs : TM1.SupportsStmt S (TM1.Stmt.branch p q₁ q₂)
h : p a v = true
⊢ q₁ ∈ insert (TM1.Stmt.branch p q₁ q₂) (TM1.stmts₁ q₁ ∪ TM1.stmts₁ q₂)

Proof state:
case right.mk.some.mk.some.write.refl
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
b : Γ → σ → Γ
h₂ : some (TM1.Stmt.write b val✝) ∈ TM1.stmts M S
hs : TM1.SupportsStmt S (TM1.Stmt.write b val✝)
a_ih✝ :
  ∀ (v : σ),
    some val✝ ∈ TM1.stmts M S →
      some (trAux M a val✝ v) = some ((some val✝, v'), write (b a v')) →
        TM1.SupportsStmt S val✝ → some val✝ ∈ TM1.stmts M S
⊢ some val✝ ∈ TM1.stmts M S

Tactic:
refine TM1.stmts_trans ?_ h₂

Result:
case right.mk.some.mk.some.write.refl
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
b : Γ → σ → Γ
h₂ : some (TM1.Stmt.write b val✝) ∈ TM1.stmts M S
hs : TM1.SupportsStmt S (TM1.Stmt.write b val✝)
a_ih✝ :
  ∀ (v : σ),
    some val✝ ∈ TM1.stmts M S →
      some (trAux M a val✝ v) = some ((some val✝, v'), write (b a v')) →
        TM1.SupportsStmt S val✝ → some val✝ ∈ TM1.stmts M S
⊢ val✝ ∈ TM1.stmts₁ (TM1.Stmt.write b val✝)

Proof state:
case right.mk.some.mk.none
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v : σ
q : TM1.Stmt Γ Λ σ
v' : σ
h₂ : some q ∈ TM1.stmts M S
h₁ : ((none, v'), s) ∈ tr M (some q, v) a
⊢ none ∈ TM1.stmts M S

Tactic:
exact Multiset.mem_cons_self _ _

Result:
no goals

Proof state:
case left.left
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
⊢ default.1 ∈ TM1.stmts M S

Tactic:
simp only [default, TM1.stmts, Finset.mem_insertNone, Option.mem_def, Option.some_inj,
  forall_eq', Finset.mem_biUnion]

Result:
case left.left
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
⊢ ∃ a ∈ S, M default ∈ TM1.stmts₁ (M a)