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

Proof state:
case cons.inr.intro.intro
α : Type u
a : α
l : List α
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
⊢ a :: l₁' ++ l₂ ~ a :: l

Tactic:
exact (IH _ _ h).cons _

Result:
no goals

Proof state:
case cons
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h : (l₁, l₂) ∈ (a :: l).sublists'.zip (a :: l).sublists'.reverse
⊢ l₁ ++ l₂ ~ a :: l

Tactic:
rw [sublists'_cons, reverse_append, zip_append, ← map_reverse, zip_map_right, zip_map_left] at *
  <;> [simp only [mem_append, mem_map, Prod.map_apply, id_eq, Prod.mk.injEq, Prod.exists,
    exists_eq_right_right] at h; simp]

Result:
case cons
α : Type u
a : α
l : List α
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 ∧ a_1 = l₁ ∧ a :: b = l₂) ∨
    ∃ a_1, (a_1, l₂) ∈ l.sublists'.zip l.sublists'.reverse ∧ a :: a_1 = l₁
⊢ l₁ ++ l₂ ~ a :: l

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:
case nil
α : Type u
l₁ l₂ : List α
h : (l₁, l₂) ∈ [].sublists'.zip [].sublists'.reverse
⊢ l₁ ++ l₂ ~ []

Tactic:
simp_all only [sublists'_nil, reverse_cons, reverse_nil, nil_append, zip_cons_cons,
  zip_nil_right, mem_singleton, Prod.mk.injEq, append_nil, Perm.refl]

Result:
no goals

Proof state:
case cons
α : Type u
a : α
l : List α
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 ∧ a_1 = l₁ ∧ a :: b = l₂) ∨
    ∃ a_1, (a_1, l₂) ∈ l.sublists'.zip l.sublists'.reverse ∧ a :: a_1 = l₁
⊢ l₁ ++ l₂ ~ a :: l

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

Result:
case cons.inl.intro.intro.intro.intro
α : Type u
a : α
l : List α
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 :: l₂' ~ a :: l

case cons.inr.intro.intro
α : Type u
a : α
l : List α
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
⊢ a :: l₁' ++ l₂ ~ a :: l

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

Tactic:
induction' l with a l IH <;> intro l₁ l₂ h

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

case cons
α : Type u
a : α
l : List α
IH : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse → l₁ ++ l₂ ~ l
l₁ l₂ : List α
h : (l₁, l₂) ∈ (a :: l).sublists'.zip (a :: l).sublists'.reverse
⊢ l₁ ++ l₂ ~ a :: l

Proof state:
case cons.inl.intro.intro.intro.intro
α : Type u
a : α
l : List α
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 :: l₂' ~ a :: l

Tactic:
exact perm_middle.trans ((IH _ _ h).cons _)

Result:
no goals