Like show but for hypotheses. Changes a hypothesis or goal to a definitionally equivalent one.
example (a b : ℕ) (H : a + 0 = b + 0) : a + 3 = b + 3 := begin -- a + 0 is definitially equivalent to a, and same for b change a = b at H, rw H end
Enter search terms or a module, class or function name.