Apply a rewrite on a precise term

Stream: new members

[Hamza Maimoune]

Hello everyone,

I would like to ask you if there is a way to apply a rewrite tactic on a particular term. For example, if I want to replace only the second term of an expression.

Thank you.

[Ryan Lahfa]

You can perform something like:

conv_rhs {
  rw [what you want]
}

It'll rewrite the right hand only.
Inside of a conv block, you can use congr in order to split parts of your equation, like if you have A * B, congr will give you two goals A then B, you can use skip to through some you don't want.

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib/blob/master/docs/extras/conv.md might help

[Hamza Maimoune]

Thank you both

[Patrick Massot]

@Hamza MAIMOUNE , please also try:

example (a b : ℕ) (h : a = b): a + a + a + a + a = 0 :=
begin
  rw [h] {occs := occurrences.pos [1, 3]},
  sorry,
end

The syntax is awfully verbose but it can still be quicker than a complicated conv navigation.