α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₁ l₂ r₁ r₂ s₁ : List α
e₁ : l₁ ++ a :: r₁ = s₁
⊢ s₁ ~ l₂ ++ a :: r₂ → l₁ ++ r₁ ~ l₂ ++ r₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₁ l₂ r₁ r₂ : List α
⊢ l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂ → l₁ ++ r₁ ~ l₂ ++ r₂
generalize e₁ : l₁ ++ a :: r₁ = s₁
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₁ l₂ r₁ r₂ s₁ : List α
e₁ : l₁ ++ a :: r₁ = s₁
s₂ : List α
e₂ : l₂ ++ a :: r₂ = s₂
⊢ s₁ ~ s₂ → l₁ ++ r₁ ~ l₂ ++ r₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₁ l₂ r₁ r₂ s₁ : List α
e₁ : l₁ ++ a :: r₁ = s₁
⊢ s₁ ~ l₂ ++ a :: r₂ → l₁ ++ r₁ ~ l₂ ++ r₂
generalize e₂ : l₂ ++ a :: r₂ = s₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₁ l₂ r₁ r₂ s₁ : List α
e₁ : l₁ ++ a :: r₁ = s₁
s₂ : List α
e₂ : l₂ ++ a :: r₂ = s₂
p : s₁ ~ s₂
⊢ l₁ ++ r₁ ~ l₂ ++ r₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₁ l₂ r₁ r₂ s₁ : List α
e₁ : l₁ ++ a :: r₁ = s₁
s₂ : List α
e₂ : l₂ ++ a :: r₂ = s₂
⊢ s₁ ~ s₂ → l₁ ++ r₁ ~ l₂ ++ r₂
intro p
α : Type uu
β : Type vv
l₁ l₂ : List α
a : α
s₁ s₂ : List α
p : s₁ ~ s₂
⊢ ∀ {l₁ l₂ r₁ r₂ : List α}, l₁ ++ a :: r₁ = s₁ → l₂ ++ a :: r₂ = s₂ → l₁ ++ r₁ ~ l₂ ++ r₂
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
a : α
l₁ l₂ r₁ r₂ s₁ : List α
e₁ : l₁ ++ a :: r₁ = s₁
s₂ : List α
e₂ : l₂ ++ a :: r₂ = s₂
p : s₁ ~ s₂
⊢ l₁ ++ r₁ ~ l₂ ++ r₂
revert l₁ l₂ r₁ r₂ e₁ e₂
α : Type uu
a : α
s₁ s₂ : List α
p : s₁ ~ s₂
⊢ ∀ {l₁ l₂ r₁ r₂ : List α}, l₁ ++ a :: r₁ = s₁ → l₂ ++ a :: r₂ = s₂ → l₁ ++ r₁ ~ l₂ ++ r₂
α : Type uu
β : Type vv
l₁ l₂ : List α
a : α
s₁ s₂ : List α
p : s₁ ~ s₂
⊢ ∀ {l₁ l₂ r₁ r₂ : List α}, l₁ ++ a :: r₁ = s₁ → l₂ ++ a :: r₂ = s₂ → l₁ ++ r₁ ~ l₂ ++ r₂
clear l₁ l₂ β
α : Type uu
a : α
s₁ s₂ : List α
p : s₁ ~ s₂
⊢ ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = s₁ → x_1 ++ a :: x_3 = s₂ → x ++ x_2 ~ x_1 ++ x_3
α : Type uu
a : α
s₁ s₂ : List α
p : s₁ ~ s₂
⊢ ∀ {l₁ l₂ r₁ r₂ : List α}, l₁ ++ a :: r₁ = s₁ → l₂ ++ a :: r₂ = s₂ → l₁ ++ r₁ ~ l₂ ++ r₂
show ∀ _ _ _ _, _
case refine_1
α : Type uu
a : α
s₁ s₂ : List α
p : s₁ ~ s₂
l₁ l₂ r₁ r₂ : List α
e₁ : l₁ ++ a :: r₁ = []
e₂ : l₂ ++ a :: r₂ = []
⊢ l₁ ++ r₁ ~ l₂ ++ r₂

case refine_2
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
x : α
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
l₁ l₂ r₁ r₂ : List α
e₁ : l₁ ++ a :: r₁ = x :: t₁
e₂ : l₂ ++ a :: r₂ = x :: t₂
⊢ l₁ ++ r₁ ~ l₂ ++ r₂

case refine_3
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
x y : α
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
l₁ l₂ r₁ r₂ : List α
e₁ : l₁ ++ a :: r₁ = y :: x :: t₁
e₂ : l₂ ++ a :: r₂ = x :: y :: t₂
⊢ l₁ ++ r₁ ~ l₂ ++ r₂

case refine_4
α : Type uu
a : α
s₁ s₂ : List α
p : s₁ ~ s₂
t₁ t₂ t₃ : List α
p₁ : t₁ ~ t₂
p₂ : t₂ ~ t₃
IH₁ : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
IH₂ : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₂ → x_1 ++ a :: x_3 = t₃ → x ++ x_2 ~ x_1 ++ x_3
l₁ l₂ r₁ r₂ : List α
e₁ : l₁ ++ a :: r₁ = t₁
e₂ : l₂ ++ a :: r₂ = t₃
⊢ l₁ ++ r₁ ~ l₂ ++ r₂
α : Type uu
a : α
s₁ s₂ : List α
p : s₁ ~ s₂
⊢ ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = s₁ → x_1 ++ a :: x_3 = s₂ → x ++ x_2 ~ x_1 ++ x_3
refine
    perm_induction_on p ?_ (fun x t₁ t₂ p IH => ?_) (fun x y t₁ t₂ p IH => ?_)
      fun t₁ t₂ t₃ p₁ p₂ IH₁ IH₂ => ?_
  <;> intro l₁ l₂ r₁ r₂ e₁ e₂
case refine_1
α : Type uu
a : α
s₁ s₂ : List α
p : s₁ ~ s₂
l₁ l₂ r₁ r₂ : List α
e₁ : l₁ ++ a :: r₁ = []
e₂ : l₂ ++ a :: r₂ = []
⊢ a ∈ []
case refine_1
α : Type uu
a : α
s₁ s₂ : List α
p : s₁ ~ s₂
l₁ l₂ r₁ r₂ : List α
e₁ : l₁ ++ a :: r₁ = []
e₂ : l₂ ++ a :: r₂ = []
⊢ l₁ ++ r₁ ~ l₂ ++ r₂
apply (not_mem_nil a).elim
case refine_1
α : Type uu
a : α
s₁ s₂ : List α
p : s₁ ~ s₂
l₁ l₂ r₁ r₂ : List α
e₁ : l₁ ++ a :: r₁ = []
e₂ : l₂ ++ a :: r₂ = []
⊢ a ∈ l₁ ++ a :: r₁
case refine_1
α : Type uu
a : α
s₁ s₂ : List α
p : s₁ ~ s₂
l₁ l₂ r₁ r₂ : List α
e₁ : l₁ ++ a :: r₁ = []
e₂ : l₂ ++ a :: r₂ = []
⊢ a ∈ []
rw [← e₁]
no goals
case refine_1
α : Type uu
a : α
s₁ s₂ : List α
p : s₁ ~ s₂
l₁ l₂ r₁ r₂ : List α
e₁ : l₁ ++ a :: r₁ = []
e₂ : l₂ ++ a :: r₂ = []
⊢ a ∈ l₁ ++ a :: r₁
simp
case refine_2.nil.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
tail_eq✝¹ : r₁ = t₁
tail_eq✝ : r₂ = t₂
head_eq✝ : a = a
⊢ [] ++ r₁ ~ [] ++ r₂

case refine_2.nil.cons
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
z : α
l₂ : List α
tail_eq✝¹ : r₁ = t₁
tail_eq✝ : l₂ ++ a :: r₂ = t₂
head_eq✝ : z = a
⊢ [] ++ r₁ ~ z :: l₂ ++ r₂

case refine_2.cons.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
y : α
l₁ : List α
tail_eq✝¹ : l₁ ++ a :: r₁ = t₁
tail_eq✝ : r₂ = t₂
head_eq✝ : a = y
⊢ y :: l₁ ++ r₁ ~ [] ++ r₂

case refine_2.cons.cons
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
y : α
l₁ : List α
z : α
l₂ : List α
tail_eq✝¹ : l₁ ++ a :: r₁ = t₁
tail_eq✝ : l₂ ++ a :: r₂ = t₂
head_eq✝ : z = y
⊢ y :: l₁ ++ r₁ ~ z :: l₂ ++ r₂
case refine_2
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
x : α
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
l₁ l₂ r₁ r₂ : List α
e₁ : l₁ ++ a :: r₁ = x :: t₁
e₂ : l₂ ++ a :: r₂ = x :: t₂
⊢ l₁ ++ r₁ ~ l₂ ++ r₂
cases' l₁ with y l₁ <;> cases' l₂ with z l₂ <;> dsimp at e₁ e₂ <;> injections <;> subst x
case refine_2.nil.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
r₁ r₂ : List α
head_eq✝ : a = a
p : r₁ ~ r₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = r₁ → x_1 ++ a :: x_3 = r₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ [] ++ r₁ ~ [] ++ r₂
case refine_2.nil.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
tail_eq✝¹ : r₁ = t₁
tail_eq✝ : r₂ = t₂
head_eq✝ : a = a
⊢ [] ++ r₁ ~ [] ++ r₂
substs t₁ t₂
no goals
case refine_2.nil.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
r₁ r₂ : List α
head_eq✝ : a = a
p : r₁ ~ r₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = r₁ → x_1 ++ a :: x_3 = r₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ [] ++ r₁ ~ [] ++ r₂
exact p
case refine_2.nil.cons
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
r₁ r₂ l₂ : List α
p : r₁ ~ l₂ ++ a :: r₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = r₁ → x_1 ++ a :: x_3 = l₂ ++ a :: r₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ [] ++ r₁ ~ a :: l₂ ++ r₂
case refine_2.nil.cons
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
z : α
l₂ : List α
tail_eq✝¹ : r₁ = t₁
tail_eq✝ : l₂ ++ a :: r₂ = t₂
head_eq✝ : z = a
⊢ [] ++ r₁ ~ z :: l₂ ++ r₂
substs z t₁ t₂
no goals
case refine_2.nil.cons
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
r₁ r₂ l₂ : List α
p : r₁ ~ l₂ ++ a :: r₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = r₁ → x_1 ++ a :: x_3 = l₂ ++ a :: r₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ [] ++ r₁ ~ a :: l₂ ++ r₂
exact p.trans perm_middle
case refine_2.cons.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
r₁ r₂ l₁ : List α
p : l₁ ++ a :: r₁ ~ r₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = l₁ ++ a :: r₁ → x_1 ++ a :: x_3 = r₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ a :: l₁ ++ r₁ ~ [] ++ r₂
case refine_2.cons.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
y : α
l₁ : List α
tail_eq✝¹ : l₁ ++ a :: r₁ = t₁
tail_eq✝ : r₂ = t₂
head_eq✝ : a = y
⊢ y :: l₁ ++ r₁ ~ [] ++ r₂
substs y t₁ t₂
no goals
case refine_2.cons.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
r₁ r₂ l₁ : List α
p : l₁ ++ a :: r₁ ~ r₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = l₁ ++ a :: r₁ → x_1 ++ a :: x_3 = r₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ a :: l₁ ++ r₁ ~ [] ++ r₂
exact perm_middle.symm.trans p
case refine_2.cons.cons
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
r₁ r₂ : List α
y : α
l₁ l₂ : List α
p : l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = l₁ ++ a :: r₁ → x_1 ++ a :: x_3 = l₂ ++ a :: r₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ y :: l₁ ++ r₁ ~ y :: l₂ ++ r₂
case refine_2.cons.cons
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
y : α
l₁ : List α
z : α
l₂ : List α
tail_eq✝¹ : l₁ ++ a :: r₁ = t₁
tail_eq✝ : l₂ ++ a :: r₂ = t₂
head_eq✝ : z = y
⊢ y :: l₁ ++ r₁ ~ z :: l₂ ++ r₂
substs z t₁ t₂
no goals
case refine_2.cons.cons
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
r₁ r₂ : List α
y : α
l₁ l₂ : List α
p : l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = l₁ ++ a :: r₁ → x_1 ++ a :: x_3 = l₂ ++ a :: r₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ y :: l₁ ++ r₁ ~ y :: l₂ ++ r₂
exact (IH _ _ _ _ rfl rfl).cons y
case refine_3.nil.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
tail_eq✝¹ : r₁ = a :: t₁
tail_eq✝ : r₂ = a :: t₂
⊢ [] ++ r₁ ~ [] ++ r₂

case refine_3.nil.cons.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
u : α
tail_eq✝¹ : r₂ = t₂
tail_eq✝ : r₁ = u :: t₁
head_eq✝ : a = a
⊢ [] ++ r₁ ~ [u] ++ r₂

case refine_3.nil.cons.cons
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
u v : α
l₂ : List α
tail_eq✝¹ : l₂ ++ a :: r₂ = t₂
tail_eq✝ : r₁ = u :: t₁
head_eq✝ : v = a
⊢ [] ++ r₁ ~ u :: v :: l₂ ++ r₂

case refine_3.cons.nil.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
y : α
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
tail_eq✝¹ : r₁ = t₁
tail_eq✝ : r₂ = y :: t₂
head_eq✝ : a = a
⊢ [y] ++ r₁ ~ [] ++ r₂

case refine_3.cons.nil.cons.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
y : α
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
u : α
tail_eq✝¹ : r₁ = t₁
head_eq✝¹ : a = y
tail_eq✝ : r₂ = t₂
head_eq✝ : u = a
⊢ [y] ++ r₁ ~ [u] ++ r₂

case refine_3.cons.nil.cons.cons
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
y : α
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
u v : α
l₂ : List α
tail_eq✝¹ : r₁ = t₁
head_eq✝¹ : v = y
tail_eq✝ : l₂ ++ a :: r₂ = t₂
head_eq✝ : u = a
⊢ [y] ++ r₁ ~ u :: v :: l₂ ++ r₂

case refine_3.cons.cons.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
y : α
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
z : α
l₁ : List α
tail_eq✝¹ : l₁ ++ a :: r₁ = t₁
tail_eq✝ : r₂ = y :: t₂
head_eq✝ : a = z
⊢ y :: z :: l₁ ++ r₁ ~ [] ++ r₂

case refine_3.cons.cons.cons.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
y : α
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
z : α
l₁ : List α
u : α
tail_eq✝¹ : l₁ ++ a :: r₁ = t₁
head_eq✝¹ : a = y
tail_eq✝ : r₂ = t₂
head_eq✝ : u = z
⊢ y :: z :: l₁ ++ r₁ ~ [u] ++ r₂

case refine_3.cons.cons.cons.cons
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
y : α
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
z : α
l₁ : List α
u v : α
l₂ : List α
tail_eq✝¹ : l₁ ++ a :: r₁ = t₁
head_eq✝¹ : v = y
tail_eq✝ : l₂ ++ a :: r₂ = t₂
head_eq✝ : u = z
⊢ y :: z :: l₁ ++ r₁ ~ u :: v :: l₂ ++ r₂
case refine_3
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
x y : α
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
l₁ l₂ r₁ r₂ : List α
e₁ : l₁ ++ a :: r₁ = y :: x :: t₁
e₂ : l₂ ++ a :: r₂ = x :: y :: t₂
⊢ l₁ ++ r₁ ~ l₂ ++ r₂
rcases l₁ with (_ | ⟨y, _ | ⟨z, l₁⟩⟩) <;> rcases l₂ with (_ | ⟨u, _ | ⟨v, l₂⟩⟩) <;>
      dsimp at e₁ e₂ <;> injections <;> substs x y
case refine_3.nil.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ [] ++ a :: t₁ ~ [] ++ a :: t₂
case refine_3.nil.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
tail_eq✝¹ : r₁ = a :: t₁
tail_eq✝ : r₂ = a :: t₂
⊢ [] ++ r₁ ~ [] ++ r₂
substs r₁ r₂
no goals
case refine_3.nil.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ [] ++ a :: t₁ ~ [] ++ a :: t₂
exact p.cons a
case refine_3.nil.cons.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
u : α
head_eq✝ : a = a
⊢ [] ++ u :: t₁ ~ [u] ++ t₂
case refine_3.nil.cons.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
u : α
tail_eq✝¹ : r₂ = t₂
tail_eq✝ : r₁ = u :: t₁
head_eq✝ : a = a
⊢ [] ++ r₁ ~ [u] ++ r₂
substs r₁ r₂
no goals
case refine_3.nil.cons.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
u : α
head_eq✝ : a = a
⊢ [] ++ u :: t₁ ~ [u] ++ t₂
exact p.cons u
case refine_3.nil.cons.cons
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₁ r₂ : List α
u : α
l₂ : List α
p : t₁ ~ l₂ ++ a :: r₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = l₂ ++ a :: r₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ [] ++ u :: t₁ ~ u :: a :: l₂ ++ r₂
case refine_3.nil.cons.cons
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
u v : α
l₂ : List α
tail_eq✝¹ : l₂ ++ a :: r₂ = t₂
tail_eq✝ : r₁ = u :: t₁
head_eq✝ : v = a
⊢ [] ++ r₁ ~ u :: v :: l₂ ++ r₂
substs r₁ v t₂
no goals
case refine_3.nil.cons.cons
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₁ r₂ : List α
u : α
l₂ : List α
p : t₁ ~ l₂ ++ a :: r₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = l₂ ++ a :: r₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ [] ++ u :: t₁ ~ u :: a :: l₂ ++ r₂
exact (p.trans perm_middle).cons u
case refine_3.cons.nil.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
y : α
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
head_eq✝ : a = a
⊢ [y] ++ t₁ ~ [] ++ y :: t₂
case refine_3.cons.nil.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
y : α
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
tail_eq✝¹ : r₁ = t₁
tail_eq✝ : r₂ = y :: t₂
head_eq✝ : a = a
⊢ [y] ++ r₁ ~ [] ++ r₂
substs r₁ r₂
no goals
case refine_3.cons.nil.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
y : α
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
head_eq✝ : a = a
⊢ [y] ++ t₁ ~ [] ++ y :: t₂
exact p.cons y
case refine_3.cons.nil.cons.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ [a] ++ t₁ ~ [a] ++ t₂
case refine_3.cons.nil.cons.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
y : α
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
u : α
tail_eq✝¹ : r₁ = t₁
head_eq✝¹ : a = y
tail_eq✝ : r₂ = t₂
head_eq✝ : u = a
⊢ [y] ++ r₁ ~ [u] ++ r₂
substs r₁ r₂ y u
no goals
case refine_3.cons.nil.cons.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ [a] ++ t₁ ~ [a] ++ t₂
exact p.cons a
case refine_3.cons.nil.cons.cons
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
y : α
t₁ r₂ l₂ : List α
p : t₁ ~ l₂ ++ a :: r₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = l₂ ++ a :: r₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ [y] ++ t₁ ~ a :: y :: l₂ ++ r₂
case refine_3.cons.nil.cons.cons
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
y : α
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
u v : α
l₂ : List α
tail_eq✝¹ : r₁ = t₁
head_eq✝¹ : v = y
tail_eq✝ : l₂ ++ a :: r₂ = t₂
head_eq✝ : u = a
⊢ [y] ++ r₁ ~ u :: v :: l₂ ++ r₂
substs r₁ u v t₂
no goals
case refine_3.cons.nil.cons.cons
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
y : α
t₁ r₂ l₂ : List α
p : t₁ ~ l₂ ++ a :: r₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = l₂ ++ a :: r₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ [y] ++ t₁ ~ a :: y :: l₂ ++ r₂
exact ((p.trans perm_middle).cons y).trans (swap _ _ _)
case refine_3.cons.cons.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
y : α
t₂ r₁ l₁ : List α
p : l₁ ++ a :: r₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = l₁ ++ a :: r₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ y :: a :: l₁ ++ r₁ ~ [] ++ y :: t₂
case refine_3.cons.cons.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
y : α
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
z : α
l₁ : List α
tail_eq✝¹ : l₁ ++ a :: r₁ = t₁
tail_eq✝ : r₂ = y :: t₂
head_eq✝ : a = z
⊢ y :: z :: l₁ ++ r₁ ~ [] ++ r₂
substs r₂ z t₁
no goals
case refine_3.cons.cons.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
y : α
t₂ r₁ l₁ : List α
p : l₁ ++ a :: r₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = l₁ ++ a :: r₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ y :: a :: l₁ ++ r₁ ~ [] ++ y :: t₂
exact (perm_middle.symm.trans p).cons y
case refine_3.cons.cons.cons.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₂ r₁ l₁ : List α
u : α
p : l₁ ++ a :: r₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = l₁ ++ a :: r₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ a :: u :: l₁ ++ r₁ ~ [u] ++ t₂
case refine_3.cons.cons.cons.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
y : α
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
z : α
l₁ : List α
u : α
tail_eq✝¹ : l₁ ++ a :: r₁ = t₁
head_eq✝¹ : a = y
tail_eq✝ : r₂ = t₂
head_eq✝ : u = z
⊢ y :: z :: l₁ ++ r₁ ~ [u] ++ r₂
substs r₂ y z t₁
no goals
case refine_3.cons.cons.cons.nil
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
t₂ r₁ l₁ : List α
u : α
p : l₁ ++ a :: r₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = l₁ ++ a :: r₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ a :: u :: l₁ ++ r₁ ~ [u] ++ t₂
exact (swap _ _ _).trans ((perm_middle.symm.trans p).cons u)
case refine_3.cons.cons.cons.cons
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
y : α
r₁ r₂ : List α
z : α
l₁ l₂ : List α
p : l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = l₁ ++ a :: r₁ → x_1 ++ a :: x_3 = l₂ ++ a :: r₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ y :: z :: l₁ ++ r₁ ~ z :: y :: l₂ ++ r₂
case refine_3.cons.cons.cons.cons
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
y : α
t₁ t₂ : List α
p : t₁ ~ t₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
r₁ r₂ : List α
z : α
l₁ : List α
u v : α
l₂ : List α
tail_eq✝¹ : l₁ ++ a :: r₁ = t₁
head_eq✝¹ : v = y
tail_eq✝ : l₂ ++ a :: r₂ = t₂
head_eq✝ : u = z
⊢ y :: z :: l₁ ++ r₁ ~ u :: v :: l₂ ++ r₂
substs u v t₁ t₂
no goals
case refine_3.cons.cons.cons.cons
α : Type uu
a : α
s₁ s₂ : List α
p✝ : s₁ ~ s₂
y : α
r₁ r₂ : List α
z : α
l₁ l₂ : List α
p : l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂
IH : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = l₁ ++ a :: r₁ → x_1 ++ a :: x_3 = l₂ ++ a :: r₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ y :: z :: l₁ ++ r₁ ~ z :: y :: l₂ ++ r₂
exact (IH _ _ _ _ rfl rfl).swap' _ _
case refine_4
α : Type uu
a : α
s₁ s₂ : List α
p : s₁ ~ s₂
t₂ l₁ l₂ r₁ r₂ : List α
p₁ : l₁ ++ a :: r₁ ~ t₂
IH₁ : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = l₁ ++ a :: r₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
p₂ : t₂ ~ l₂ ++ a :: r₂
IH₂ : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₂ → x_1 ++ a :: x_3 = l₂ ++ a :: r₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ l₁ ++ r₁ ~ l₂ ++ r₂
case refine_4
α : Type uu
a : α
s₁ s₂ : List α
p : s₁ ~ s₂
t₁ t₂ t₃ : List α
p₁ : t₁ ~ t₂
p₂ : t₂ ~ t₃
IH₁ : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
IH₂ : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₂ → x_1 ++ a :: x_3 = t₃ → x ++ x_2 ~ x_1 ++ x_3
l₁ l₂ r₁ r₂ : List α
e₁ : l₁ ++ a :: r₁ = t₁
e₂ : l₂ ++ a :: r₂ = t₃
⊢ l₁ ++ r₁ ~ l₂ ++ r₂
substs t₁ t₃
case refine_4
α : Type uu
a : α
s₁ s₂ : List α
p : s₁ ~ s₂
t₂ l₁ l₂ r₁ r₂ : List α
p₁ : l₁ ++ a :: r₁ ~ t₂
IH₁ : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = l₁ ++ a :: r₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
p₂ : t₂ ~ l₂ ++ a :: r₂
IH₂ : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₂ → x_1 ++ a :: x_3 = l₂ ++ a :: r₂ → x ++ x_2 ~ x_1 ++ x_3
this : a ∈ t₂
⊢ l₁ ++ r₁ ~ l₂ ++ r₂
case refine_4
α : Type uu
a : α
s₁ s₂ : List α
p : s₁ ~ s₂
t₂ l₁ l₂ r₁ r₂ : List α
p₁ : l₁ ++ a :: r₁ ~ t₂
IH₁ : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = l₁ ++ a :: r₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
p₂ : t₂ ~ l₂ ++ a :: r₂
IH₂ : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₂ → x_1 ++ a :: x_3 = l₂ ++ a :: r₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ l₁ ++ r₁ ~ l₂ ++ r₂
have : a ∈ t₂ := p₁.subset (by simp)
case refine_4.intro.intro
α : Type uu
a : α
s₁ s₂ : List α
p : s₁ ~ s₂
t₂ l₁ l₂✝ r₁ r₂✝ : List α
p₁ : l₁ ++ a :: r₁ ~ t₂
IH₁ : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = l₁ ++ a :: r₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
p₂ : t₂ ~ l₂✝ ++ a :: r₂✝
IH₂ : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₂ → x_1 ++ a :: x_3 = l₂✝ ++ a :: r₂✝ → x ++ x_2 ~ x_1 ++ x_3
this : a ∈ t₂
l₂ r₂ : List α
e₂ : t₂ = l₂ ++ a :: r₂
⊢ l₁ ++ r₁ ~ l₂✝ ++ r₂✝
case refine_4
α : Type uu
a : α
s₁ s₂ : List α
p : s₁ ~ s₂
t₂ l₁ l₂ r₁ r₂ : List α
p₁ : l₁ ++ a :: r₁ ~ t₂
IH₁ : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = l₁ ++ a :: r₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
p₂ : t₂ ~ l₂ ++ a :: r₂
IH₂ : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₂ → x_1 ++ a :: x_3 = l₂ ++ a :: r₂ → x ++ x_2 ~ x_1 ++ x_3
this : a ∈ t₂
⊢ l₁ ++ r₁ ~ l₂ ++ r₂
rcases mem_split this with ⟨l₂, r₂, e₂⟩
case refine_4.intro.intro
α : Type uu
a : α
s₁ s₂ : List α
p : s₁ ~ s₂
l₁ l₂✝ r₁ r₂✝ l₂ r₂ : List α
p₁ : l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂
IH₁ :
  ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = l₁ ++ a :: r₁ → x_1 ++ a :: x_3 = l₂ ++ a :: r₂ → x ++ x_2 ~ x_1 ++ x_3
p₂ : l₂ ++ a :: r₂ ~ l₂✝ ++ a :: r₂✝
IH₂ :
  ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = l₂ ++ a :: r₂ → x_1 ++ a :: x_3 = l₂✝ ++ a :: r₂✝ → x ++ x_2 ~ x_1 ++ x_3
this : a ∈ l₂ ++ a :: r₂
⊢ l₁ ++ r₁ ~ l₂✝ ++ r₂✝
case refine_4.intro.intro
α : Type uu
a : α
s₁ s₂ : List α
p : s₁ ~ s₂
t₂ l₁ l₂✝ r₁ r₂✝ : List α
p₁ : l₁ ++ a :: r₁ ~ t₂
IH₁ : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = l₁ ++ a :: r₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
p₂ : t₂ ~ l₂✝ ++ a :: r₂✝
IH₂ : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₂ → x_1 ++ a :: x_3 = l₂✝ ++ a :: r₂✝ → x ++ x_2 ~ x_1 ++ x_3
this : a ∈ t₂
l₂ r₂ : List α
e₂ : t₂ = l₂ ++ a :: r₂
⊢ l₁ ++ r₁ ~ l₂✝ ++ r₂✝
subst t₂
no goals
case refine_4.intro.intro
α : Type uu
a : α
s₁ s₂ : List α
p : s₁ ~ s₂
l₁ l₂✝ r₁ r₂✝ l₂ r₂ : List α
p₁ : l₁ ++ a :: r₁ ~ l₂ ++ a :: r₂
IH₁ :
  ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = l₁ ++ a :: r₁ → x_1 ++ a :: x_3 = l₂ ++ a :: r₂ → x ++ x_2 ~ x_1 ++ x_3
p₂ : l₂ ++ a :: r₂ ~ l₂✝ ++ a :: r₂✝
IH₂ :
  ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = l₂ ++ a :: r₂ → x_1 ++ a :: x_3 = l₂✝ ++ a :: r₂✝ → x ++ x_2 ~ x_1 ++ x_3
this : a ∈ l₂ ++ a :: r₂
⊢ l₁ ++ r₁ ~ l₂✝ ++ r₂✝
exact (IH₁ _ _ _ _ rfl rfl).trans (IH₂ _ _ _ _ rfl rfl)
no goals
α : Type uu
a : α
s₁ s₂ : List α
p : s₁ ~ s₂
t₂ l₁ l₂ r₁ r₂ : List α
p₁ : l₁ ++ a :: r₁ ~ t₂
IH₁ : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = l₁ ++ a :: r₁ → x_1 ++ a :: x_3 = t₂ → x ++ x_2 ~ x_1 ++ x_3
p₂ : t₂ ~ l₂ ++ a :: r₂
IH₂ : ∀ (x x_1 x_2 x_3 : List α), x ++ a :: x_2 = t₂ → x_1 ++ a :: x_3 = l₂ ++ a :: r₂ → x ++ x_2 ~ x_1 ++ x_3
⊢ a ∈ l₁ ++ a :: r₁
simp