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

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : UniformlyPrimcodable β
this : Primrec fun e => (decode e.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) e.unpair.2)
⊢ ∀ (n : ℕ),
    ((decode n.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) n.unpair.2)) =
      Option.map Sigma.fst (decode n)
Tactic:
intro n
State after:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : UniformlyPrimcodable β
this : Primrec fun e => (decode e.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) e.unpair.2)
n : ℕ
⊢ ((decode n.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) n.unpair.2)) =
    Option.map Sigma.fst (decode n)

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : UniformlyPrimcodable β
this : Primrec fun e => (decode e.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) e.unpair.2)
n : ℕ
⊢ ((decode n.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) n.unpair.2)) =
    Option.map Sigma.fst (decode n)
Tactic:
simp
State after:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : UniformlyPrimcodable β
this : Primrec fun e => (decode e.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) e.unpair.2)
n : ℕ
⊢ ((decode n.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) n.unpair.2)) =
    Option.map Sigma.fst ((decode n.unpair.1).bind fun a => Option.map (Sigma.mk a) (decode n.unpair.2))

State before:
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : UniformlyPrimcodable β
this : Primrec fun e => (decode e.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) e.unpair.2)
n : ℕ
⊢ ((decode n.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) n.unpair.2)) =
    Option.map Sigma.fst ((decode n.unpair.1).bind fun a => Option.map (Sigma.mk a) (decode n.unpair.2))
Tactic:
rcases (decode n.unpair.1) with (_ | a) <;> simp
State after:
case some
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : UniformlyPrimcodable β
this : Primrec fun e => (decode e.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) e.unpair.2)
n : ℕ
a : α
⊢ Option.map (fun x => a) (encodeDecode (β a) n.unpair.2) = Option.map (Sigma.fst ∘ Sigma.mk a) (decode n.unpair.2)

State before:
case some
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : UniformlyPrimcodable β
this : Primrec fun e => (decode e.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) e.unpair.2)
n : ℕ
a : α
⊢ Option.map (fun x => a) (encodeDecode (β a) n.unpair.2) = Option.map (Sigma.fst ∘ Sigma.mk a) (decode n.unpair.2)
Tactic:
{ simp[encodeDecode_eq_encode_map_decode, Function.comp] }
State after:
no goals

State before:
case some
σ : Type u_1
α : Type u_2
β : α → Type u_3
γ : Type u_4
inst✝⁷ : Primcodable σ
inst✝⁶ : Primcodable α
inst✝⁵ : (a : α) → Fintype (β a)
inst✝⁴ : (a : α) → DecidableEq (β a)
inst✝³ : (a : α) → Primcodable (β a)
inst✝² : PrimrecCard β
inst✝¹ : Primcodable γ
inst✝ : UniformlyPrimcodable β
this : Primrec fun e => (decode e.unpair.1).bind fun a => Option.map (fun x => a) (encodeDecode (β a) e.unpair.2)
n : ℕ
a : α
⊢ Option.map (fun x => a) (encodeDecode (β a) n.unpair.2) = Option.map (Sigma.fst ∘ Sigma.mk a) (decode n.unpair.2)
Tactic:
simp[encodeDecode_eq_encode_map_decode, Function.comp]
State after:
no goals