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

State before:
α : Type u_1
xss : List (List α)
k : xss.join.Index
⊢ join k.unjoin = k
Tactic:
induction xss with
| nil => contradiction
| cons xs xss ih =>
  match h : unappend k with
  | .inl j => rw [unappend_eq_iff_eq_append] at h; rw [h, unjoin, unappend_append, join]
  | .inr k => rw [unappend_eq_iff_eq_append] at h; rw [h, unjoin, unappend_append, join, ih]
State after:
no goals

State before:
case nil
α : Type u_1
k : [].join.Index
⊢ join k.unjoin = k
Tactic:
contradiction
State after:
no goals

State before:
case cons
α : Type u_1
xs : List α
xss : List (List α)
ih : ∀ (k : xss.join.Index), join k.unjoin = k
k : (xs :: xss).join.Index
⊢ join k.unjoin = k
Tactic:
match h : unappend k with
| .inl j => rw [unappend_eq_iff_eq_append] at h; rw [h, unjoin, unappend_append, join]
| .inr k => rw [unappend_eq_iff_eq_append] at h; rw [h, unjoin, unappend_append, join, ih]
State after:
no goals

State before:
α : Type u_1
xs : List α
xss : List (List α)
ih : ∀ (k : xss.join.Index), join k.unjoin = k
k : (xs :: xss).join.Index
j : xs.Index
h : k.unappend = Sum.inl j
⊢ join k.unjoin = k
Tactic:
rw [unappend_eq_iff_eq_append] at h
State after:
α : Type u_1
xs : List α
xss : List (List α)
ih : ∀ (k : xss.join.Index), join k.unjoin = k
k : (xs :: xss).join.Index
j : xs.Index
h : k = append (Sum.inl j)
⊢ join k.unjoin = k

State before:
α : Type u_1
xs : List α
xss : List (List α)
ih : ∀ (k : xss.join.Index), join k.unjoin = k
k : (xs :: xss).join.Index
j : xs.Index
h : k = append (Sum.inl j)
⊢ join k.unjoin = k
Tactic:
rw [h, unjoin, unappend_append, join]
State after:
no goals

State before:
α : Type u_1
xs : List α
xss : List (List α)
ih : ∀ (k : xss.join.Index), join k.unjoin = k
k✝ : (xs :: xss).join.Index
k : xss.join.Index
h : k✝.unappend = Sum.inr k
⊢ join k✝.unjoin = k✝
Tactic:
rw [unappend_eq_iff_eq_append] at h
State after:
α : Type u_1
xs : List α
xss : List (List α)
ih : ∀ (k : xss.join.Index), join k.unjoin = k
k✝ : (xs :: xss).join.Index
k : xss.join.Index
h : k✝ = append (Sum.inr k)
⊢ join k✝.unjoin = k✝

State before:
α : Type u_1
xs : List α
xss : List (List α)
ih : ∀ (k : xss.join.Index), join k.unjoin = k
k✝ : (xs :: xss).join.Index
k : xss.join.Index
h : k✝ = append (Sum.inr k)
⊢ join k✝.unjoin = k✝
Tactic:
rw [h, unjoin, unappend_append, join, ih]
State after:
no goals