-- Mathlib/Data/List/Zip.lean
theorem mem_zip_inits_tails {l : List α} {init tail : List α} :
    (init, tail) ∈ zip l.inits l.tails ↔ init ++ tail = l

Proof state:
case cons.mpr
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ init ++ tail = hd :: tl →
    (init, tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t => hd :: t) id (a, b) = (init, tail)

Tactic:
rcases init with - | ⟨hd', tl'⟩

Result:
case cons.mpr.nil
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
tail : List α
⊢ [] ++ tail = hd :: tl →
    ([], tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t => hd :: t) id (a, b) = ([], tail)

case cons.mpr.cons
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
⊢ hd' :: tl' ++ tail = hd :: tl →
    (hd' :: tl', tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t => hd :: t) id (a, b) = (hd' :: tl', tail)

Proof state:
case cons.mpr.nil
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
⊢ ([], hd :: tl) = ([], hd :: tl) ∨
    ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t => hd :: t) id (a, b) = ([], hd :: tl)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
l init tail : List α
⊢ (init, tail) ∈ l.inits.zip l.tails ↔ init ++ tail = l

Tactic:
induction' l with hd tl ih generalizing init tail <;> simp_rw [tails, inits, zip_cons_cons]

Result:
case nil
α : Type u
init tail : List α
⊢ (init, tail) ∈ ([], []) :: [].zip [] ↔ init ++ tail = []

case cons
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ (init, tail) ∈ ([], hd :: tl) :: (map (fun t => hd :: t) tl.inits).zip tl.tails ↔ init ++ tail = hd :: tl

Proof state:
case cons.mpr.cons
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
h : hd' :: tl' ++ tail = hd :: tl
⊢ (hd' :: tl', tail) = ([], hd :: tl) ∨
    ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t => hd :: t) id (a, b) = (hd' :: tl', tail)

Tactic:
right

Result:
case cons.mpr.cons.h
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
h : hd' :: tl' ++ tail = hd :: tl
⊢ ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t => hd :: t) id (a, b) = (hd' :: tl', tail)

Proof state:
case cons.mpr.nil
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
tail : List α
⊢ [] ++ tail = hd :: tl →
    ([], tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t => hd :: t) id (a, b) = ([], tail)

Tactic:
rintro rfl

Result:
case cons.mpr.nil
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
⊢ ([], hd :: tl) = ([], hd :: tl) ∨
    ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t => hd :: t) id (a, b) = ([], hd :: tl)

Proof state:
case h
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
h : hd' :: tl' ++ tail = hd :: tl
⊢ (tl', tail) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t => hd :: t) id (tl', tail) = (hd' :: tl', tail)

Tactic:
simp_all

Result:
no goals

Proof state:
case cons.mp
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ ((init, tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t => hd :: t) id (a, b) = (init, tail)) →
    init ++ tail = hd :: tl

Tactic:
rintro (⟨rfl, rfl⟩ | ⟨_, _, h, rfl, rfl⟩)

Result:
case cons.mp.inl.refl
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
⊢ [] ++ hd :: tl = hd :: tl

case cons.mp.inr.intro.intro.intro.refl
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
w✝¹ w✝ : List α
h : (w✝¹, w✝) ∈ tl.inits.zip tl.tails
⊢ (fun t => hd :: t) w✝¹ ++ id w✝ = hd :: tl

Proof state:
case nil
α : Type u
init tail : List α
⊢ (init, tail) ∈ ([], []) :: [].zip [] ↔ init ++ tail = []

Tactic:
simp

Result:
no goals

Proof state:
case cons.mpr.cons
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
⊢ hd' :: tl' ++ tail = hd :: tl →
    (hd' :: tl', tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t => hd :: t) id (a, b) = (hd' :: tl', tail)

Tactic:
intro h

Result:
case cons.mpr.cons
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
h : hd' :: tl' ++ tail = hd :: tl
⊢ (hd' :: tl', tail) = ([], hd :: tl) ∨
    ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t => hd :: t) id (a, b) = (hd' :: tl', tail)

Proof state:
case cons.mpr.cons.h
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
h : hd' :: tl' ++ tail = hd :: tl
⊢ ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t => hd :: t) id (a, b) = (hd' :: tl', tail)

Tactic:
use tl', tail

Result:
case h
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
h : hd' :: tl' ++ tail = hd :: tl
⊢ (tl', tail) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t => hd :: t) id (tl', tail) = (hd' :: tl', tail)

Proof state:
case cons
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ (init, tail) ∈ ([], hd :: tl) :: (map (fun t => hd :: t) tl.inits).zip tl.tails ↔ init ++ tail = hd :: tl

Tactic:
constructor <;> rw [mem_cons, zip_map_left, mem_map, Prod.exists]

Result:
case cons.mp
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ ((init, tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t => hd :: t) id (a, b) = (init, tail)) →
    init ++ tail = hd :: tl

case cons.mpr
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ init ++ tail = hd :: tl →
    (init, tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t => hd :: t) id (a, b) = (init, tail)

Proof state:
case cons.mp.inl.refl
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
⊢ [] ++ hd :: tl = hd :: tl

Tactic:
simp

Result:
no goals

Proof state:
case cons.mp.inr.intro.intro.intro.refl
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
w✝¹ w✝ : List α
h : (w✝¹, w✝) ∈ tl.inits.zip tl.tails
⊢ (fun t => hd :: t) w✝¹ ++ id w✝ = hd :: tl

Tactic:
simp [ih.mp h]

Result:
no goals