How to create alias inside tactic mode

Stream: new members

[Bernardo Borges]

With a more complicated proof it is often useful to create aliases for clarity. For example, in this proof I used da and ma to represent a / c and a % c further in the proof:

lemma add_ceildiv (a b c : ℕ)
  : (a + b) ⌈/⌉ c ≤ (a ⌈/⌉ c) + (b ⌈/⌉ c) := by
  rw [←Nat.div_add_mod a c,←Nat.div_add_mod b c]

  let ma := a % c
  have rma : ma = a % c := by exact rfl
  rw [←rma]

  let da := a / c
  have rda : da = a / c := by exact rfl
  rw [←rda]

  let mb := b % c
  have rmb : mb = b % c := by exact rfl
  rw [←rmb]

  let db := b / c
  have rdb : db = b / c := by exact rfl
  rw [←rdb]

  -- rename tactic?

  /-
  ⊢ (c * da + ma + (c * db + mb)) ⌈/⌉ c
  ≤ (c * da + ma) ⌈/⌉ c + (c * db + mb) ⌈/⌉ c
  -/
  admit
  done

Is there another way to achieve these aliases? Preferably in one line? Any other suggestions are welcome!

[Kevin Buzzard]

set mb := b % c with rmb etc

[Bernardo Borges]

Great! Exactly what I was looking for! Thanks!