norm_cast question

Stream: general

[Adam Kurkiewicz]

I can use norm_cast to prove that (2 * a) / 2 = a, where a is a natural number.

But proving a slightly more general (b * a) / b = a, where b is non-zero already fails.

Is there a stronger tactic to use? Or can I somehow hint to norm_cast that it has all it needs to finish the proof? Or should I use a different tactic?

import Mathlib

theorem Nat.mul_div_self_two (a : ℕ) : (2 * a) / 2 = a := by
  have in_rat : ((2 : ℚ) * a) / 2 = a := by ring_nf
  have two_divides_two_a : (2 ∣ 2 * a) := by
    use a
  norm_cast at in_rat

theorem Nat.mul_div_self (a b: ℕ) (H : b ≠ 0) : (b * a) / b = a := by
  have h_in_rat : ((b : ℚ) ≠ 0) := Nat.cast_ne_zero.mpr H
  have goal_in_rat : (a * (b : ℚ)) / b = a := by calc
    (a * (b : ℚ)) / b = a * ((↑b)⁻¹ * b) := by ring_nf
    _ = ↑a * 1 := by rw[Rat.inv_mul_cancel b h_in_rat]
    _ = ↑a := by ring

  have two_divides_two_a: (b ∣ b * a) := by
    use a

  norm_cast at goal_in_rat

[Ruben Van de Velde]

field_simp [hb]

[Adam Kurkiewicz]

great, thank you. Looks like field_simp can simply despatch with the whole proof.