gcongr for biUnion

Stream: mathlib4

[Yaël Dillies]

I am trying to make gcongr handle goals of the form ⋃ i ≤ m, f i ⊆ ⋃ i ≤ n, f i (shows up in the proof of Prokhorov's theorem). I thought I could get it to work using something like

import Mathlib.Data.Set.Lattice

@[gcongr]
lemma Set.iUnion_prop_mono {α : Type*} {p q : Prop} {s t : Set α} (hpq : p → q) (hst : s ⊆ t) :
    ⋃ _ : p, s ≤ ⋃ _ : q, t :=
  iUnion_subset fun hp ↦ hst.trans <| subset_iUnion (fun _ ↦ t) <| hpq hp

but it fails with

@[gcongr] attribute only applies to lemmas proving f x₁ ... xₙ ∼ f x₁' ... xₙ'.
 Not all arguments are free variables in the conclusion of ∀ {α : Type u_1} {p q : Prop} {s t : Set α},
  (p → q) → s ⊆ t → ⋃ (_ : p), s ≤ ⋃ (_ : q), t

[Yaël Dillies]

What am I doing wrong?

[Floris van Doorn]

I expect that it doesn't like -> as a binary relation...?

[Aaron Liu]

This works

import Mathlib.Data.Set.Lattice

@[gcongr]
lemma Set.iUnion_prop_mono {α : Type*} {p q : Prop} {s : p → Set α} {t : q → Set α} (hpq : p → q)
    (hst : ∀ hp hq, s hp ⊆ t hq) : iUnion s ≤ iUnion t :=
  iUnion_subset fun hp ↦ (hst hp (hpq hp)).trans <| subset_iUnion t <| hpq hp

[Aaron Liu]

The issue was that fun (_ : p) => s is not a free variable

[Yaël Dillies]

Aah, yeah. I wasn't thinking of the lambda

[Yaël Dillies]

@Heather Macbeth, any chance we can make this gcongr error message print which arguments are not free variables?

[Bhavik Mehta]

This is the part which checks that: https://github.com/leanprover-community/mathlib4/blob/b406f8ce738a4ff26f4acd63c269c9b71ff15bd7/Mathlib/Tactic/GCongr/Core.lean#L187