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

State before:
α✝ : Type u_1
xss : List (List α✝)
k : xss.join.Index
i : (i : xss.Index) × i.val.Index
⊢ k.unjoin = i ↔ k = join i
Tactic:
constructor
State after:
case mp
α✝ : Type u_1
xss : List (List α✝)
k : xss.join.Index
i : (i : xss.Index) × i.val.Index
⊢ k.unjoin = i → k = join i

case mpr
α✝ : Type u_1
xss : List (List α✝)
k : xss.join.Index
i : (i : xss.Index) × i.val.Index
⊢ k = join i → k.unjoin = i

State before:
case mp
α✝ : Type u_1
xss : List (List α✝)
k : xss.join.Index
i : (i : xss.Index) × i.val.Index
⊢ k.unjoin = i → k = join i
Tactic:
intro h
State after:
case mp
α✝ : Type u_1
xss : List (List α✝)
k : xss.join.Index
i : (i : xss.Index) × i.val.Index
h : k.unjoin = i
⊢ k = join i

State before:
case mp
α✝ : Type u_1
xss : List (List α✝)
k : xss.join.Index
i : (i : xss.Index) × i.val.Index
h : k.unjoin = i
⊢ k = join i
Tactic:
rw [←h, join_unjoin]
State after:
no goals

State before:
case mpr
α✝ : Type u_1
xss : List (List α✝)
k : xss.join.Index
i : (i : xss.Index) × i.val.Index
⊢ k = join i → k.unjoin = i
Tactic:
intro h
State after:
case mpr
α✝ : Type u_1
xss : List (List α✝)
k : xss.join.Index
i : (i : xss.Index) × i.val.Index
h : k = join i
⊢ k.unjoin = i

State before:
case mpr
α✝ : Type u_1
xss : List (List α✝)
k : xss.join.Index
i : (i : xss.Index) × i.val.Index
h : k = join i
⊢ k.unjoin = i
Tactic:
rw [h, unjoin_join]
State after:
no goals