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

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

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

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

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

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

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