Theorem: List.Index.unoption_eq_iff_eq_option (Extra/Index/Option.lean)

State before:
α✝ : Type u_1
xs : List α✝
k : xs.option.Index
i : Option xs.Index
⊢ k.unoption = i ↔ k = option i
Tactic:
constructor
State after:
case mp
α✝ : Type u_1
xs : List α✝
k : xs.option.Index
i : Option xs.Index
⊢ k.unoption = i → k = option i

case mpr
α✝ : Type u_1
xs : List α✝
k : xs.option.Index
i : Option xs.Index
⊢ k = option i → k.unoption = i

State before:
case mp
α✝ : Type u_1
xs : List α✝
k : xs.option.Index
i : Option xs.Index
⊢ k.unoption = i → k = option i
Tactic:
intro h
State after:
case mp
α✝ : Type u_1
xs : List α✝
k : xs.option.Index
i : Option xs.Index
h : k.unoption = i
⊢ k = option i

State before:
case mp
α✝ : Type u_1
xs : List α✝
k : xs.option.Index
i : Option xs.Index
h : k.unoption = i
⊢ k = option i
Tactic:
rw [←h, option_unoption]
State after:
no goals

State before:
case mpr
α✝ : Type u_1
xs : List α✝
k : xs.option.Index
i : Option xs.Index
⊢ k = option i → k.unoption = i
Tactic:
intro h
State after:
case mpr
α✝ : Type u_1
xs : List α✝
k : xs.option.Index
i : Option xs.Index
h : k = option i
⊢ k.unoption = i

State before:
case mpr
α✝ : Type u_1
xs : List α✝
k : xs.option.Index
i : Option xs.Index
h : k = option i
⊢ k.unoption = i
Tactic:
rw [h, unoption_option]
State after:
no goals