-- Mathlib/Data/List/Sublists.lean
theorem revzip_sublists (l : List α) : ∀ l₁ l₂, (l₁, l₂) ∈ revzip l.sublists → l₁ ++ l₂ ~ l

Proof state:
case nil
α : Type u
l₁ l₂ : List α
h : (l₁, l₂) ∈ [].sublists.zip [].sublists.reverse
⊢ l₁ ++ l₂ ~ []

Tactic:
simp only [sublists_nil, reverse_cons, reverse_nil, nil_append, zip_cons_cons, zip_nil_right,
  mem_cons, Prod.mk.injEq, not_mem_nil, or_false] at h

Result:
case nil
α : Type u
l₁ l₂ : List α
h : l₁ = [] ∧ l₂ = []
⊢ l₁ ++ l₂ ~ []

Proof state:
case append_singleton.inr.intro.intro.intro.intro
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
⊢ l₁' ++ ([a] ++ id l₂) ~ l' ++ [a]

Tactic:
apply (perm_append_comm.append_left _).trans

Result:
case append_singleton.inr.intro.intro.intro.intro
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
⊢ l₁' ++ (id l₂ ++ [a]) ~ l' ++ [a]

Proof state:
case append_singleton
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ (l' ++ [a]).sublists.zip (l' ++ [a]).sublists.reverse → l₁ ++ l₂ ~ l' ++ [a]

Tactic:
intro l₁ l₂ h

Result:
case append_singleton
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h : (l₁, l₂) ∈ (l' ++ [a]).sublists.zip (l' ++ [a]).sublists.reverse
⊢ l₁ ++ l₂ ~ l' ++ [a]

Proof state:
case append_singleton.inl.intro.intro.intro.intro
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂' : List α
h : (l₁, l₂') ∈ l'.sublists.zip l'.sublists.reverse
⊢ id l₁ ++ l₂' ++ [a] ~ l' ++ [a]

Tactic:
exact (ih _ _ h).append_right _

Result:
no goals

Proof state:
case append_singleton.inr.intro.intro.intro.intro
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
⊢ l₁' ++ (id l₂ ++ [a]) ~ l' ++ [a]

Tactic:
rw [← append_assoc]

Result:
case append_singleton.inr.intro.intro.intro.intro
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
⊢ l₁' ++ id l₂ ++ [a] ~ l' ++ [a]

Proof state:
α : Type u
l : List α
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists.zip l.sublists.reverse → l₁ ++ l₂ ~ l

Tactic:
induction' l using List.reverseRecOn with l' a ih

Result:
case nil
α : Type u
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ [].sublists.zip [].sublists.reverse → l₁ ++ l₂ ~ []

case append_singleton
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ (l' ++ [a]).sublists.zip (l' ++ [a]).sublists.reverse → l₁ ++ l₂ ~ l' ++ [a]

Proof state:
case append_singleton
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    map (Prod.map id fun x => x ++ [a]) (l'.sublists.zip l'.sublists.reverse) ++
      map (Prod.map (fun x => x ++ [a]) id) (l'.sublists.zip l'.sublists.reverse)
⊢ l₁ ++ l₂ ~ l' ++ [a]

Tactic:
simp only [Prod.mk.inj_iff, mem_map, mem_append, Prod.map_apply, Prod.exists] at h

Result:
case append_singleton
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (∃ a_1 b, (a_1, b) ∈ l'.sublists.zip l'.sublists.reverse ∧ id a_1 = l₁ ∧ b ++ [a] = l₂) ∨
    ∃ a_1 b, (a_1, b) ∈ l'.sublists.zip l'.sublists.reverse ∧ a_1 ++ [a] = l₁ ∧ id b = l₂
⊢ l₁ ++ l₂ ~ l' ++ [a]

Proof state:
case nil
α : Type u
l₁ l₂ : List α
h : (l₁, l₂) ∈ [].sublists.zip [].sublists.reverse
⊢ l₁ ++ l₂ ~ []

Tactic:
simp? at h says
  simp only [sublists_nil, reverse_cons, reverse_nil, nil_append, zip_cons_cons, zip_nil_right,
    mem_cons, Prod.mk.injEq, not_mem_nil, or_false] at h

Result:
case nil
α : Type u
l₁ l₂ : List α
h : l₁ = [] ∧ l₂ = []
⊢ l₁ ++ l₂ ~ []

Proof state:
case append_singleton
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (∃ a_1 b, (a_1, b) ∈ l'.sublists.zip l'.sublists.reverse ∧ id a_1 = l₁ ∧ b ++ [a] = l₂) ∨
    ∃ a_1 b, (a_1, b) ∈ l'.sublists.zip l'.sublists.reverse ∧ a_1 ++ [a] = l₁ ∧ id b = l₂
⊢ l₁ ++ l₂ ~ l' ++ [a]

Tactic:
rcases h with (⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', l₂, h, rfl, rfl⟩)

Result:
case append_singleton.inl.intro.intro.intro.intro
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂' : List α
h : (l₁, l₂') ∈ l'.sublists.zip l'.sublists.reverse
⊢ id l₁ ++ (l₂' ++ [a]) ~ l' ++ [a]

case append_singleton.inr.intro.intro.intro.intro
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
⊢ l₁' ++ [a] ++ id l₂ ~ l' ++ [a]

Proof state:
case append_singleton.inr.intro.intro.intro.intro
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
⊢ l₁' ++ id l₂ ++ [a] ~ l' ++ [a]

Tactic:
exact (ih _ _ h).append_right _

Result:
no goals

Proof state:
case nil
α : Type u
l₁ l₂ : List α
h : l₁ = [] ∧ l₂ = []
⊢ l₁ ++ l₂ ~ []

Tactic:
simp [h]

Result:
no goals

Proof state:
case append_singleton.inl.intro.intro.intro.intro
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂' : List α
h : (l₁, l₂') ∈ l'.sublists.zip l'.sublists.reverse
⊢ id l₁ ++ (l₂' ++ [a]) ~ l' ++ [a]

Tactic:
rw [← append_assoc]

Result:
case append_singleton.inl.intro.intro.intro.intro
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂' : List α
h : (l₁, l₂') ∈ l'.sublists.zip l'.sublists.reverse
⊢ id l₁ ++ l₂' ++ [a] ~ l' ++ [a]

Proof state:
α : Type u
l : List α
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists.revzip → l₁ ++ l₂ ~ l

Tactic:
rw [revzip]

Result:
α : Type u
l : List α
⊢ ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists.zip l.sublists.reverse → l₁ ++ l₂ ~ l

Proof state:
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂ : List α
h :
  (l₁, l₂) ∈
    (l'.sublists ++ map (fun x => x ++ [a]) l'.sublists).zip
      ((map (fun x => x ++ [a]) l'.sublists).reverse ++ l'.sublists.reverse)
⊢ l'.sublists.length = (map (fun x => x ++ [a]) l'.sublists).reverse.length

Tactic:
simp

Result:
no goals

Proof state:
case append_singleton.inr.intro.intro.intro.intro
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
⊢ l₁' ++ [a] ++ id l₂ ~ l' ++ [a]

Tactic:
rw [append_assoc]

Result:
case append_singleton.inr.intro.intro.intro.intro
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
⊢ l₁' ++ ([a] ++ id l₂) ~ l' ++ [a]