Zulip Chat Archive

Stream: mathlib4

Topic: Make 'grw' match the entire LHS when rewriting

Aaron Hill (Nov 22 2025 at 21:21):

Consider the following synthetic lemma:

import Mathlib

lemma my_lemma (a b: ℝ): a + b + 25 ≤ b + a + 100 := by
  grw [Finset.single_le_sum (f := fun y => a + y + 25) (s := {3, 4})]
  . sorry
  . sorry
  . sorry

I'm trying to apply Finset.single_le_sum, using the entire LHS as the 'f' parameter (abstracted over 'b'). I can accomplish this by manually writing out a '(fun y => <body with 'b' replaced with 'y'>)' argument. However, this get very frustrating when the goal is more complicated (e.g. it contains proof terms, or pretty-printing doesn't roundtrip properly due to coercions).

Is there a way for me to accomplish the same rewrite while only explicitly naming 'b', and somehow telling grw to abstract 'b' from the entire LHS of the relation?

Aaron Hill (Nov 22 2025 at 21:24):

I thought about trying to first rewrite the goal to have an explicit ( fun y => <body>) b term, but I couldn't find any tactic that does that

Aaron Liu (Nov 22 2025 at 21:45):

I guess this is what rw is for

Aaron Liu (Nov 22 2025 at 22:01):

perhaps not the cleanest method but hey it works

import Mathlib

lemma my_lemma (a b: ℝ): a + b + 25 ≤ b + a + 100 := by
  refine letI goal := _; (?_ : zeta% goal)
  let f (y : ℝ) : ℝ := by
    haveI h : zeta% goal := sorry
    haveI hby : b = y := sorry
    exact letI lhs := _; letI h' : lhs ≤ _ := (by rewrite [hby] at h; exact h); lhs
  clear goal
  grw [Finset.single_le_sum (f := zeta% f) (s := {3, 4})]
  . sorry
  . sorry
  . sorry

Aaron Hill (Nov 23 2025 at 01:13):

Isn't haveI h : zeta% goal := sorry just the original goal again?

Aaron Liu (Nov 23 2025 at 02:32):

yes it is

Aaron Liu (Nov 23 2025 at 02:32):

but now I can rewrite on it

Aaron Hill (Nov 23 2025 at 02:36):

oh, wait, those sorries don't actually end up in the final proof

Aaron Hill (Nov 23 2025 at 02:36):

wow

Aaron Liu (Nov 23 2025 at 02:38):

well if they did then it would be kind of pointless since now I have to either fill them in or risk being unsound

Aaron Hill (Nov 23 2025 at 02:39):

yeah, I misunderstood your original post

Aaron Liu (Nov 23 2025 at 02:43):

I wish there were an easier way to manipulate expressions like this that doesn't require unification yoga

Jovan Gerbscheid (Dec 05 2025 at 17:54):

(deleted)

František Silváši 🦉 (Dec 05 2025 at 18:20):

I think there are two problems being conflated here? I don't think there's a need to do both 'abstracting over b' _and_ the rewrite in the same step.

With some simple machinery:

lemma my_lemma (a b: ℝ): a + b + 25 ≤ b + a + 100 := by
  -- Abstract over b
  change (_ + · + _) _ ≤ _
  set f := fun _ => _
  -- Rewrite
  grw [Finset.single_le_sum (f := f) (s := {3, 4})]
  . sorry
  . sorry
  . sorry

František Silváši 🦉 (Dec 05 2025 at 18:26):

So regardless of how complicated the expression is, do the generalisation in simplest way you can so that it's in the form f generalisedVar, and then target 'the' f.

Jovan Gerbscheid (Dec 05 2025 at 18:27):

Generally I would try to change the proof so that you can grw in the other direction. Maybe using a calc block.

Last updated: Dec 20 2025 at 21:32 UTC