feat(tactic/congr): additions to the congr' tactic (#3936)

This PR gives a way to apply `ext` after `congr'`.
`congr' 3 with x y : 2` is a new notation for `congr' 3; ext x y : 2`.
New tactic `rcongr` that recursively keeps applying `congr'` and `ext`.
Move `congr'` and every tactic depending on it from `tactic/interactive` to a new file `tactic/congr`.
The original `tactic.interactive.congr'` is now best called as `tactic.congr'`. 
Other than the tactics `congr'` and `rcongr` no tactics have been (essentially) changed.

archive/sensitivity.lean

@@ -410,7 +410,7 @@ begin
     ... = ∑ p in (coeffs y).support.filter (Q.adjacent q), |coeffs y p|     : by simp [finset.sum_filter]
     ... ≤ ∑ p in (coeffs y).support.filter (Q.adjacent q), |coeffs y q|     : finset.sum_le_sum (λ p _, H_max p)
     ... = (finset.card ((coeffs y).support.filter (Q.adjacent q)): ℝ) * |coeffs y q| : by rw [finset.sum_const, nsmul_eq_mul]
-    ... = (finset.card ((coeffs y).support ∩ (Q.adjacent q).to_finset): ℝ) * |coeffs y q| : by {congr, ext, simp, refl}
+    ... = (finset.card ((coeffs y).support ∩ (Q.adjacent q).to_finset): ℝ) * |coeffs y q| : by { congr' with x, simp, refl }
     ... ≤ (finset.card ((H ∩ Q.adjacent q).to_finset )) * |ε q y| :
      (mul_le_mul_right H_q_pos).mpr (by {
              norm_cast,

src/algebra/big_operators/ring.lean

@@ -47,7 +47,7 @@ end semiring
 lemma sum_div [division_ring β] {s : finset α} {f : α → β} {b : β} :
   (∑ x in s, f x) / b = ∑ x in s, f x / b :=
 calc (∑ x in s, f x) / b = ∑ x in s, f x * (1 / b) : by rw [div_eq_mul_one_div, sum_mul]
-                     ... = ∑ x in s, f x / b : by { congr, ext, rw ← div_eq_mul_one_div (f x) b }
+                     ... = ∑ x in s, f x / b : by { congr' with x, rw ← div_eq_mul_one_div (f x) b }
 
 section comm_semiring
 variables [comm_semiring β]
@@ -78,7 +78,7 @@ begin
     refine sum_congr rfl (λ g _, _),
     rw [attach_insert, prod_insert, prod_image],
     { simp only [pi.cons_same],
-      congr', ext ⟨v, hv⟩, congr',
+      congr' with ⟨v, hv⟩, congr',
       exact (pi.cons_ne (by rintro rfl; exact ha hv)).symm },
     { exact λ _ _ _ _, subtype.eq ∘ subtype.mk.inj },
     { simp only [mem_image], rintro ⟨⟨_, hm⟩, _, rfl⟩, exact ha hm } }

src/algebra/group_action_hom.lean

@@ -62,7 +62,7 @@ variables {M X Y}
 f.map_smul' m x
 
 @[ext] theorem ext : ∀ {f g : X →[M] Y}, (∀ x, f x = g x) → f = g
-| ⟨f, _⟩ ⟨g, _⟩ H := by { congr' 1, ext x, exact H x }
+| ⟨f, _⟩ ⟨g, _⟩ H := by { congr' 1 with x, exact H x }
 
 theorem ext_iff {f g : X →[M] Y} : f = g ↔ ∀ x, f x = g x :=
 ⟨λ H x, by rw H, ext⟩
@@ -132,7 +132,7 @@ variables {M A B}
 @[norm_cast] lemma coe_fn_coe' (f : A →+[M] B) : ((f : A →[M] B) : A → B) = f := rfl
 
 @[ext] theorem ext : ∀ {f g : A →+[M] B}, (∀ x, f x = g x) → f = g
-| ⟨f, _, _, _⟩ ⟨g, _, _, _⟩ H := by { congr' 1, ext x, exact H x }
+| ⟨f, _, _, _⟩ ⟨g, _, _, _⟩ H := by { congr' 1 with x, exact H x }
 
 theorem ext_iff {f g : A →+[M] B} : f = g ↔ ∀ x, f x = g x :=
 ⟨λ H x, by rw H, ext⟩
@@ -206,7 +206,7 @@ variables {M R S}
 @[norm_cast] lemma coe_fn_coe' (f : R →+*[M] S) : ((f : R →+[M] S) : R → S) = f := rfl
 
 @[ext] theorem ext : ∀ {f g : R →+*[M] S}, (∀ x, f x = g x) → f = g
-| ⟨f, _, _, _, _, _⟩ ⟨g, _, _, _, _, _⟩ H := by { congr' 1, ext x, exact H x }
+| ⟨f, _, _, _, _, _⟩ ⟨g, _, _, _, _, _⟩ H := by { congr' 1 with x, exact H x }
 
 theorem ext_iff {f g : R →+*[M] S} : f = g ↔ ∀ x, f x = g x :=
 ⟨λ H x, by rw H, ext⟩

src/algebra/linear_recurrence.lean

@@ -83,8 +83,7 @@ lemma eq_mk_of_is_sol_of_eq_init {u : ℕ → α} {init : fin E.order → α}
   else begin
     rw [mk_sol, ← nat.sub_add_cancel (le_of_not_lt h'), h (n-E.order)],
     simp [h'],
-    congr',
-    ext k,
+    congr' with k,
     exact have wf : n - E.order + k.1 < n, by have := k.2; omega,
       by rw eq_mk_of_is_sol_of_eq_init
   end

src/analysis/analytic/basic.lean

@@ -522,7 +522,7 @@ begin
       = ∑ s : finset (fin n), nnnorm (p n) * ((nnnorm x) ^ (n - s.card) * r ^ s.card) :
         by simp [← mul_assoc]
       ... = nnnorm (p n) * (nnnorm x + r) ^ n :
-      by { rw [add_comm, ← finset.mul_sum, ← fin.sum_pow_mul_eq_add_pow], congr, ext1 s, ring }
+      by { rw [add_comm, ← finset.mul_sum, ← fin.sum_pow_mul_eq_add_pow], congr' with s : 1, ring }
     end
   ... ≤ (∑' (n : ℕ), (C * a ^ n : ennreal)) :
     tsum_le_tsum (λ n, by exact_mod_cast hC n) ennreal.summable ennreal.summable

src/analysis/analytic/composition.lean

@@ -227,8 +227,7 @@ begin
   rw ← this,
   simp only [finset.sum_singleton, continuous_multilinear_map.sum_apply],
   change q c.length (p.apply_composition c v) = q 0 v',
-  congr,
-  ext i,
+  congr' with i,
   simp only [composition.ones_length] at i,
   exact fin_zero_elim i
 end
@@ -428,8 +427,7 @@ begin
   ... = (∑' (n : ℕ), (∑' (c : composition n), (Cq : ennreal) * a ^ n)) : ennreal.tsum_sigma' _
   ... = (∑' (n : ℕ), ↑(fintype.card (composition n)) * (Cq : ennreal) * a ^ n) :
     begin
-      congr' 1,
-      ext1 n,
+      congr' 1 with n : 1,
       rw [tsum_fintype, finset.sum_const, nsmul_eq_mul, finset.card_univ, mul_assoc]
     end
   ... ≤ (∑' (n : ℕ), (2 : ennreal) ^ n * (Cq : ennreal) * a ^ n) :
@@ -443,7 +441,7 @@ begin
       rw ← ennreal.coe_le_coe at this,
       exact this
     end
-  ... = (∑' (n : ℕ), (Cq : ennreal) * (2 * a) ^ n) : by { congr' 1, ext1 n, rw mul_pow, ring }
+  ... = (∑' (n : ℕ), (Cq : ennreal) * (2 * a) ^ n) : by { congr' 1 with n : 1, rw mul_pow, ring }
   ... = (Cq : ennreal) * (1 - 2 * a) ⁻¹ : by rw [ennreal.tsum_mul_left, ennreal.tsum_geometric]
   ... < ⊤ : by simp [lt_top_iff_ne_top, ennreal.mul_eq_top, two_a]
 end
@@ -838,10 +836,7 @@ begin
   rcases j with ⟨a', b'⟩,
   rintros ⟨h, h'⟩,
   have H : a = a', by { ext1, exact h },
-  induction H,
-  congr,
-  ext1,
-  exact h'
+  induction H, congr, ext1, exact h'
 end
 
 /-- Rewriting equality in the dependent type

src/analysis/calculus/times_cont_diff.lean

@@ -224,7 +224,7 @@ multilinear series are equal, then the values are also equal. -/
 lemma congr (p : formal_multilinear_series 𝕜 E F) {m n : ℕ} {v : fin m → E} {w : fin n → E}
   (h1 : m = n) (h2 : ∀ (i : ℕ) (him : i < m) (hin : i < n), v ⟨i, him⟩ = w ⟨i, hin⟩) :
   p m v = p n w :=
-by { cases h1, congr, ext ⟨i, hi⟩, exact h2 i hi hi }
+by { cases h1, congr' with ⟨i, hi⟩, exact h2 i hi hi }
 
 end formal_multilinear_series
 
@@ -328,8 +328,7 @@ begin
   ext y v,
   change (p x 1) (snoc 0 y) = (p x 1) (cons y v),
   unfold_coes,
-  congr,
-  ext i,
+  congr' with i,
   have : i = 0 := subsingleton.elim i 0,
   rw this,
   refl

src/analysis/convex/basic.lean

@@ -871,7 +871,7 @@ lemma finset.center_mass_segment'
 begin
   rw [s.center_mass_eq_of_sum_1 _ hws, t.center_mass_eq_of_sum_1 _ hwt,
     smul_sum, smul_sum, ← finset.sum_sum_elim, finset.center_mass_eq_of_sum_1],
-  { congr, ext ⟨⟩; simp only [sum.elim_inl, sum.elim_inr, mul_smul] },
+  { congr' with ⟨⟩; simp only [sum.elim_inl, sum.elim_inr, mul_smul] },
   { rw [sum_sum_elim, ← mul_sum, ← mul_sum, hws, hwt, mul_one, mul_one, hab] }
 end
 
@@ -891,7 +891,7 @@ lemma finset.center_mass_ite_eq (hi : i ∈ t) :
 begin
   rw [finset.center_mass_eq_of_sum_1],
   transitivity ∑ j in t, if (i = j) then z i else 0,
-  { congr, ext i, split_ifs, exacts [h ▸ one_smul _ _, zero_smul _ _] },
+  { congr' with i, split_ifs, exacts [h ▸ one_smul _ _, zero_smul _ _] },
   { rw [sum_ite_eq, if_pos hi] },
   { rw [sum_ite_eq, if_pos hi] }
 end

src/analysis/hofer.lean

@@ -72,7 +72,7 @@ begin
           ≤ ∑ i in r, d (u i) (u $ i+1) : dist_le_range_sum_dist u (n + 1)
       ... ≤ ∑ i in r, ε/2^i             : sum_le_sum (λ i i_in, (IH i $ nat.lt_succ_iff.mp $
                                                                   finset.mem_range.mp i_in).1)
-      ... = ∑ i in r, (1/2)^i*ε         : by { congr, ext i, field_simp }
+      ... = ∑ i in r, (1/2)^i*ε         : by { congr' with i, field_simp }
       ... = (∑ i in r, (1/2)^i)*ε       : finset.sum_mul.symm
       ... ≤ 2*ε                         : mul_le_mul_of_nonneg_right (sum_geometric_two_le _)
                                             (le_of_lt ε_pos), },

src/analysis/normed_space/multilinear.lean

@@ -122,10 +122,10 @@ begin
     -- use the bound on `f` on the ball of size `δ` to conclude.
     calc
       ∥f m∥ = ∥f (λi, (d i)⁻¹ • (d i • m i))∥ :
-        by { unfold_coes, congr, ext i, rw [← mul_smul, inv_mul_cancel (hd i).1, one_smul] }
+        by { unfold_coes, congr' with i, rw [← mul_smul, inv_mul_cancel (hd i).1, one_smul] }
       ... = ∥(∏ i, (d i)⁻¹) • f (λi, d i • m i)∥ : by rw f.map_smul_univ
       ... = (∏ i, ∥d i∥⁻¹) * ∥f (λi, d i • m i)∥ :
-        by { rw [norm_smul, normed_field.norm_prod], congr, ext i, rw normed_field.norm_inv }
+        by { rw [norm_smul, normed_field.norm_prod], congr' with i, rw normed_field.norm_inv }
       ... ≤ (∏ i, ∥d i∥⁻¹) * (1 + ∥f 0∥) :
         mul_le_mul_of_nonneg_left (H ((pi_norm_le_iff (le_of_lt δ_pos)).2 (λi, (hd i).2.1)))
           (prod_nonneg B)

src/analysis/special_functions/exp_log.lean

@@ -487,8 +487,7 @@ begin
   have A : ∀ y ∈ set.Ioo (-1 : ℝ) 1, deriv F y = - (y^n) / (1 - y),
   { assume y hy,
     have : (∑ i in range n, (↑i + 1) * y ^ i / (↑i + 1)) = (∑ i in range n, y ^ i),
-    { congr,
-      ext i,
+    { congr' with i,
       have : (i : ℝ) + 1 ≠ 0 := ne_of_gt (nat.cast_add_one_pos i),
       field_simp [this, mul_comm] },
     field_simp [F, this, ← geom_series_def, geom_sum (ne_of_lt hy.2),

src/category_theory/limits/limits.lean

@@ -323,8 +323,7 @@ lemma cone_of_hom_fac {Y : C} (f : Y ⟶ X) :
 cone_of_hom h f = (limit_cone h).extend f :=
 begin
   dsimp [cone_of_hom, limit_cone, cone.extend],
-  congr,
-  ext j,
+  congr' with j,
   have t := congr_fun (h.hom.naturality f.op) (𝟙 X),
   dsimp at t,
   simp only [comp_id] at t,
@@ -366,8 +365,7 @@ def of_nat_iso {X : C} (h : yoneda.obj X ≅ F.cones) :
     rw ←hom_of_cone_of_hom h m,
     congr,
     rw cone_of_hom_fac,
-    dsimp, cases s, congr,
-    ext j, exact w j,
+    dsimp, cases s, congr' with j, exact w j,
   end }
 end
 
@@ -652,8 +650,7 @@ lemma cocone_of_hom_fac {Y : C} (f : X ⟶ Y) :
 cocone_of_hom h f = (colimit_cocone h).extend f :=
 begin
   dsimp [cocone_of_hom, colimit_cocone, cocone.extend],
-  congr,
-  ext j,
+  congr' with j,
   have t := congr_fun (h.hom.naturality f) (𝟙 X),
   dsimp at t,
   simp only [id_comp] at t,
@@ -695,8 +692,7 @@ def of_nat_iso {X : C} (h : coyoneda.obj (op X) ≅ F.cocones) :
     rw ←hom_of_cocone_of_hom h m,
     congr,
     rw cocone_of_hom_fac,
-    dsimp, cases s, congr,
-    ext j, exact w j,
+    dsimp, cases s, congr' with j, exact w j,
   end }
 end
 

src/computability/turing_machine.lean

@@ -1278,7 +1278,7 @@ end
 theorem tr_eval (l : list Γ) : TM0.eval tr l = TM1.eval M l :=
 (congr_arg _ (tr_eval' _ _ _ tr_respects ⟨some _, _, _⟩)).trans begin
   rw [roption.map_eq_map, roption.map_map, TM1.eval],
-  congr', ext ⟨⟩, refl
+  congr' with ⟨⟩, refl
 end
 
 variables [fintype σ]

src/control/monad/cont.lean

@@ -115,7 +115,7 @@ instance {ε} [monad_cont m] : monad_cont (except_t ε m) :=
 
 instance {ε} [monad_cont m] [is_lawful_monad_cont m] : is_lawful_monad_cont (except_t ε m) :=
 { call_cc_bind_right := by { intros, simp [call_cc,except_t.call_cc,call_cc_bind_right], ext, dsimp,
-    congr, ext ⟨ ⟩; simp [except_t.bind_cont,@call_cc_dummy m _], },
+    congr' with ⟨ ⟩; simp [except_t.bind_cont,@call_cc_dummy m _], },
   call_cc_bind_left  := by { intros,
     simp [call_cc,except_t.call_cc,call_cc_bind_right,except_t.goto_mk_label,map_eq_bind_pure_comp,
       bind_assoc,@call_cc_bind_left m _], ext, refl },
@@ -136,7 +136,7 @@ instance [monad_cont m] : monad_cont (option_t m) :=
 
 instance [monad_cont m] [is_lawful_monad_cont m] : is_lawful_monad_cont (option_t m) :=
 { call_cc_bind_right := by { intros, simp [call_cc,option_t.call_cc,call_cc_bind_right], ext, dsimp,
-    congr, ext ⟨ ⟩; simp [option_t.bind_cont,@call_cc_dummy m _], },
+    congr' with ⟨ ⟩; simp [option_t.bind_cont,@call_cc_dummy m _], },
   call_cc_bind_left  := by { intros, simp [call_cc,option_t.call_cc,call_cc_bind_right,
     option_t.goto_mk_label,map_eq_bind_pure_comp,bind_assoc,@call_cc_bind_left m _], ext, refl },
   call_cc_dummy := by { intros, simp [call_cc,option_t.call_cc,@call_cc_dummy m _], ext, refl }, }
@@ -169,8 +169,8 @@ instance {σ} [monad_cont m] : monad_cont (state_t σ m) :=
 
 instance {σ} [monad_cont m] [is_lawful_monad_cont m] : is_lawful_monad_cont (state_t σ m) :=
 { call_cc_bind_right := by { intros,
-    simp [call_cc,state_t.call_cc,call_cc_bind_right,(>>=),state_t.bind], ext, dsimp, congr,
-    ext ⟨x₀,x₁⟩, refl },
+    simp [call_cc,state_t.call_cc,call_cc_bind_right,(>>=),state_t.bind], ext, dsimp,
+    congr' with ⟨x₀,x₁⟩, refl },
   call_cc_bind_left  := by { intros, simp [call_cc,state_t.call_cc,call_cc_bind_left,(>>=),
     state_t.bind,state_t.goto_mk_label], ext, refl },
   call_cc_dummy := by { intros, simp [call_cc,state_t.call_cc,call_cc_bind_right,(>>=),

src/data/finset/lattice.lean

@@ -486,7 +486,7 @@ lemma supr_insert_update {x : α} {t : finset α} (f : α → β) {s : β} (hx :
   (⨆ (i ∈ insert x t), function.update f x s i) = (s ⊔ ⨆ (i ∈ t), f i) :=
 begin
   simp only [finset.supr_insert, update_same],
-  congr' 2, ext i, congr' 1, ext hi, apply update_noteq, rintro rfl, exact hx hi
+  rcongr i hi, apply update_noteq, rintro rfl, exact hx hi
 end
 
 lemma infi_insert_update {x : α} {t : finset α} (f : α → β) {s : β} (hx : x ∉ t) :

src/data/list/func.lean

@@ -279,7 +279,7 @@ by {apply get_pointwise, apply zero_add}
 begin
   rw [add, @nil_pointwise α α α ⟨0⟩ ⟨0⟩],
   apply eq.trans _ (map_id as),
-  congr, ext,
+  congr' with x,
   have : @default α ⟨0⟩ = 0 := rfl,
   rw [this, zero_add], refl
 end
@@ -289,7 +289,7 @@ end
 begin
   rw [add, @pointwise_nil α α α ⟨0⟩ ⟨0⟩],
   apply eq.trans _ (map_id as),
-  congr, ext,
+  congr' with x,
   have : @default α ⟨0⟩ = 0 := rfl,
   rw [this, add_zero], refl
 end
@@ -326,7 +326,7 @@ by {apply get_pointwise, apply sub_zero}
   (as : list α) : sub [] as = neg as :=
 begin
   rw [sub, nil_pointwise],
-  congr, ext,
+  congr' with x,
   have : @default α ⟨0⟩ = 0 := rfl,
   rw [this, zero_sub]
 end
@@ -336,7 +336,7 @@ end
 begin
   rw [sub, pointwise_nil],
   apply eq.trans _ (map_id as),
-  congr, ext,
+  congr' with x,
   have : @default α ⟨0⟩ = 0 := rfl,
   rw [this, sub_zero], refl
 end

src/data/list/sigma.lean

@@ -92,7 +92,7 @@ theorem nodupkeys_join {L : list (list (sigma β))} :
 begin
   rw [nodupkeys_iff_pairwise, pairwise_join, pairwise_map],
   refine and_congr (ball_congr $ λ l h, by simp [nodupkeys_iff_pairwise]) _,
-  apply iff_of_eq, congr', ext l₁ l₂,
+  apply iff_of_eq, congr' with l₁ l₂,
   simp [keys, disjoint_iff_ne]
 end
 

src/data/monoid_algebra.lean

@@ -195,7 +195,7 @@ have f.sum (λ a b, ite (x * a = y) (0 * b) 0) = 0, by simp,
 calc (single x r * f) y = sum f (λ a b, ite (x * a = y) (r * b) 0) :
   (mul_apply _ _ _).trans $ sum_single_index this
 ... = f.sum (λ a b, ite (a = z) (r * b) 0) :
-  by { simp only [H], congr, ext; split_ifs; refl  }
+  by { simp only [H], congr' with g s, split_ifs; refl  }
 ... = if z ∈ f.support then (r * f z) else 0 : f.support.sum_ite_eq' _ _
 ... = _ : by split_ifs with h; simp at h; simp [h]
 
@@ -559,7 +559,7 @@ have f.sum (λ a b, ite (x + a = y) (0 * b) 0) = 0, by simp,
 calc (single x r * f) y = sum f (λ a b, ite (x + a = y) (r * b) 0) :
   (mul_apply _ _ _).trans $ sum_single_index this
 ... = f.sum (λ a b, ite (a = z) (r * b) 0) :
-  by { simp only [H], congr, ext; split_ifs; refl  }
+  by { simp only [H], congr' with g s, split_ifs; refl  }
 ... = if z ∈ f.support then (r * f z) else 0 : f.support.sum_ite_eq' _ _
 ... = _ : by split_ifs with h; simp at h; simp [h]
 

src/data/mv_polynomial.lean

@@ -388,7 +388,7 @@ lemma coeff_mul_X' (m) (s : σ) (p : mv_polynomial σ α) :
 begin
   split_ifs with h h,
   { conv_rhs {rw ← coeff_mul_X _ s},
-    congr' 1, ext t,
+    congr' with  t,
     by_cases hj : s = t,
     { subst t, simp only [nat_sub_apply, add_apply, single_eq_same],
       refine (nat.sub_add_cancel $ nat.pos_of_ne_zero _).symm, rwa mem_support_iff at h },
@@ -550,7 +550,7 @@ lemma eval₂_assoc (q : γ → mv_polynomial σ α) (p : mv_polynomial γ α) :
   eval₂ f (λ t, eval₂ f g (q t)) p = eval₂ f g (eval₂ C q p) :=
 begin
   show _ = eval₂_hom f g (eval₂ C q p),
-  rw eval₂_comp_left (eval₂_hom f g), congr, ext a, simp,
+  rw eval₂_comp_left (eval₂_hom f g), congr' with a, simp,
 end
 
 end eval₂
@@ -592,7 +592,7 @@ theorem eval_assoc {τ}
 begin
   rw eval₂_comp_left (eval g),
   unfold eval, simp only [coe_eval₂_hom],
-  congr, ext a, simp
+  congr' with a, simp
 end
 
 end eval
@@ -1121,9 +1121,9 @@ lemma rename_eq (f : β → γ) (p : mv_polynomial β α) :
   rename f p = finsupp.map_domain (finsupp.map_domain f) p :=
 begin
   simp only [rename, eval₂_hom, eval₂, finsupp.map_domain, ring_hom.coe_of],
-  congr, ext s a : 2,
+  congr' with s a : 2,
   rw [← monomial, monomial_eq, finsupp.prod_sum_index],
-  congr, ext n i : 2,
+  congr' with n i : 2,
   rw [finsupp.prod_single_index],
   exact pow_zero _,
   exact assume a, pow_zero _,

src/data/pfunctor/multivariate/M.lean

@@ -228,7 +228,7 @@ begin
     rcases M.bisim_lemma P e₂ with ⟨g₂', e₂', _, rfl⟩,
     rw [e₁', e₂'],
     exact ⟨_, _, _, rfl, rfl, λ b, ⟨_, _, h' b, rfl, rfl⟩⟩ },
-  subst this, congr, ext i p,
+  subst this, congr' with i p,
   induction p with x a f h' i c x a f h' i c p IH generalizing f₁ f₂;
   try {
     rcases h _ _ r with ⟨a', f', f₁', f₂', e₁, e₂, h''⟩,