case nil
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init✝ tail✝ init tail : List α
⊢ (init, tail) ∈ ([], []) :: zip [] [] ↔ init ++ tail = []

case cons
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init✝ tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
init tail : List α
⊢ (init, tail) ∈ ([], hd :: tl) :: zip (map (fun t => hd :: t) (inits tl)) (tails tl) ↔ init ++ tail = hd :: tl
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
l init tail : List α
⊢ (init, tail) ∈ zip (inits l) (tails l) ↔ init ++ tail = l
induction' l with hd tl ih generalizing init tail <;> simp_rw [tails, inits, zip_cons_cons]
no goals
case nil
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init✝ tail✝ init tail : List α
⊢ (init, tail) ∈ ([], []) :: zip [] [] ↔ init ++ tail = []
simp
case cons.mp
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init✝ tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
init tail : List α
⊢ ((init, tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (a, b) = (init, tail)) →
    init ++ tail = hd :: tl

case cons.mpr
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init✝ tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
init tail : List α
⊢ init ++ tail = hd :: tl →
    (init, tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (a, b) = (init, tail)
case cons
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init✝ tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
init tail : List α
⊢ (init, tail) ∈ ([], hd :: tl) :: zip (map (fun t => hd :: t) (inits tl)) (tails tl) ↔ init ++ tail = hd :: tl
constructor <;> rw [mem_cons, zip_map_left, mem_map, Prod.exists]
case cons.mp.inl.refl
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init tail : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
⊢ [] ++ hd :: tl = hd :: tl

case cons.mp.inr.intro.intro.intro.refl
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init tail : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
w✝¹ w✝ : List α
h : (w✝¹, w✝) ∈ zip (inits tl) (tails tl)
⊢ (fun t => hd :: t) w✝¹ ++ id w✝ = hd :: tl
case cons.mp
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init✝ tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
init tail : List α
⊢ ((init, tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (a, b) = (init, tail)) →
    init ++ tail = hd :: tl
rintro (⟨rfl, rfl⟩ | ⟨_, _, h, rfl, rfl⟩)
no goals
case cons.mp.inl.refl
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init tail : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
⊢ [] ++ hd :: tl = hd :: tl
simp
no goals
case cons.mp.inr.intro.intro.intro.refl
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init tail : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
w✝¹ w✝ : List α
h : (w✝¹, w✝) ∈ zip (inits tl) (tails tl)
⊢ (fun t => hd :: t) w✝¹ ++ id w✝ = hd :: tl
simp [ih.mp h]
case cons.mpr.nil
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
tail : List α
⊢ [] ++ tail = hd :: tl →
    ([], tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (a, b) = ([], tail)

case cons.mpr.cons
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
⊢ hd' :: tl' ++ tail = hd :: tl →
    (hd' :: tl', tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (a, b) = (hd' :: tl', tail)
case cons.mpr
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init✝ tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
init tail : List α
⊢ init ++ tail = hd :: tl →
    (init, tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (a, b) = (init, tail)
cases' init with hd' tl'
case cons.mpr.nil
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init tail : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
⊢ ([], hd :: tl) = ([], hd :: tl) ∨
    ∃ a b, (a, b) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (a, b) = ([], hd :: tl)
case cons.mpr.nil
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
tail : List α
⊢ [] ++ tail = hd :: tl →
    ([], tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (a, b) = ([], tail)
rintro rfl
no goals
case cons.mpr.nil
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init tail : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
⊢ ([], hd :: tl) = ([], hd :: tl) ∨
    ∃ a b, (a, b) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (a, b) = ([], hd :: tl)
simp
case cons.mpr.cons
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
h : hd' :: tl' ++ tail = hd :: tl
⊢ (hd' :: tl', tail) = ([], hd :: tl) ∨
    ∃ a b, (a, b) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (a, b) = (hd' :: tl', tail)
case cons.mpr.cons
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
⊢ hd' :: tl' ++ tail = hd :: tl →
    (hd' :: tl', tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (a, b) = (hd' :: tl', tail)
intro h
case cons.mpr.cons.h
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
h : hd' :: tl' ++ tail = hd :: tl
⊢ ∃ a b, (a, b) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (a, b) = (hd' :: tl', tail)
case cons.mpr.cons
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
h : hd' :: tl' ++ tail = hd :: tl
⊢ (hd' :: tl', tail) = ([], hd :: tl) ∨
    ∃ a b, (a, b) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (a, b) = (hd' :: tl', tail)
right
case cons.mpr.cons.h
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
h : hd' :: tl' ++ tail = hd :: tl
⊢ (tl', tail) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (tl', tail) = (hd' :: tl', tail)
case cons.mpr.cons.h
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
h : hd' :: tl' ++ tail = hd :: tl
⊢ ∃ a b, (a, b) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (a, b) = (hd' :: tl', tail)
use tl', tail
no goals
case cons.mpr.cons.h
α : Type u
β : Type ?u.161184
γ : Type ?u.161187
δ : Type ?u.161190
ε : Type ?u.161193
init tail✝ : List α
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ zip (inits tl) (tails tl) ↔ init ++ tail = tl
tail : List α
hd' : α
tl' : List α
h : hd' :: tl' ++ tail = hd :: tl
⊢ (tl', tail) ∈ zip (inits tl) (tails tl) ∧ Prod.map (fun t => hd :: t) id (tl', tail) = (hd' :: tl', tail)
simp_all