α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
i : Encodable α
n : ℕ
⊢ Option.map (↑(Equiv.sigmaEquivProd α β))
      (Option.bind (decode (unpair n).fst) fun a => Option.map (Sigma.mk a) (decode (unpair n).snd)) =
    Option.bind (decode (unpair n).fst) fun a => Option.map (Prod.mk a) (decode (unpair n).snd)
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
i : Encodable α
n : ℕ
⊢ decode n = Option.bind (decode (unpair n).fst) fun a => Option.map (Prod.mk a) (decode (unpair n).snd)
simp only [decode_ofEquiv, Equiv.symm_symm, decode_sigma_val]
no goals
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
i : Encodable α
n : ℕ
⊢ Option.map (↑(Equiv.sigmaEquivProd α β))
      (Option.bind (decode (unpair n).fst) fun a => Option.map (Sigma.mk a) (decode (unpair n).snd)) =
    Option.bind (decode (unpair n).fst) fun a => Option.map (Prod.mk a) (decode (unpair n).snd)
cases (decode n.unpair.1 : Option α) <;> cases (decode n.unpair.2 : Option β)
<;> rfl