mathlib

813a191d - chore(logic/basic): Make higher `forall_congr`/`exists_congr` lemmas dependent (#11490)

chore(logic/basic): Make higher `forall_congr`/`exists_congr` lemmas dependent (#11490) Currently, `forall₂_congr` and friends take as arguments non dependent propositions like `p q : α → β → Prop`. This prevents them being useful virtually anywhere as most often foralls are nested like `∀ a, a ∈ s → ...` and `a ∈ s` depends on `a`. This PR turns them into `Π a, β a → Prop` (and similar for higher arities). As a bonus, it adds the `5`-ary version and golfs all occurrences of nested `forall_congr`s.