case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁ l₂ t₁ : List α
a : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
ih : List.union l₁✝ t₁ ~ List.union l₂✝ t₁
⊢ List.insert a (List.union l₁✝ t₁) ~ List.insert a (List.union l₂✝ t₁)

case swap
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ t₁ : List α
x✝ y✝ : α
l✝ : List α
⊢ List.insert y✝ (List.insert x✝ (List.union l✝ t₁)) ~ List.insert x✝ (List.insert y✝ (List.union l✝ t₁))

case trans
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁ l₂ t₁ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih_1 : List.union l₁✝ t₁ ~ List.union l₂✝ t₁
ih_2 : List.union l₂✝ t₁ ~ List.union l₃✝ t₁
⊢ List.union l₁✝ t₁ ~ List.union l₃✝ t₁
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ t₁ : List α
h : l₁ ~ l₂
⊢ List.union l₁ t₁ ~ List.union l₂ t₁
induction' h with a _ _ _ ih _ _ _ _ _ _ _ _ ih_1 ih_2 <;> try simp
case trans
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁ l₂ t₁ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih_1 : List.union l₁✝ t₁ ~ List.union l₂✝ t₁
ih_2 : List.union l₂✝ t₁ ~ List.union l₃✝ t₁
⊢ List.union l₁✝ t₁ ~ List.union l₃✝ t₁
case trans
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁ l₂ t₁ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih_1 : List.union l₁✝ t₁ ~ List.union l₂✝ t₁
ih_2 : List.union l₂✝ t₁ ~ List.union l₃✝ t₁
⊢ List.union l₁✝ t₁ ~ List.union l₃✝ t₁
simp
no goals
case cons
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁ l₂ t₁ : List α
a : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
ih : List.union l₁✝ t₁ ~ List.union l₂✝ t₁
⊢ List.insert a (List.union l₁✝ t₁) ~ List.insert a (List.union l₂✝ t₁)
exact ih.insert a
no goals
case swap
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
inst✝ : DecidableEq α
l₁ l₂ t₁ : List α
x✝ y✝ : α
l✝ : List α
⊢ List.insert y✝ (List.insert x✝ (List.union l✝ t₁)) ~ List.insert x✝ (List.insert y✝ (List.union l✝ t₁))
apply perm_insert_swap
no goals
case trans
α : Type uu
β : Type vv
l₁✝¹ l₂✝¹ : List α
inst✝ : DecidableEq α
l₁ l₂ t₁ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih_1 : List.union l₁✝ t₁ ~ List.union l₂✝ t₁
ih_2 : List.union l₂✝ t₁ ~ List.union l₃✝ t₁
⊢ List.union l₁✝ t₁ ~ List.union l₃✝ t₁
exact ih_1.trans ih_2