Adding an extra hypothesis breaks linarith

Stream: mathlib4

[Eric Wieser]

It looks like some surprising unification is going on here:

import Mathlib.Tactic.Linarith

theorem foo {i m : ℕ} : i ∣ 2 ^ m → True := fun _ => trivial

theorem bad1 (k a i : ℕ)
    (useless : i ≤ i)
    (h : (↑a : ℤ) * 2 ^ k = 2 ^ i) : True := by
  have := foo ⟨2^k, by linarith⟩
  trivial

theorem bad2 (k a i : ℕ)
    (h : (↑a : ℤ) * 2 ^ k = 2 ^ i)
    (useless : i ≤ i) : True := by
  have := foo ⟨2^k, by linarith⟩
  trivial

theorem ok3 (k a i : ℕ)
    (h : (↑a : ℤ) * 2 ^ k = 2 ^ i)  : True := by
  have := foo ⟨2^k, by linarith⟩
  trivial

I'm able to fix bad1, but my fix doesn't work for bad2

[Eric Wieser]

(#28290 is the fix for bad1)

[Aaron Liu]

you have metavariables :/

[Eric Wieser]

Yes, that much I know :)