# Zulip Chat Archive

## Stream: new members

### Topic: Apply rw to hypothesis

#### Chu-Wee Lim (Oct 04 2019 at 18:19):

Sorry quick question. Is there a way to apply the rewrite tactic to a hypothesis instead of goal?

E.g. if h : a + c = b + c, I would like to apply add_right_cancel to it and obtain a = b.

#### Johan Commelin (Oct 04 2019 at 18:21):

Yes, `rw lemma at hyp`

#### Johan Commelin (Oct 04 2019 at 18:22):

Similarly `simp at hyp`

, `change foo at hyp`

, `push_neg at hyp`

, etc...

#### Chu-Wee Lim (Oct 04 2019 at 18:39):

Sorry I tried the following, but it's giving me an error.

example : ∀ a b c d : ℕ, a + c + d = b + c + d → a = b := assume a b c d h,

begin

rw add_right_cancel at h,

end

Error message: rewrite tactic failed, lemma lhs is a metavariable

#### Johan Commelin (Oct 04 2019 at 19:33):

@Chu-Wee Lim The problem is that `add_right_cancel`

is not formulated as an `iff`

statement. So you cannot use it like this.

#### Johan Commelin (Oct 04 2019 at 19:35):

You can do something like

example : ∀ a b c d : ℕ, a + c + d = b + c + d → a = b := assume a b c d h, begin have step1 := add_right_cancel h, have step2 := add_right_cancel step1, exact step2, end

#### Floris van Doorn (Oct 04 2019 at 19:59):

If it were an `iff`

statement, you could rewrite with it:

example : ∀ a b c d : ℕ, a + c + d = b + c + d → a = b := begin intros a b c d h, rw [add_right_cancel_iff, add_right_cancel_iff] at h, exact h end

#### Patrick Massot (Oct 04 2019 at 20:55):

Johan's solution is fake tactic mode, it could be written as

example : ∀ a b c d : ℕ, a + c + d = b + c + d → a = b := assume a b c d h, add_right_cancel (add_right_cancel h)

(which is perfectly fine). More in the tactic mode spirit would be:

example : ∀ a b c d : ℕ, a + c + d = b + c + d → a = b := assume a b c d h, begin apply add_right_cancel, apply add_right_cancel h, end

Although my taste in this case is to declare this as something Lean should just crush without asking any question:

example : ∀ a b c d : ℕ, a + c + d = b + c + d → a = b := by { intros, linarith }

Last updated: May 12 2021 at 04:19 UTC