Theorem: List.Index.unjoin_join (Extra/Index/Join.lean)

State before:
α✝ : Type u_1
xss : List (List α✝)
i : (i : xss.Index) × i.val.Index
⊢ (join i).unjoin = i
Tactic:
induction xss with
| nil => cases i; contradiction
| cons xs xss ih =>
  match i with
  | ⟨head, _⟩ => simp only [join, unjoin, unappend_append]
  | ⟨tail _, _⟩ => simp only [join, unjoin, unappend_append]; rw [ih]
State after:
no goals

State before:
case nil
α✝ : Type u_1
i : (i : [].Index) × i.val.Index
⊢ (join i).unjoin = i
Tactic:
cases i
State after:
case nil.mk
α✝ : Type u_1
fst✝ : [].Index
snd✝ : fst✝.val.Index
⊢ (join ⟨fst✝, snd✝⟩).unjoin = ⟨fst✝, snd✝⟩

State before:
case nil.mk
α✝ : Type u_1
fst✝ : [].Index
snd✝ : fst✝.val.Index
⊢ (join ⟨fst✝, snd✝⟩).unjoin = ⟨fst✝, snd✝⟩
Tactic:
contradiction
State after:
no goals

State before:
case cons
α✝ : Type u_1
xs : List α✝
xss : List (List α✝)
ih : ∀ (i : (i : xss.Index) × i.val.Index), (join i).unjoin = i
i : (i : (xs :: xss).Index) × i.val.Index
⊢ (join i).unjoin = i
Tactic:
match i with
| ⟨head, _⟩ => simp only [join, unjoin, unappend_append]
| ⟨tail _, _⟩ => simp only [join, unjoin, unappend_append]; rw [ih]
State after:
no goals

State before:
α✝ : Type u_1
xs : List α✝
xss : List (List α✝)
ih : ∀ (i : (i : xss.Index) × i.val.Index), (join i).unjoin = i
i : (i : (xs :: xss).Index) × i.val.Index
snd✝ : head.val.Index
⊢ (join ⟨head, snd✝⟩).unjoin = ⟨head, snd✝⟩
Tactic:
simp only [join, unjoin, unappend_append]
State after:
no goals

State before:
α✝ : Type u_1
xs : List α✝
xss : List (List α✝)
ih : ∀ (i : (i : xss.Index) × i.val.Index), (join i).unjoin = i
i : (i : (xs :: xss).Index) × i.val.Index
a✝ : xss.Index
snd✝ : a✝.tail.val.Index
⊢ (join ⟨a✝.tail, snd✝⟩).unjoin = ⟨a✝.tail, snd✝⟩
Tactic:
simp only [join, unjoin, unappend_append]
State after:
α✝ : Type u_1
xs : List α✝
xss : List (List α✝)
ih : ∀ (i : (i : xss.Index) × i.val.Index), (join i).unjoin = i
i : (i : (xs :: xss).Index) × i.val.Index
a✝ : xss.Index
snd✝ : a✝.tail.val.Index
⊢ ⟨(join ⟨a✝, snd✝⟩).unjoin.fst.tail, (join ⟨a✝, snd✝⟩).unjoin.snd⟩ = ⟨a✝.tail, snd✝⟩

State before:
α✝ : Type u_1
xs : List α✝
xss : List (List α✝)
ih : ∀ (i : (i : xss.Index) × i.val.Index), (join i).unjoin = i
i : (i : (xs :: xss).Index) × i.val.Index
a✝ : xss.Index
snd✝ : a✝.tail.val.Index
⊢ ⟨(join ⟨a✝, snd✝⟩).unjoin.fst.tail, (join ⟨a✝, snd✝⟩).unjoin.snd⟩ = ⟨a✝.tail, snd✝⟩
Tactic:
rw [ih]
State after:
no goals