Lean: `by linear_combination h` as an argument fails when the lemma's implicit vars are unassigned

Passing (by linear_combination hab) to a lemma like foo {α β : ℤ} (h : t * α + p * β = 1) ... gives 'ring failed, ring expressions not equal', even though the identity is trivial. The tactic block elaborates before α, β are unified with anything (later arguments do not fix them), so ring is asked to prove t * ?α + p * ?β = 1. Fix: name them, foo (α := α) (β := β) (by linear_combination hab) .... Related: linear_combination only proves equalities, so for a p ∣ ... goal, use push_cast; exact hu or simpa using hu (or Dvd.intro), not linear_combination.