Theorem: map_plusone_pred (Saturn/PrependClause.lean)

State before:
n : Option ℕ
m j : ℕ
hyp : some (j + 1) = some (m + 1)
⊢ j + 1 = m + 1
Tactic:
injection hyp
State after:
no goals

State before:
n : Option ℕ
m j : ℕ
hyp : some (j + 1) = some (m + 1)
lem1 : j + 1 = m + 1 := Option.noConfusion hyp fun val_eq => val_eq
⊢ j = m
Tactic:
injection lem1
State after:
no goals