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

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

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

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

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

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

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