chore(logic/basic): Make higher forall_congr/exists_congr lemmas dependent (#11490)

YaelDillies · YaelDillies · commit 813a191df011 · 2022-01-18T03:54:41.000Z
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.
diff --git a/src/algebra/associated.lean b/src/algebra/associated.lean
@@ -625,8 +625,7 @@ begin
   apply and_congr mk_ne_zero,
   apply and_congr,
   { rw [is_unit_mk], },
-  apply forall_congr, assume a,
-  apply forall_congr, assume b,
+  refine forall₂_congr (λ a b, _),
   rw [mk_mul_mk, mk_dvd_mk, mk_dvd_mk, mk_dvd_mk],
 end
 
diff --git a/src/analysis/asymptotics/asymptotics.lean b/src/analysis/asymptotics/asymptotics.lean
@@ -418,7 +418,7 @@ by { unfold is_O, exact exists_congr (λ _, is_O_with_norm_right) }
 alias is_O_norm_right ↔ asymptotics.is_O.of_norm_right asymptotics.is_O.norm_right
 
 @[simp] theorem is_o_norm_right : is_o f (λ x, ∥g' x∥) l ↔ is_o f g' l :=
-by { unfold is_o, exact forall_congr (λ _, forall_congr $ λ _, is_O_with_norm_right) }
+by { unfold is_o, exact forall₂_congr (λ _ _, is_O_with_norm_right) }
 
 alias is_o_norm_right ↔ asymptotics.is_o.of_norm_right asymptotics.is_o.norm_right
 
@@ -433,7 +433,7 @@ by { unfold is_O, exact exists_congr (λ _, is_O_with_norm_left) }
 alias is_O_norm_left ↔ asymptotics.is_O.of_norm_left asymptotics.is_O.norm_left
 
 @[simp] theorem is_o_norm_left : is_o (λ x, ∥f' x∥) g l ↔ is_o f' g l :=
-by { unfold is_o,  exact forall_congr (λ _, forall_congr $ λ _, is_O_with_norm_left) }
+by { unfold is_o, exact forall₂_congr (λ _ _, is_O_with_norm_left) }
 
 alias is_o_norm_left ↔ asymptotics.is_o.of_norm_left asymptotics.is_o.norm_left
 
@@ -468,7 +468,7 @@ by { unfold is_O, exact exists_congr (λ _, is_O_with_neg_right) }
 alias is_O_neg_right ↔ asymptotics.is_O.of_neg_right asymptotics.is_O.neg_right
 
 @[simp] theorem is_o_neg_right : is_o f (λ x, -(g' x)) l ↔ is_o f g' l :=
-by { unfold is_o, exact forall_congr (λ _, (forall_congr (λ _, is_O_with_neg_right))) }
+by { unfold is_o, exact forall₂_congr (λ _ _, is_O_with_neg_right) }
 
 alias is_o_neg_right ↔ asymptotics.is_o.of_neg_right asymptotics.is_o.neg_right
 
@@ -483,7 +483,7 @@ by { unfold is_O, exact exists_congr (λ _, is_O_with_neg_left) }
 alias is_O_neg_left ↔ asymptotics.is_O.of_neg_left asymptotics.is_O.neg_left
 
 @[simp] theorem is_o_neg_left : is_o (λ x, -(f' x)) g l ↔ is_o f' g l :=
-by { unfold is_o, exact forall_congr (λ _, (forall_congr (λ _, is_O_with_neg_left))) }
+by { unfold is_o, exact forall₂_congr (λ _ _, is_O_with_neg_left) }
 
 alias is_o_neg_left ↔ asymptotics.is_o.of_neg_right asymptotics.is_o.neg_left
 
@@ -1463,7 +1463,7 @@ by { unfold is_O, exact exists_congr (λ C, e.is_O_with_congr hb) }
 /-- Transfer `is_o` over a `local_homeomorph`. -/
 lemma is_o_congr (e : local_homeomorph α β) {b : β} (hb : b ∈ e.target) {f : β → E} {g : β → F} :
   is_o f g (𝓝 b) ↔ is_o (f ∘ e) (g ∘ e) (𝓝 (e.symm b)) :=
-by { unfold is_o, exact (forall_congr $ λ c, forall_congr $ λ hc, e.is_O_with_congr hb) }
+by { unfold is_o, exact forall₂_congr (λ c hc, e.is_O_with_congr hb) }
 
 end local_homeomorph
 
@@ -1488,6 +1488,6 @@ by { unfold is_O, exact exists_congr (λ C, e.is_O_with_congr) }
 /-- Transfer `is_o` over a `homeomorph`. -/
 lemma is_o_congr (e : α ≃ₜ β) {b : β} {f : β → E} {g : β → F} :
   is_o f g (𝓝 b) ↔ is_o (f ∘ e) (g ∘ e) (𝓝 (e.symm b)) :=
-by { unfold is_o, exact forall_congr (λ c, forall_congr (λ hc, e.is_O_with_congr)) }
+by { unfold is_o, exact forall₂_congr (λ c hc, e.is_O_with_congr) }
 
 end homeomorph
diff --git a/src/analysis/box_integral/basic.lean b/src/analysis/box_integral/basic.lean
@@ -205,7 +205,7 @@ lemma integrable_iff_cauchy_basis [complete_space F] :
 begin
   rw [integrable_iff_cauchy, cauchy_map_iff',
     (l.has_basis_to_filter_Union_top _).prod_self.tendsto_iff uniformity_basis_dist_le],
-  refine forall_congr (λ ε, forall_congr $ λ ε0, exists_congr $ λ r, _),
+  refine forall₂_congr (λ ε ε0, exists_congr $ λ r, _),
   simp only [exists_prop, prod.forall, set.mem_Union, exists_imp_distrib,
     prod_mk_mem_set_prod_eq, and_imp, mem_inter_eq, mem_set_of_eq],
   exact and_congr iff.rfl ⟨λ H c₁ c₂ π₁ π₂ h₁ hU₁ h₂ hU₂, H π₁ π₂ c₁ h₁ hU₁ c₂ h₂ hU₂,
diff --git a/src/analysis/convex/basic.lean b/src/analysis/convex/basic.lean
@@ -479,11 +479,9 @@ variables {𝕜 s}
 lemma convex_iff_segment_subset :
   convex 𝕜 s ↔ ∀ ⦃x y⦄, x ∈ s → y ∈ s → [x -[𝕜] y] ⊆ s :=
 begin
-  split,
-  { rintro h x y hx hy z ⟨a, b, ha, hb, hab, rfl⟩,
-    exact h hx hy ha hb hab },
-  { rintro h x y hx hy a b ha hb hab,
-    exact h hx hy ⟨a, b, ha, hb, hab, rfl⟩ }
+  refine forall₄_congr (λ x y hx hy, ⟨_, λ h a b ha hb hab, h ⟨a, b, ha, hb, hab, rfl⟩⟩),
+  rintro h _ ⟨a, b, ha, hb, hab, rfl⟩,
+  exact h ha hb hab,
 end
 
 lemma convex.segment_subset (h : convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ s) :
@@ -591,11 +589,8 @@ end
 
 lemma convex_iff_open_segment_subset :
   convex 𝕜 s ↔ ∀ ⦃x y⦄, x ∈ s → y ∈ s → open_segment 𝕜 x y ⊆ s :=
-begin
-  rw convex_iff_segment_subset,
-  exact forall₂_congr (λ x y, forall₂_congr $ λ hx hy,
-    (open_segment_subset_iff_segment_subset hx hy).symm),
-end
+convex_iff_segment_subset.trans $ forall₄_congr $ λ x y hx hy,
+  (open_segment_subset_iff_segment_subset hx hy).symm
 
 lemma convex_singleton (c : E) : convex 𝕜 ({c} : set E) :=
 begin
diff --git a/src/analysis/convex/star.lean b/src/analysis/convex/star.lean
@@ -193,7 +193,7 @@ end
 
 lemma star_convex_iff_open_segment_subset (hx : x ∈ s) :
   star_convex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s → open_segment 𝕜 x y ⊆ s :=
-star_convex_iff_segment_subset.trans $ forall_congr $ λ y, forall_congr $ λ hy,
+star_convex_iff_segment_subset.trans $ forall₂_congr $ λ y hy,
   (open_segment_subset_iff_segment_subset hx hy).symm
 
 lemma star_convex_singleton (x : E) : star_convex 𝕜 x {x} :=
diff --git a/src/analysis/normed/group/quotient.lean b/src/analysis/normed/group/quotient.lean
@@ -191,7 +191,7 @@ begin
      ... ↔ ∀ ε > 0, (∃ x ∈ S, x ∈ metric.ball m ε) : by simp [dist_eq_norm, ← sub_eq_add_neg,
                                                               norm_sub_rev]
      ... ↔ m ∈ closure ↑S : by simp [metric.mem_closure_iff, dist_comm],
-    apply forall_congr, intro ε, apply forall_congr, intro  ε_pos,
+    refine forall₂_congr (λ ε ε_pos, _),
     rw [← S.exists_neg_mem_iff_exists_mem],
     simp },
   { use 0,
diff --git a/src/category_theory/sites/sheaf.lean b/src/category_theory/sites/sheaf.lean
@@ -266,7 +266,7 @@ lemma is_sheaf_iff_multiequalizer
   (∀ (X : C) (S : J.cover X), is_iso (S.to_multiequalizer P)) :=
 begin
   rw is_sheaf_iff_multifork,
-  apply forall_congr (λ X, _), apply forall_congr (λ S, _), split,
+  refine forall₂_congr (λ X S, ⟨_, _⟩),
   { rintros ⟨h⟩,
     let e : P.obj (op X) ≅ multiequalizer (S.index P) :=
       h.cone_point_unique_up_to_iso (limit.is_limit _),
diff --git a/src/combinatorics/additive/salem_spencer.lean b/src/combinatorics/additive/salem_spencer.lean
@@ -210,8 +210,7 @@ section nat
 lemma add_salem_spencer_iff_eq_right {s : set ℕ} :
   add_salem_spencer s ↔ ∀ ⦃a b c⦄, a ∈ s → b ∈ s → c ∈ s → a + b = c + c → a = c :=
 begin
-  refine forall_congr (λ a, forall_congr $ λ b, forall_congr $ λ c, forall_congr $
-    λ _, forall_congr $ λ _, forall_congr $ λ _,  forall_congr $ λ habc, ⟨_, _⟩),
+  refine forall₄_congr (λ a b c _, forall₃_congr $ λ _ _ habc, ⟨_, _⟩),
   { rintro rfl,
     simp_rw ←two_mul at habc,
     exact mul_left_cancel₀ two_ne_zero habc },
diff --git a/src/data/multiset/basic.lean b/src/data/multiset/basic.lean
@@ -1868,8 +1868,7 @@ lemma rel_cons_right {as b bs} :
   rel r as (b ::ₘ bs) ↔ (∃a as', r a b ∧ rel r as' bs ∧ as = a ::ₘ as') :=
 begin
   rw [← rel_flip, rel_cons_left],
-  apply exists_congr, assume a,
-  apply exists_congr, assume as',
+  refine exists₂_congr (λ a as', _),
   rw [rel_flip, flip]
 end
 
diff --git a/src/data/set/function.lean b/src/data/set/function.lean
@@ -951,8 +951,7 @@ lemma injective_piecewise_iff {f g : α → β} :
 begin
   rw [injective_iff_inj_on_univ, ← union_compl_self s, inj_on_union (@disjoint_compl_right _ s _),
     (piecewise_eq_on s f g).inj_on_iff, (piecewise_eq_on_compl s f g).inj_on_iff],
-  refine and_congr iff.rfl (and_congr iff.rfl $ forall_congr $ λ x, forall_congr $ λ hx,
-    forall_congr $ λ y, forall_congr $ λ hy, _),
+  refine and_congr iff.rfl (and_congr iff.rfl $ forall₄_congr $ λ x hx y hy, _),
   rw [piecewise_eq_of_mem s f g hx, piecewise_eq_of_not_mem s f g hy]
 end
 
diff --git a/src/data/set/prod.lean b/src/data/set/prod.lean
@@ -275,7 +275,7 @@ lemma pi_inter_distrib : s.pi (λ i, t i ∩ t₁ i) = s.pi t ∩ s.pi t₁ :=
 ext $ λ x, by simp only [forall_and_distrib, mem_pi, mem_inter_eq]
 
 lemma pi_congr (h : s₁ = s₂) (h' : ∀ i ∈ s₁, t₁ i = t₂ i) : s₁.pi t₁ = s₂.pi t₂ :=
-h ▸ (ext $ λ x, forall_congr $ λ i, forall_congr $ λ hi, h' i hi ▸ iff.rfl)
+h ▸ (ext $ λ x, forall₂_congr $ λ i hi, h' i hi ▸ iff.rfl)
 
 lemma pi_eq_empty (hs : i ∈ s) (ht : t i = ∅) : s.pi t = ∅ :=
 by { ext f, simp only [mem_empty_eq, not_forall, iff_false, mem_pi, not_imp],
diff --git a/src/geometry/manifold/diffeomorph.lean b/src/geometry/manifold/diffeomorph.lean
@@ -246,7 +246,7 @@ h.times_cont_mdiff_within_at_diffeomorph_comp_iff hm
 @[simp] lemma times_cont_mdiff_on_diffeomorph_comp_iff {m} (h : M ≃ₘ^n⟮I, J⟯ N) {f : M' → M}
   (hm : m ≤ n) {s} :
   times_cont_mdiff_on I' J m (h ∘ f) s ↔ times_cont_mdiff_on I' I m f s :=
-forall_congr $ λ x, forall_congr $ λ hx, h.times_cont_mdiff_within_at_diffeomorph_comp_iff hm
+forall₂_congr $ λ x hx, h.times_cont_mdiff_within_at_diffeomorph_comp_iff hm
 
 @[simp] lemma times_cont_mdiff_diffeomorph_comp_iff {m} (h : M ≃ₘ^n⟮I, J⟯ N) {f : M' → M}
   (hm : m ≤ n) :
diff --git a/src/logic/basic.lean b/src/logic/basic.lean
@@ -817,45 +817,59 @@ end equality
 /-! ### Declarations about quantifiers -/
 
 section quantifiers
-variables {α : Sort*} {β : Sort*} {p q : α → Prop} {b : Prop}
+variables {α : Sort*}
 
-lemma forall_imp (h : ∀ a, p a → q a) : (∀ a, p a) → ∀ a, q a :=
-λ h' a, h a (h' a)
+section congr
+variables {β : α → Sort*} {γ : Π a, β a → Sort*} {δ : Π a b, γ a b → Sort*}
+  {ε : Π a b c, δ a b c → Sort*}
+
+lemma forall₂_congr {p q : Π a, β a → Prop} (h : ∀ a b, p a b ↔ q a b) :
+  (∀ a b, p a b) ↔ ∀ a b, q a b :=
+forall_congr $ λ a, forall_congr $ h a
+
+lemma forall₃_congr {p q : Π a b, γ a b → Prop} (h : ∀ a b c, p a b c ↔ q a b c) :
+  (∀ a b c, p a b c) ↔ ∀ a b c, q a b c :=
+forall_congr $ λ a, forall₂_congr $ h a
+
+lemma forall₄_congr {p q : Π a b c, δ a b c → Prop} (h : ∀ a b c d, p a b c d ↔ q a b c d) :
+  (∀ a b c d, p a b c d) ↔ ∀ a b c d, q a b c d :=
+forall_congr $ λ a, forall₃_congr $ h a
+
+lemma forall₅_congr {p q : Π a b c d, ε a b c d → Prop}
+  (h : ∀ a b c d e, p a b c d e ↔ q a b c d e) :
+  (∀ a b c d e, p a b c d e) ↔ ∀ a b c d e, q a b c d e :=
+forall_congr $ λ a, forall₄_congr $ h a
+
+lemma exists₂_congr {p q : Π a, β a → Prop}  (h : ∀ a b, p a b ↔ q a b) :
+  (∃ a b, p a b) ↔ ∃ a b, q a b :=
+exists_congr $ λ a, exists_congr $ h a
+
+lemma exists₃_congr {p q : Π a b, γ a b → Prop} (h : ∀ a b c, p a b c ↔ q a b c) :
+  (∃ a b c, p a b c) ↔ ∃ a b c, q a b c :=
+exists_congr $ λ a, exists₂_congr $ h a
 
-lemma forall₂_congr {p q : α → β → Prop} (h : ∀ a b, p a b ↔ q a b) :
-  (∀ a b, p a b) ↔ (∀ a b, q a b) :=
-forall_congr (λ a, forall_congr (h a))
+lemma exists₄_congr {p q : Π a b c, δ a b c → Prop} (h : ∀ a b c d, p a b c d ↔ q a b c d) :
+  (∃ a b c d, p a b c d) ↔ ∃ a b c d, q a b c d :=
+exists_congr $ λ a, exists₃_congr $ h a
 
-lemma forall₃_congr {γ : Sort*} {p q : α → β → γ → Prop}
-  (h : ∀ a b c, p a b c ↔ q a b c) :
-  (∀ a b c, p a b c) ↔ (∀ a b c, q a b c) :=
-forall_congr (λ a, forall₂_congr (h a))
+lemma exists₅_congr {p q : Π a b c d, ε a b c d → Prop}
+  (h : ∀ a b c d e, p a b c d e ↔ q a b c d e) :
+  (∃ a b c d e, p a b c d e) ↔ ∃ a b c d e, q a b c d e :=
+exists_congr $ λ a, exists₄_congr $ h a
 
-lemma forall₄_congr {γ δ : Sort*} {p q : α → β → γ → δ → Prop}
-  (h : ∀ a b c d, p a b c d ↔ q a b c d) :
-  (∀ a b c d, p a b c d) ↔ (∀ a b c d, q a b c d) :=
-forall_congr (λ a, forall₃_congr (h a))
+end congr
+
+variables {β : Sort*} {p q : α → Prop} {b : Prop}
+
+lemma forall_imp (h : ∀ a, p a → q a) : (∀ a, p a) → ∀ a, q a :=
+λ h' a, h a (h' a)
 
 lemma Exists.imp (h : ∀ a, (p a → q a)) (p : ∃ a, p a) : ∃ a, q a := exists_imp_exists h p
 
 lemma exists_imp_exists' {p : α → Prop} {q : β → Prop} (f : α → β) (hpq : ∀ a, p a → q (f a))
   (hp : ∃ a, p a) : ∃ b, q b :=
 exists.elim hp (λ a hp', ⟨_, hpq _ hp'⟩)
 
-lemma exists₂_congr {p q : α → β → Prop} (h : ∀ a b, p a b ↔ q a b) :
-  (∃ a b, p a b) ↔ (∃ a b, q a b) :=
-exists_congr (λ a, exists_congr (h a))
-
-lemma exists₃_congr {γ : Sort*} {p q : α → β → γ → Prop}
-  (h : ∀ a b c, p a b c ↔ q a b c) :
-  (∃ a b c, p a b c) ↔ (∃ a b c, q a b c) :=
-exists_congr (λ a, exists₂_congr (h a))
-
-lemma exists₄_congr {γ δ : Sort*} {p q : α → β → γ → δ → Prop}
-  (h : ∀ a b c d, p a b c d ↔ q a b c d) :
-  (∃ a b c d, p a b c d) ↔ (∃ a b c d, q a b c d) :=
-exists_congr (λ a, exists₃_congr (h a))
-
 theorem forall_swap {p : α → β → Prop} : (∀ x y, p x y) ↔ ∀ y x, p x y :=
 ⟨swap, swap⟩
 
diff --git a/src/measure_theory/group/basic.lean b/src/measure_theory/group/basic.lean
@@ -76,8 +76,10 @@ variables [measurable_space G]
 lemma map_mul_left_eq_self [topological_space G] [has_mul G] [has_continuous_mul G] [borel_space G]
   {μ : measure G} : (∀ g, measure.map ((*) g) μ = μ) ↔ is_mul_left_invariant μ :=
 begin
-  apply forall_congr, intro g, rw [measure.ext_iff], apply forall_congr, intro A,
-  apply forall_congr, intro hA, rw [map_apply (measurable_const_mul g) hA]
+  refine forall_congr (λ g, _),
+  rw measure.ext_iff,
+  refine forall₂_congr (λ A hA, _),
+  rw [map_apply (measurable_const_mul g) hA]
 end
 
 @[to_additive]
@@ -94,8 +96,10 @@ lemma map_mul_right_eq_self [topological_space G] [has_mul G] [has_continuous_mu
   {μ : measure G} :
   (∀ g, measure.map (λ h, h * g) μ = μ) ↔ is_mul_right_invariant μ :=
 begin
-  apply forall_congr, intro g, rw [measure.ext_iff], apply forall_congr, intro A,
-  apply forall_congr, intro hA, rw [map_apply (measurable_mul_const g) hA]
+  refine forall_congr (λ g, _),
+  rw measure.ext_iff,
+  refine forall₂_congr (λ A hA, _),
+  rw [map_apply (measurable_mul_const g) hA]
 end
 
 /-- The measure `A ↦ μ (A⁻¹)`, where `A⁻¹` is the pointwise inverse of `A`. -/
diff --git a/src/measure_theory/measure/outer_measure.lean b/src/measure_theory/measure/outer_measure.lean
@@ -1242,7 +1242,7 @@ le_of_function.trans $ forall_congr $ λ s, le_infi_iff
 
 theorem trim_le_trim_iff {m₁ m₂ : outer_measure α} :
   m₁.trim ≤ m₂.trim ↔ ∀ s, measurable_set s → m₁ s ≤ m₂ s :=
-le_trim_iff.trans $ forall_congr $ λ s, forall_congr $ λ hs, by rw [trim_eq _ hs]
+le_trim_iff.trans $ forall₂_congr $ λ s hs, by rw [trim_eq _ hs]
 
 theorem trim_eq_trim_iff {m₁ m₂ : outer_measure α} :
   m₁.trim = m₂.trim ↔ ∀ s, measurable_set s → m₁ s = m₂ s :=
diff --git a/src/order/complete_lattice.lean b/src/order/complete_lattice.lean
@@ -1352,7 +1352,7 @@ lemma set_independent_iff {α : Type*} [complete_lattice α] (s : set α) :
   set_independent s ↔ independent (coe : s → α) :=
 begin
   simp_rw [independent, set_independent, set_coe.forall, Sup_eq_supr],
-  apply forall_congr, intro a, apply forall_congr, intro ha,
+  refine forall₂_congr (λ a ha, _),
   congr' 2,
   convert supr_subtype.symm,
   simp [supr_and],
diff --git a/src/order/filter/bases.lean b/src/order/filter/bases.lean
@@ -489,11 +489,11 @@ mem_iff_inf_principal_compl.trans disjoint_iff.symm
 
 lemma le_iff_forall_disjoint_principal_compl {f g : filter α} :
   f ≤ g ↔ ∀ V ∈ g, disjoint f (𝓟 Vᶜ) :=
-forall_congr $ λ _, forall_congr $ λ _, mem_iff_disjoint_principal_compl
+forall₂_congr $ λ _ _, mem_iff_disjoint_principal_compl
 
 lemma le_iff_forall_inf_principal_compl {f g : filter α} :
   f ≤ g ↔ ∀ V ∈ g, f ⊓ 𝓟 Vᶜ = ⊥ :=
-forall_congr $ λ _, forall_congr $ λ _, mem_iff_inf_principal_compl
+forall₂_congr $ λ _ _, mem_iff_inf_principal_compl
 
 lemma inf_ne_bot_iff_frequently_left {f g : filter α} :
   ne_bot (f ⊓ g) ↔ ∀ {p : α → Prop}, (∀ᶠ x in f, p x) → ∃ᶠ x in g, p x :=
diff --git a/src/order/filter/basic.lean b/src/order/filter/basic.lean
@@ -2446,13 +2446,10 @@ lemma mem_prod_principal {f : filter α} {s : set (α × β)} {t : set β}:
   s ∈ f ×ᶠ 𝓟 t ↔ {a | ∀ b ∈ t, (a, b) ∈ s} ∈ f :=
 begin
   rw [← @exists_mem_subset_iff _ f, mem_prod_iff],
-  apply exists_congr, intro u, apply exists_congr, intro u_in,
-  split,
+  refine exists₂_congr (λ u u_in, ⟨_, λ h, ⟨t, mem_principal_self t, _⟩⟩),
   { rintros ⟨v, v_in, hv⟩ a a_in b b_in,
     exact hv (mk_mem_prod a_in $ v_in b_in) },
-  { intro h,
-    refine ⟨t, mem_principal_self t, _⟩,
-    rintros ⟨x, y⟩ ⟨hx, hy⟩,
+  { rintro ⟨x, y⟩ ⟨hx, hy⟩,
     exact h hx y hy }
 end
 
diff --git a/src/order/filter/lift.lean b/src/order/filter/lift.lean
@@ -388,8 +388,8 @@ eventually_lift'_iff monotone_powerset
 lemma eventually_lift'_powerset' {f : filter α} {p : set α → Prop}
   (hp : ∀ ⦃s t⦄, s ⊆ t → p t → p s) :
   (∀ᶠ s in f.lift' powerset, p s) ↔ ∃ s ∈ f, p s :=
-eventually_lift'_powerset.trans $ exists_congr $ λ s, exists_congr $
-  λ hsf, ⟨λ H, H s (subset.refl s), λ hs t ht, hp ht hs⟩
+eventually_lift'_powerset.trans $ exists₂_congr $ λ s hsf,
+  ⟨λ H, H s (subset.refl s), λ hs t ht, hp ht hs⟩
 
 instance lift'_powerset_ne_bot (f : filter α) : ne_bot (f.lift' powerset) :=
 (lift'_ne_bot_iff monotone_powerset).2 $ λ _ _, powerset_nonempty
diff --git a/src/order/sup_indep.lean b/src/order/sup_indep.lean
@@ -104,7 +104,7 @@ lemma complete_lattice.independent_iff_sup_indep [complete_lattice α] {s : fins
 begin
   classical,
   rw finset.sup_indep_iff_disjoint_erase,
-  refine subtype.forall.trans (forall_congr $ λ a, forall_congr $ λ b, _),
+  refine subtype.forall.trans (forall₂_congr $ λ a b, _),
   rw finset.sup_eq_supr,
   congr' 2,
   refine supr_subtype.trans _,
diff --git a/src/ring_theory/local_properties.lean b/src/ring_theory/local_properties.lean
@@ -103,8 +103,8 @@ lemma ring_hom.of_localization_span_iff_finite :
   ring_hom.of_localization_span @P ↔ ring_hom.of_localization_finite_span @P :=
 begin
   delta ring_hom.of_localization_span ring_hom.of_localization_finite_span,
-  iterate 5 { apply forall_congr, intro _ },
-  resetI,
+  apply forall₅_congr, -- TODO: Using `refine` here breaks `resetI`.
+  introsI,
   split,
   { intros h s, exact h s },
   { intros h s hs hs',
diff --git a/src/topology/algebra/mul_action.lean b/src/topology/algebra/mul_action.lean
@@ -171,9 +171,8 @@ lemma continuous_within_at_const_smul_iff (c : G) :
 tendsto_const_smul_iff c
 
 @[to_additive]
-lemma continuous_on_const_smul_iff (c : G) :
-  continuous_on (λ x, c • f x) s ↔ continuous_on f s :=
-forall_congr $ λ b, forall_congr $ λ hb, continuous_within_at_const_smul_iff c
+lemma continuous_on_const_smul_iff (c : G) : continuous_on (λ x, c • f x) s ↔ continuous_on f s :=
+forall₂_congr $ λ b hb, continuous_within_at_const_smul_iff c
 
 @[to_additive]
 lemma continuous_at_const_smul_iff (c : G) :
diff --git a/src/topology/algebra/uniform_group.lean b/src/topology/algebra/uniform_group.lean
@@ -191,9 +191,9 @@ def topological_group.to_uniform_space : uniform_space G :=
     let S' := λ x, {p : G × G | p.1 = x → p.2 ∈ S},
     show is_open S ↔ ∀ (x : G), x ∈ S → S' x ∈ comap (λp:G×G, p.2 / p.1) (𝓝 (1 : G)),
     rw [is_open_iff_mem_nhds],
-    refine forall_congr (assume a, forall_congr (assume ha, _)),
+    refine forall₂_congr (λ a ha, _),
     rw [← nhds_translation_div, mem_comap, mem_comap],
-    refine exists_congr (assume t, exists_congr (assume ht, _)),
+    refine exists₂_congr (λ t ht, _),
     show (λ (y : G), y / a) ⁻¹' t ⊆ S ↔ (λ (p : G × G), p.snd / p.fst) ⁻¹' t ⊆ S' a,
     split,
     { rintros h ⟨x, y⟩ hx rfl, exact h hx },
diff --git a/src/topology/local_homeomorph.lean b/src/topology/local_homeomorph.lean
diff --git a/src/topology/metric_space/basic.lean b/src/topology/metric_space/basic.lean
diff --git a/src/topology/separation.lean b/src/topology/separation.lean
diff --git a/src/topology/sheaves/sheaf_condition/opens_le_cover.lean b/src/topology/sheaves/sheaf_condition/opens_le_cover.lean
diff --git a/src/topology/uniform_space/basic.lean b/src/topology/uniform_space/basic.lean
diff --git a/src/topology/uniform_space/compact_convergence.lean b/src/topology/uniform_space/compact_convergence.lean
diff --git a/src/topology/uniform_space/separation.lean b/src/topology/uniform_space/separation.lean
diff --git a/src/topology/uniform_space/uniform_convergence.lean b/src/topology/uniform_space/uniform_convergence.lean
