Zulip Chat Archive
Stream: mathlib4
Topic: gcongr and le
Yury G. Kudryashov (Aug 29 2024 at 21:55):
How can I teach gcongr to deal with (s : Set _) ≤ t as s ⊆ t?
Yury G. Kudryashov (Aug 29 2024 at 21:56):
Some lemmas take Monotone (s : Nat → Set _) as an argument, and fun s t h => ?_ gives a ≤ goal.
Last updated: May 02 2025 at 03:31 UTC