α : Type uu
β : Type vv
l₁ l₂ : List α
o₁ o₂ : Option α
p : Option.toList o₁ ~ Option.toList o₂
⊢ o₁ = o₂
α : Type uu
β : Type vv
l₁ l₂ : List α
o₁ o₂ : Option α
⊢ Option.toList o₁ ~ Option.toList o₂ ↔ o₁ = o₂
refine' ⟨fun p => _, fun e => e ▸ Perm.refl _⟩
case none.none
α : Type uu
β : Type vv
l₁ l₂ : List α
p : Option.toList none ~ Option.toList none
⊢ none = none

case none.some
α : Type uu
β : Type vv
l₁ l₂ : List α
b : α
p : Option.toList none ~ Option.toList (some b)
⊢ none = some b

case some.none
α : Type uu
β : Type vv
l₁ l₂ : List α
a : α
p : Option.toList (some a) ~ Option.toList none
⊢ some a = none

case some.some
α : Type uu
β : Type vv
l₁ l₂ : List α
a b : α
p : Option.toList (some a) ~ Option.toList (some b)
⊢ some a = some b
α : Type uu
β : Type vv
l₁ l₂ : List α
o₁ o₂ : Option α
p : Option.toList o₁ ~ Option.toList o₂
⊢ o₁ = o₂
cases' o₁ with a <;> cases' o₂ with b
no goals
case none.none
α : Type uu
β : Type vv
l₁ l₂ : List α
p : Option.toList none ~ Option.toList none
⊢ none = none
rfl
no goals
case none.some
α : Type uu
β : Type vv
l₁ l₂ : List α
b : α
p : Option.toList none ~ Option.toList (some b)
⊢ none = some b
cases p.length_eq
no goals
case some.none
α : Type uu
β : Type vv
l₁ l₂ : List α
a : α
p : Option.toList (some a) ~ Option.toList none
⊢ some a = none
cases p.length_eq
no goals
case some.some
α : Type uu
β : Type vv
l₁ l₂ : List α
a b : α
p : Option.toList (some a) ~ Option.toList (some b)
⊢ some a = some b
exact Option.mem_toList.1 (p.symm.subset <| by simp)
no goals
α : Type uu
β : Type vv
l₁ l₂ : List α
a b : α
p : Option.toList (some a) ~ Option.toList (some b)
⊢ b ∈ Option.toList (some b)
simp