no goals
α : Type u_1
β : Type ?u.116351
γ : Type ?u.116354
δ : Type ?u.116357
σ : Type ?u.116360
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
x✝ : Option α × α
o : Option α
a : α
⊢ (Option.casesOn ((fun a x => a) (o, a).fst (o, a).snd) ((fun x b => b) (o, a).fst (o, a).snd) fun b => b) =
    Option.getD (o, a).fst (o, a).snd
cases o <;> rfl