Apply rw to hypothesis

Stream: new members

[Chu-Wee Lim]

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]

Yes, rw lemma at hyp

[Johan Commelin]

Similarly simp at hyp, change foo at hyp, push_neg at hyp, etc...

[Chu-Wee Lim]

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]

@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]

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]

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]

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 }