α : Type u_1
l₁ l₂ : Lists' α true
h : of' l₁ ~ of' l₂
⊢ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
α : Type u_1
l₁ l₂ : Lists' α true
⊢ of' l₁ ~ of' l₂ ↔ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
refine' ⟨fun h => _, fun ⟨h₁, h₂⟩ => Equiv.antisymm h₁ h₂⟩
case refl
α : Type u_1
l₁ : Lists' α true
⊢ l₁ ⊆ l₁ ∧ l₁ ⊆ l₁

case antisymm
α : Type u_1
l₁ l₂ : Lists' α true
h₁ : Lists'.Subset l₁ l₂
h₂ : Lists'.Subset l₂ l₁
⊢ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
α : Type u_1
l₁ l₂ : Lists' α true
h : of' l₁ ~ of' l₂
⊢ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
cases' h with _ _ _ h₁ h₂
no goals
case antisymm
α : Type u_1
l₁ l₂ : Lists' α true
h₁ : Lists'.Subset l₁ l₂
h₂ : Lists'.Subset l₂ l₁
⊢ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
. exact ⟨h₁, h₂⟩
no goals
case refl
α : Type u_1
l₁ : Lists' α true
⊢ l₁ ⊆ l₁ ∧ l₁ ⊆ l₁
simp [Lists'.Subset.refl]
no goals
case antisymm
α : Type u_1
l₁ l₂ : Lists' α true
h₁ : Lists'.Subset l₁ l₂
h₂ : Lists'.Subset l₂ l₁
⊢ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
exact ⟨h₁, h₂⟩