tactic to hide/drop/forget assumption I don't need anymore

Stream: new members

[Lynn]

Hi! Is there a tactic for getting rid of an assumption I don't need anymore? I wrote something like

  have f80: 80 = 2 * (2 * (2 * (2 * 5))) := by refl,
  rw [f80, nat.gcd_mul_left],
  have f10: 10 = 2 * 5 := by refl,
  rw [f10, nat.gcd_mul_left],

but I would like to add drop f10 f80 or hide f10 f80 or forget f10 f80 or something, so that they don't clutter the list of assumptions, because I don't need them anymore in the rest of the proof.

[Lynn]

also, if there's a way to write this without introducing an assumption for it, that would be cool too, something like rw (by refl) : 10 = 2 * 5 except syntactically valid

[Kevin Buzzard]

clear f10 f80

[Kevin Buzzard]

and rw (show 80 = 2 * (2 * (2 * (2 * 5))), by refl) should work

[Lynn]

clear! that's the magic word I was looking for, thank you :)