α : Type u_1
β : Type ?u.23484
inst✝² : Denumerable α
inst✝¹ : Denumerable β
γ : α → Type u_2
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ (Option.bind (decode (unpair n).fst) fun a => Option.map (Sigma.mk a) (decode (unpair n).snd)) =
    some { fst := ofNat α (unpair n).fst, snd := ofNat (γ (ofNat α (unpair n).fst)) (unpair n).snd }
α : Type u_1
β : Type ?u.23484
inst✝² : Denumerable α
inst✝¹ : Denumerable β
γ : α → Type u_2
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ some (ofNat (Sigma γ) n) =
    some { fst := ofNat α (unpair n).fst, snd := ofNat (γ (ofNat α (unpair n).fst)) (unpair n).snd }
rw [← decode_eq_ofNat, decode_sigma_val]
no goals
α : Type u_1
β : Type ?u.23484
inst✝² : Denumerable α
inst✝¹ : Denumerable β
γ : α → Type u_2
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ (Option.bind (decode (unpair n).fst) fun a => Option.map (Sigma.mk a) (decode (unpair n).snd)) =
    some { fst := ofNat α (unpair n).fst, snd := ofNat (γ (ofNat α (unpair n).fst)) (unpair n).snd }
simp