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

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

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

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

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

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

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