Theorem: BinOp.Identity.unique (WTA.lean)

State before:
α : Type
e e' : α
op : BinOp α
⊢ Identity op e → Identity op e' → e = e'
Tactic:
intro h h'
State after:
α : Type
e e' : α
op : BinOp α
h : Identity op e
h' : Identity op e'
⊢ e = e'

State before:
α : Type
e e' : α
op : BinOp α
h : Identity op e
h' : Identity op e'
⊢ e = e'
Tactic:
rw [←h'.left e, h.right e']
State after:
no goals