How to prove (z-1)/(z-1)=1 ?

Stream: general

[Jiatong Yang]

import algebra
example (z : ℤ) (H : z ≠ 1) : (z - 1) / (z - 1) = 1 := begin
  apply div_self,
end

This apply tactic fails.

[Heather Macbeth]

@Jiatong Yang You can use docs#int.div_self instead of docs#div_self. The main div_self lemma requires that the type be a docs#group_with_zero, which ℤ is not.

[Jiatong Yang]

Thank you very much! I thought lean couldn't identify (z-1) with itself. :joy: :joy:

[Winston Yin]

I find that in such cases where the expressions look the same but Lean fails to apply the lemma, it is helpful to use @ and explicitly type out every single argument, leaving the typeclass arguments as _. Lean will tell you exactly which _ cannot be synthesised.