Theorem: List.Index.unsum_eq_iff_eq_sum (Extra/Index/Sum.lean)

State before:
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : xs.Index ⊕ ys.Index
⊢ k.unsum = i ↔ k = sum i
Tactic:
constructor
State after:
case mp
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : xs.Index ⊕ ys.Index
⊢ k.unsum = i → k = sum i

case mpr
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : xs.Index ⊕ ys.Index
⊢ k = sum i → k.unsum = i

State before:
case mp
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : xs.Index ⊕ ys.Index
⊢ k.unsum = i → k = sum i
Tactic:
intro h
State after:
case mp
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : xs.Index ⊕ ys.Index
h : k.unsum = i
⊢ k = sum i

State before:
case mp
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : xs.Index ⊕ ys.Index
h : k.unsum = i
⊢ k = sum i
Tactic:
rw [←h, sum_unsum]
State after:
no goals

State before:
case mpr
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : xs.Index ⊕ ys.Index
⊢ k = sum i → k.unsum = i
Tactic:
intro h
State after:
case mpr
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : xs.Index ⊕ ys.Index
h : k = sum i
⊢ k.unsum = i

State before:
case mpr
α✝¹ : Type u_1
xs : List α✝¹
α✝ : Type u_2
ys : List α✝
k : (xs.sum ys).Index
i : xs.Index ⊕ ys.Index
h : k = sum i
⊢ k.unsum = i
Tactic:
rw [h, unsum_sum]
State after:
no goals