rintro (_ | a) <;> simp
α✝ : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : Type u_4
γ : Type u_5
σ : Type u_6
τ : Type u_7
inst✝⁸ : Primcodable α✝
inst✝⁷ : Primcodable α₁
inst✝⁶ : Primcodable α₂
inst✝⁵ : Primcodable β
inst✝⁴ : Primcodable γ
inst✝³ : Primcodable σ
inst✝² : Primcodable τ
α : Type u_8
inst✝¹ : Primcodable α
inst✝ : Inhabited α
⊢ ∀ (n : Option α), (Option.casesOn (id n) default fun b => b) = n.get!
no goals