## 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
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
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,
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 :=


(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

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