Why does gcongr hide variables?

Stream: mathlib4

[Terence Tao]

When applying gcongr to products I can't conclude because the bound variables I need to use are hidden from view. For instance

import Mathlib
open Finset
open BigOperators

example (n : ℕ) : ∏ j in range n, (j+1) ≤ ∏ j in range n, n := by
  gcongr
  sorry

gcongr reduces (as it should) to asking to show that j+1 \leq n for all j \in range n, except that I can't actually access the variable j. Is there a way to make gcongr make the bound variables usable?

(In this case I can proceed using prod_le_prod instead, but I think it would be nice to have gcongr be a "one-stop-shop" for all these sorts of reductions.)

[Scott Morrison]

(First, it's helpful if code blocks compile right away: e.g. adding import Mathlib at the top of this one.)

[Scott Morrison]

You can work around this behaviour using the rename_i tactic, which lets you give accessible names to "tombstoned" hypotheses.

[Scott Morrison]

and gcongr with i a is the actual solution.

[Gareth Ma]

For the original inequality, I also found this solution, though I do not recommend it :P

example (n : ℕ) : ∏ j in range n, (j + 1) ≤ ∏ j in range n, n := by unhygienic -- !
  gcongr
  rwa [mem_range] at a

[Notification Bot]

16 messages were moved from this topic to #mathlib4 > gcongr handling equality? by Heather Macbeth.