Theorem: Fin.restrict_inj (Fifteen/Data/Fin/Basic.lean)

State before:
m n : Nat
i j : Fin m
hi : ↑i < n
hj : ↑j < n
h : restrict i hi = restrict j hj
⊢ i = j
Tactic:
rcases i with ⟨i,hi'⟩
State after:
case mk
m n : Nat
j : Fin m
hj : ↑j < n
i : Nat
hi' : i < m
hi : ↑{ val := i, isLt := hi' } < n
h : restrict { val := i, isLt := hi' } hi = restrict j hj
⊢ { val := i, isLt := hi' } = j

State before:
case mk
m n : Nat
j : Fin m
hj : ↑j < n
i : Nat
hi' : i < m
hi : ↑{ val := i, isLt := hi' } < n
h : restrict { val := i, isLt := hi' } hi = restrict j hj
⊢ { val := i, isLt := hi' } = j
Tactic:
rcases j with ⟨j,hj'⟩
State after:
case mk.mk
m n i : Nat
hi' : i < m
hi : ↑{ val := i, isLt := hi' } < n
j : Nat
hj' : j < m
hj : ↑{ val := j, isLt := hj' } < n
h : restrict { val := i, isLt := hi' } hi = restrict { val := j, isLt := hj' } hj
⊢ { val := i, isLt := hi' } = { val := j, isLt := hj' }

State before:
case mk.mk
m n i : Nat
hi' : i < m
hi : ↑{ val := i, isLt := hi' } < n
j : Nat
hj' : j < m
hj : ↑{ val := j, isLt := hj' } < n
h : restrict { val := i, isLt := hi' } hi = restrict { val := j, isLt := hj' } hj
⊢ { val := i, isLt := hi' } = { val := j, isLt := hj' }
Tactic:
cases h
State after:
case mk.mk.refl
m n i : Nat
hi' : i < m
hi : ↑{ val := i, isLt := hi' } < n
hj' : i < m
hj : ↑{ val := i, isLt := hj' } < n
⊢ { val := i, isLt := hi' } = { val := i, isLt := hj' }

State before:
case mk.mk.refl
m n i : Nat
hi' : i < m
hi : ↑{ val := i, isLt := hi' } < n
hj' : i < m
hj : ↑{ val := i, isLt := hj' } < n
⊢ { val := i, isLt := hi' } = { val := i, isLt := hj' }
Tactic:
rfl
State after:
no goals