## Stream: new members

### Topic: Cancelling in the Integers

#### Andre Hernandez-Espiet (Rutgers) (Nov 04 2022 at 19:15):

I was wondering if there is a tactic that takes care of cancelling and dividing over the integers. For example, a tactic that would solve the following examples (the first only accepted field_simp after the manipulation):

example {a b c: ℤ } (h: a≠ 0) : c*(a*b)/a = c*b:=
begin
rw ← mul_assoc, rw mul_comm c a,rw mul_assoc,field_simp,
end

example  {a b c: ℤ} (a0:a≠  0)(h: a*b=a*c) : b=c := (mul_right_inj' a0).mp h


#### Adam Topaz (Nov 04 2022 at 19:15):

I think field_simp; ring shouuld solve such things

oh it's in Z

#### Ruben Van de Velde (Nov 04 2022 at 19:17):

Has ratify (qify?) landed?

#### Adam Topaz (Nov 04 2022 at 19:17):

division in $\mathbb{Z}$ can behave in unexpected ways

#### Adam Topaz (Nov 04 2022 at 19:18):

I'm a bit surprised that field_simp makes any progress at all!

#### Kevin Buzzard (Nov 04 2022 at 20:09):

I usually deal with division by using a high-powered tactic like ring to rearrange the term into a form where a cancelling lemma like mul_div_cancel applies. For example here I would do

import tactic

example {a b c : ℤ} (h: a ≠ 0) : c * (a * b) / a = c * b :=
begin
rw (show c * (a * b) = (c * b) * a, by ring),
exact int.mul_div_cancel _ h,
end


I like this approach because you somehow don't have to move your brain to deal with the problem.

#### Andre Hernandez-Espiet (Rutgers) (Nov 04 2022 at 20:15):

I see. I'll try to do more stuff like that in the future.

Last updated: Dec 20 2023 at 11:08 UTC