α : 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 H0
α : Type u
β : Type v
γ : Type w
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists []) (reverse (sublists [])) → l₁ ++ l₂ ~ []

case H1
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists l') (reverse (sublists l')) → l₁ ++ l₂ ~ l'
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists (l' ++ [a])) (reverse (sublists (l' ++ [a]))) → l₁ ++ l₂ ~ l' ++ [a]
α : Type u
β : Type v
γ : Type w
l : List α
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists l) (reverse (sublists l)) → l₁ ++ l₂ ~ l
induction' l using List.reverseRecOn with l' a ih
case H1
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists l') (reverse (sublists l')) → l₁ ++ l₂ ~ l'
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists (l' ++ [a])) (reverse (sublists (l' ++ [a]))) → l₁ ++ l₂ ~ l' ++ [a]
case H0
α : Type u
β : Type v
γ : Type w
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists []) (reverse (sublists [])) → l₁ ++ l₂ ~ []

case H1
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists l') (reverse (sublists l')) → l₁ ++ l₂ ~ l'
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists (l' ++ [a])) (reverse (sublists (l' ++ [a]))) → l₁ ++ l₂ ~ l' ++ [a]
. intro l₁ l₂ h
  simp at h
  simp [h]
case H0
α : Type u
β : Type v
γ : Type w
l₁ l₂ : List α
h : (l₁, l₂) ∈ zip (sublists []) (reverse (sublists []))
⊢ l₁ ++ l₂ ~ []
case H0
α : Type u
β : Type v
γ : Type w
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists []) (reverse (sublists [])) → l₁ ++ l₂ ~ []
intro l₁ l₂ h
case H0
α : Type u
β : Type v
γ : Type w
l₁ l₂ : List α
h : l₁ = [] ∧ l₂ = []
⊢ l₁ ++ l₂ ~ []
case H0
α : Type u
β : Type v
γ : Type w
l₁ l₂ : List α
h : (l₁, l₂) ∈ zip (sublists []) (reverse (sublists []))
⊢ l₁ ++ l₂ ~ []
simp at h
no goals
case H0
α : Type u
β : Type v
γ : Type w
l₁ l₂ : List α
h : l₁ = [] ∧ l₂ = []
⊢ l₁ ++ l₂ ~ []
simp [h]
case H1
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists l') (reverse (sublists l')) → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h : (l₁, l₂) ∈ zip (sublists (l' ++ [a])) (reverse (sublists (l' ++ [a])))
⊢ l₁ ++ l₂ ~ l' ++ [a]
case H1
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists l') (reverse (sublists l')) → l₁ ++ l₂ ~ l'
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists (l' ++ [a])) (reverse (sublists (l' ++ [a]))) → l₁ ++ l₂ ~ l' ++ [a]
intro l₁ l₂ h
case H1
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists l') (reverse (sublists l')) → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    map (Prod.map id fun x => x ++ [a]) (zip (sublists l') (reverse (sublists l'))) ++
      map (Prod.map (fun x => x ++ [a]) id) (zip (sublists l') (reverse (sublists l')))
⊢ l₁ ++ l₂ ~ l' ++ [a]
case H1
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists l') (reverse (sublists l')) → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h : (l₁, l₂) ∈ zip (sublists (l' ++ [a])) (reverse (sublists (l' ++ [a])))
⊢ l₁ ++ l₂ ~ l' ++ [a]
rw [sublists_concat, reverse_append, zip_append, ← map_reverse, zip_map_right,
  zip_map_left] at * <;> [skip; simp]
case H1
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
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')) ∧ id a_1 = l₁ ∧ b ++ [a] = l₂) ∨
    ∃ a_1 b, (a_1, b) ∈ zip (sublists l') (reverse (sublists l')) ∧ a_1 ++ [a] = l₁ ∧ id b = l₂
⊢ l₁ ++ l₂ ~ l' ++ [a]
case H1
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ zip (sublists l') (reverse (sublists l')) → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    map (Prod.map id fun x => x ++ [a]) (zip (sublists l') (reverse (sublists l'))) ++
      map (Prod.map (fun x => x ++ [a]) id) (zip (sublists l') (reverse (sublists l')))
⊢ l₁ ++ l₂ ~ l' ++ [a]
simp only [Prod.mk.inj_iff, mem_map, mem_append, Prod.map_mk, Prod.exists] at h
case H1.inl.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
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'))
⊢ id l₁ ++ (l₂' ++ [a]) ~ l' ++ [a]

case H1.inr.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
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] ++ id l₂ ~ l' ++ [a]
case H1
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
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')) ∧ id a_1 = l₁ ∧ b ++ [a] = l₂) ∨
    ∃ a_1 b, (a_1, b) ∈ zip (sublists l') (reverse (sublists l')) ∧ a_1 ++ [a] = l₁ ∧ id b = l₂
⊢ l₁ ++ l₂ ~ l' ++ [a]
rcases h with (⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', l₂, h, rfl, rfl⟩)
case H1.inl.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
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'))
⊢ id l₁ ++ l₂' ++ [a] ~ l' ++ [a]
case H1.inl.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
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'))
⊢ id l₁ ++ (l₂' ++ [a]) ~ l' ++ [a]
rw [← append_assoc]
no goals
case H1.inl.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
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'))
⊢ id l₁ ++ l₂' ++ [a] ~ l' ++ [a]
exact (ih _ _ h).append_right _
case H1.inr.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
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] ++ id l₂) ~ l' ++ [a]
case H1.inr.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
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] ++ id l₂ ~ l' ++ [a]
rw [append_assoc]
case H1.inr.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
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₁' ++ (id l₂ ++ [a]) ~ l' ++ [a]
case H1.inr.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
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] ++ id l₂) ~ l' ++ [a]
apply (perm_append_comm.append_left _).trans
case H1.inr.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
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₁' ++ id l₂ ++ [a] ~ l' ++ [a]
case H1.inr.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
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₁' ++ (id l₂ ++ [a]) ~ l' ++ [a]
rw [← append_assoc]
no goals
case H1.inr.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
l' : List α
a : α
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₁' ++ id l₂ ++ [a] ~ l' ++ [a]
exact (ih _ _ h).append_right _