α : Type u
β : Type v
γ : Type w
l : List α
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists' l) (reverse (sublists' l)) → l₁ ++ l₂ ~ l
α : Type u
β : Type v
γ : Type w
l : List α
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ revzip (sublists' l) → l₁ ++ l₂ ~ l
rw [revzip]
case nil
α : Type u
β : Type v
γ : Type w
l₁ l₂ : List α
h : (l₁, l₂) ∈ zip (sublists' []) (reverse (sublists' []))
⊢ l₁ ++ l₂ ~ []

case cons
α : Type u
β : Type v
γ : Type w
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists' l) (reverse (sublists' l)) → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h : (l₁, l₂) ∈ zip (sublists' (a :: l)) (reverse (sublists' (a :: l)))
⊢ l₁ ++ l₂ ~ a :: l
α : Type u
β : Type v
γ : Type w
l : List α
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists' l) (reverse (sublists' l)) → l₁ ++ l₂ ~ l
induction' l with a l IH <;> intro l₁ l₂ h
case nil
α : Type u
β : Type v
γ : Type w
l₁ l₂ : List α
h : l₁ = [] ∧ l₂ = []
⊢ l₁ ++ l₂ ~ []
case nil
α : Type u
β : Type v
γ : Type w
l₁ l₂ : List α
h : (l₁, l₂) ∈ zip (sublists' []) (reverse (sublists' []))
⊢ l₁ ++ l₂ ~ []
simp at h
no goals
case nil
α : Type u
β : Type v
γ : Type w
l₁ l₂ : List α
h : l₁ = [] ∧ l₂ = []
⊢ l₁ ++ l₂ ~ []
simp [h]
case cons
α : Type u
β : Type v
γ : Type w
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists' l) (reverse (sublists' l)) → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h :
  (∃ a_1 b, (a_1, b) ∈ zip (sublists' l) (reverse (sublists' l)) ∧ a_1 = l₁ ∧ a :: b = l₂) ∨
    ∃ a_1, (a_1, l₂) ∈ zip (sublists' l) (reverse (sublists' l)) ∧ a :: a_1 = l₁
⊢ l₁ ++ l₂ ~ a :: l
case cons
α : Type u
β : Type v
γ : Type w
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists' l) (reverse (sublists' l)) → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h : (l₁, l₂) ∈ zip (sublists' (a :: l)) (reverse (sublists' (a :: l)))
⊢ l₁ ++ l₂ ~ a :: l
rw [sublists'_cons, reverse_append, zip_append, ← map_reverse, zip_map_right, zip_map_left] at *
  <;> [simp at h; simp]
case cons.inl.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists' l) (reverse (sublists' l)) → l₁ ++ l₂ ~ l
l₁ l₂' : List α
h : (l₁, l₂') ∈ zip (sublists' l) (reverse (sublists' l))
⊢ l₁ ++ a :: l₂' ~ a :: l

case cons.inr.intro.intro
α : Type u
β : Type v
γ : Type w
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists' l) (reverse (sublists' l)) → l₁ ++ l₂ ~ l
l₂ l₁' : List α
h : (l₁', l₂) ∈ zip (sublists' l) (reverse (sublists' l))
⊢ a :: l₁' ++ l₂ ~ a :: l
case cons
α : Type u
β : Type v
γ : Type w
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists' l) (reverse (sublists' l)) → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h :
  (∃ a_1 b, (a_1, b) ∈ zip (sublists' l) (reverse (sublists' l)) ∧ a_1 = l₁ ∧ a :: b = l₂) ∨
    ∃ a_1, (a_1, l₂) ∈ zip (sublists' l) (reverse (sublists' l)) ∧ a :: a_1 = l₁
⊢ l₁ ++ l₂ ~ a :: l
rcases h with (⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', h, rfl⟩)
no goals
case cons.inl.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists' l) (reverse (sublists' l)) → l₁ ++ l₂ ~ l
l₁ l₂' : List α
h : (l₁, l₂') ∈ zip (sublists' l) (reverse (sublists' l))
⊢ l₁ ++ a :: l₂' ~ a :: l
exact perm_middle.trans ((IH _ _ h).cons _)
no goals
case cons.inr.intro.intro
α : Type u
β : Type v
γ : Type w
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists' l) (reverse (sublists' l)) → l₁ ++ l₂ ~ l
l₂ l₁' : List α
h : (l₁', l₂) ∈ zip (sublists' l) (reverse (sublists' l))
⊢ a :: l₁' ++ l₂ ~ a :: l
exact (IH _ _ h).cons _