norm cast gives me `Rat.divInt`

Stream: mathlib4

[Kevin Buzzard]

Is this expected? I assumed Rat.divInt was an implementation detail.

import Mathlib

example (a b c : ℤ) : (a : ℚ) * (b : ℚ) / (c : ℚ) = 1 := by
  -- ⊢ ↑a * ↑b / ↑c = 1
  norm_cast
  -- expecting : ↑(a * b) / ↑c = 1
  -- actual result:
  -- ⊢ Rat.divInt (a * b) c = 1
  sorry

[Ruben Van de Velde]

I've got an issue filled for something pretty similar

[Ruben Van de Velde]

That was #11573

[Kevin Buzzard]

darn it, I already thumbsed it up :-) I searched for Rat.divInt before posting but yours was Int.negSucc :-)

[Jovan Gerbscheid]

I ran into a third form of this problem:

import Mathlib

example (a b c : ℕ) : (a : ℤ) + (b : ℤ) - (c : ℤ) = 1 := by
  -- ⊢ ↑a + ↑b - ↑c = 1
  norm_cast
  -- expecting : ↑(a + b) - ↑c = 1
  -- actual result:
  -- ⊢ Int.subNatNat (a + b) c = 1
  sorry

Even more surprisingly, push_cast doesn't get rid of the Int.subNatNat.

The relevant lemma is:

@[simp, norm_cast]
theorem cast_subNatNat (m n) : ((Int.subNatNat m n : ℤ) : R) = m - n

[Kevin Buzzard]

This latter example works as expected (↑(a + b) - ↑c = 1) in Mathlib.Algebra.Ring.Int.Defs just before instance instCommRing : CommRing ℤ where ... and gives the wacky answer just after. Changing norm_cast to norm_cast squash in cast_subNatNat does not seem to fix it. Note that cast_subNatNat is defined in Mathlib.Data.Int.Cast.Basic, which is imported by Mathlib.Algebra.Ring.Int.Defs so you don't see the effect immediately, you also need to import the ring instance on Int for the problems to start.

[Kevin Buzzard]

None of norm_cast squash, norm_cast move and norm_cast elim seem to have any effect on the issue.