Theorem: Primrec.of_list_decode_eq_some_cons (Logic/Vorspiel/Computability.lean)

State before:
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
a : α
as : List α
e : ℕ
⊢ decode e = some (a :: as) → decode e.pred.unpair.1 = some a ∧ decode e.pred.unpair.2 = some as
Tactic:
rcases e with (_ | e) <;> simp
State after:
case succ
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
a : α
as : List α
e : ℕ
⊢ (Seq.seq (Option.map (fun x x_1 => x :: x_1) (decode e.unpair.1)) fun x => decode e.unpair.2) = some (a :: as) →
    decode e.unpair.1 = some a ∧ decode e.unpair.2 = some as

State before:
case succ
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
a : α
as : List α
e : ℕ
⊢ (Seq.seq (Option.map (fun x x_1 => x :: x_1) (decode e.unpair.1)) fun x => decode e.unpair.2) = some (a :: as) →
    decode e.unpair.1 = some a ∧ decode e.unpair.2 = some as
Tactic:
rcases (decode e.unpair.1) with (_ | a) <;> simp[seq_eq_bind_map, Option.bind_eq_bind]
State after:
case succ.some
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
a✝ : α
as : List α
e : ℕ
a : α
⊢ decode e.unpair.2 = some as → a = a✝ → a = a✝ ∧ decode e.unpair.2 = some as

State before:
case succ.some
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
a✝ : α
as : List α
e : ℕ
a : α
⊢ decode e.unpair.2 = some as → a = a✝ → a = a✝ ∧ decode e.unpair.2 = some as
Tactic:
rcases (decode e.unpair.2) with (_ | as) <;> simp[seq_eq_bind_map, Option.bind_eq_bind]
State after:
case succ.some.some
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
a✝ : α
as✝ : List α
e : ℕ
a : α
as : List α
⊢ as = as✝ → a = a✝ → a = a✝ ∧ as = as✝

State before:
case succ.some.some
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
a✝ : α
as✝ : List α
e : ℕ
a : α
as : List α
⊢ as = as✝ → a = a✝ → a = a✝ ∧ as = as✝
Tactic:
rintro rfl rfl
State after:
case succ.some.some
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
e : ℕ
a : α
as : List α
⊢ a = a ∧ as = as

State before:
case succ.some.some
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁶ : Primcodable α
inst✝⁵ : Primcodable α₁
inst✝⁴ : Primcodable α₂
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable σ
inst✝ : Primcodable τ
e : ℕ
a : α
as : List α
⊢ a = a ∧ as = as
Tactic:
simp
State after:
no goals