Confusing error message with rw tactic

Stream: general

[Syed Shaazib Tanvir]

I have the following function

@[grind]
def Nat.division (a : Nat) (b : {n : Nat // Nat.positive n}) : Nat × Nat :=
  if h : a < b.val then (0, a)
  else
    have h' : (a - b.val) < a := by
      obtain ⟨ b, hb ⟩ := b
      change a - b < a
      change ¬a < b at h
      apply not_lt_imp_ge at h
      have h' : a - b ≤ a
      · apply Chapter2.Nat.sub_le
      constructor
      · exact h'
      by_contra heq
      have hb' : b = 0
      · apply sub_eq_self_imp_subtrahend_zero a b heq h
      absurd hb
      change b = 0
      exact hb'
    let smaller_result := division (a - b.val) b
    (smaller_result.fst + 1, smaller_result.snd)
termination_by a

and I am trying to prove the theorem

theorem Nat.remainder_lt_divisor
  (a : Nat) (b : {n : Nat // positive n})
  : (a.division b).2 < ↑b := by
    let p (a : Nat) := (a.division b).2 < ↑b
    change p a
    apply strong_induction 0
    · intro m hm_bound hi
      change (m.division b).2 < ↑b
      unfold division
      if h : m < ↑b then
        rw [if_pos h]
      else
        sorry
    apply zero_le

Here trying to apply the rw tactic gives me the following error message:
Tactic rewrite failed: Did not find an occurrence of the pattern
if m < ↑b then ?m.55 else ?m.56
in the target expression

  (if h : m < ↑b then (0, m)
      else
        have h' := ⋯;
        have smaller_result := (m - ↑b).division b;
        (smaller_result.1 + 1, smaller_result.2)).2 <
    ↑b

which is really confusing to me since it looks like the pattern does occur

[Ruben Van de Velde]

Please share a single code block we can run, it's very hard to debug this otherwise

[Syed Shaazib Tanvir]

theorem Nat.strong_induction {p : Nat → Prop}
  (m₀ : Nat)
  (hind : ∀ m ≥ m₀, (∀ m', m' < m ∧ m' ≥ m₀ → p m') → p m)
  : (∀ m ≥ m₀, p m) := by sorry

def Nat.division (a : Nat) (b : {n : Nat // n > 0}) : Nat × Nat :=
  if h : a < b.val then (0, a)
  else
    let smaller_result := division (a - b.val) b
    (smaller_result.fst + 1, smaller_result.snd)

theorem Nat.remainder_lt_divisor
  (a : Nat) (b : {n : Nat // n > 0})
  : (a.division b).2 < ↑b := by
    let p (a : Nat) := (a.division b).2 < ↑b
    change p a
    apply strong_induction 0
    · intro m hm_bound hi
      change (m.division b).2 < ↑b
      unfold division
      if h : m < ↑b then
        rw [if_pos h]
      else
        sorry
    apply zero_le

Here's a similar example code block that gives the same error

[Ruben Van de Velde]

Thanks, the issue here is that you have a dependent if, that is, if h : m < b.val instead of if m < b.val. In this case, you need to use dif_pos rather than if_pos

[Syed Shaazib Tanvir]

That makes sense, thanks a lot for your help