no goals
α : Type u_1
β : Type ?u.115565
γ : Type ?u.115568
δ : Type ?u.115571
σ : Type ?u.115574
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable δ
inst✝¹ : Primcodable σ
inst✝ : Inhabited α
o : Option α
⊢ (Option.casesOn (id o) default fun b => b) = Option.iget o
cases o <;> rfl