at hyp { tac1, tac2 }

Stream: general

[Johan Commelin]

In feat(archive/imo): IMO 2021 Q1 #8432 we have proofs like

lemma lower_bound (n l : ℕ) (hl : 2 + sqrt (4 + 2 * n) ≤ 2 * (l : ℝ)) :
  (n : ℕ) + 4 * l ≤ 2 * l * l :=
begin
  have h₁ : sqrt (4 + 2 * n) ≤ 2 * l - 2 := by linarith,
  replace h₁ := (sqrt_le_iff.1 h₁).2,
  ring_exp at h₁,
  norm_num at h₁,
  norm_cast at h₁,
  linarith,
end

This suggest that we might want a pattern like

begin
  have h₁ : sqrt (4 + 2 * n) ≤ 2 * l - 2 := by linarith, := by linarith,
  replace h₁ := (sqrt_le_iff.1 h₁).2,
  at h₁ { ring_exp, norm_num, norm_cast },
  linarith,
end

Does that make sense? Would this be easy to implement in Lean 4?

[Scott Morrison]

Do you just mean "run each of these tactics, with at h₁ shoved on the end"? That might just work!

It feels like cheating to just do this at the syntactic level, however. We might have situations where you need to call a tactic like Foo at X with Y, but a hack like this will produce Foo with Y at X, which would fail, but users would reasonably be surprised.

(I don't see how else to do it.)