## Stream: general

### Topic: at hyp { tac1, tac2 }

#### Johan Commelin (Aug 20 2021 at 06:22):

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 (Aug 20 2021 at 07:06):

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.)

Last updated: Dec 20 2023 at 11:08 UTC