no goals
α : Type u_1
β : Type ?u.139430
γ : Type ?u.139433
δ : Type ?u.139436
σ : Type ?u.139439
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
x✝ : Option α × Option α
o₁ o₂ : Option α
⊢ (Option.casesOn (o₁, o₂).fst (o₁, o₂).snd fun b => ((o₁, o₂), b).fst.fst) =
    (fun x x_1 => HOrElse.hOrElse x fun x => x_1) (o₁, o₂).fst (o₁, o₂).snd
cases o₁ <;> cases o₂ <;> rfl