style(*): use rcases patterns with ext (#3018)

Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

src/analysis/analytic/basic.lean

@@ -510,7 +510,7 @@ begin
     λ ⟨n, s⟩, nnnorm (p n) * (nnnorm x) ^ (n - s.card) * r ^ s.card,
   have : ((λ ⟨n, s⟩, ∥p n∥ * ∥x∥ ^ (n - s.card) * r ^ s.card) :
     (Σ (n : ℕ), finset (fin n)) → ℝ) = (λ b, (Bnnnorm b : ℝ)),
-    by { ext b, rcases b with ⟨n, s⟩, simp [Bnnnorm, nnreal.coe_pow, coe_nnnorm] },
+    by { ext ⟨n, s⟩, simp [Bnnnorm, nnreal.coe_pow, coe_nnnorm] },
   rw [this, nnreal.summable_coe, ← ennreal.tsum_coe_ne_top_iff_summable],
   apply ne_of_lt,
   calc (∑' b, ↑(Bnnnorm b))
@@ -560,8 +560,7 @@ begin
       right_inv := λ ⟨k, n, s, hs⟩, by { induction hs, refl } },
   rw ← e.summable_iff,
   convert SAnorm,
-  ext i,
-  rcases i with ⟨n, s⟩,
+  ext ⟨n, s⟩,
   refl
 end
 
@@ -592,12 +591,12 @@ begin
   { convert summable.summable_comp_of_injective (p.change_origin_summable_aux2 hr)
       (change_origin_summable_aux_j_inj k),
     -- again, cleanup that could be done by `tidy`:
-    ext p, rcases p with ⟨_, ⟨_, _⟩⟩, refl },
+    ext ⟨_, ⟨_, _⟩⟩, refl },
   have : (r : ℝ)^k ≠ 0, by simp [pow_ne_zero, nnreal.coe_eq_zero, ne_of_gt rpos],
   apply (summable_mul_right_iff this).2,
   convert S,
   -- again, cleanup that could be done by `tidy`:
-  ext p, rcases p with ⟨_, ⟨_, _⟩⟩, refl,
+  ext ⟨_, ⟨_, _⟩⟩, refl,
 end
 
 -- FIXME this causes a deterministic timeout with `-T50000`
@@ -714,7 +713,7 @@ begin
       inv_fun := λ ⟨k, n, s, hs⟩, ⟨n, s⟩,
       left_inv := λ ⟨n, s⟩, rfl,
       right_inv := λ ⟨k, n, s, hs⟩, by { induction hs, refl } },
-    have : A ∘ e = B, by { ext x, cases x, refl },
+    have : A ∘ e = B, by { ext ⟨⟩, refl },
     rw ← e.has_sum_iff,
     convert has_sum_B },
   -- Summing `A ⟨k, c⟩` with fixed `k` and varying `c` is exactly the `k`-th term in the series

src/analysis/calculus/fderiv.lean

@@ -1790,8 +1790,7 @@ begin
   simp only [mul_one, is_o_norm_right] at this,
   refine (is_o.congr_of_sub _).1 this, clear this,
   convert_to is_o (λ q : T, h.deriv (p - q.2) (q.1 - q.2)) (λ q : T, q.1 - q.2) (𝓝 (p, p)),
-  { ext q,
-    rcases q with ⟨⟨x₁, y₁⟩, ⟨x₂, y₂⟩⟩, rcases p with ⟨x, y⟩,
+  { ext ⟨⟨x₁, y₁⟩, ⟨x₂, y₂⟩⟩, rcases p with ⟨x, y⟩,
     simp only [is_bounded_bilinear_map_deriv_coe, prod.mk_sub_mk, h.map_sub_left, h.map_sub_right],
     abel },
   have : is_o (λ q : T, p - q.2) (λ q, (1:ℝ)) (𝓝 (p, p)),

src/analysis/calculus/times_cont_diff.lean

@@ -200,7 +200,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, funext i, cases i with i hi, exact h2 i hi hi }
+by { cases h1, congr, ext ⟨i, hi⟩, exact h2 i hi hi }
 
 end formal_multilinear_series
 

src/analysis/convex/basic.lean

@@ -571,7 +571,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 i, cases i; simp only [sum.elim_inl, sum.elim_inr, mul_smul] },
+  { congr, ext ⟨⟩; 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
 

src/category_theory/limits/shapes/binary_products.lean

@@ -65,8 +65,8 @@ def map_pair : F ⟶ G :=
 def map_pair_iso (f : F.obj left ≅ G.obj left) (g : F.obj right ≅ G.obj right) : F ≅ G :=
 { hom := map_pair f.hom g.hom,
   inv := map_pair f.inv g.inv,
-  hom_inv_id' := begin ext j, cases j; { dsimp, simp, } end,
-  inv_hom_id' := begin ext j, cases j; { dsimp, simp, } end }
+  hom_inv_id' := begin ext ⟨⟩; { dsimp, simp, } end,
+  inv_hom_id' := begin ext ⟨⟩; { dsimp, simp, } end }
 end
 
 section

src/category_theory/limits/shapes/constructions/limits_of_products_and_equalizers.lean

@@ -82,8 +82,7 @@ local attribute [semireducible] op unop opposite
   begin
     refine (fork.of_ι _ _).π,
     { exact pi.lift c.app },
-    { ext f,
-      rcases f with ⟨⟨A,B⟩,f⟩,
+    { ext ⟨⟨A,B⟩,f⟩,
       dsimp,
       simp only [limit.lift_π, limit.lift_π_assoc, fan.mk_π_app, category.assoc],
       rw ←(c.naturality f),

src/data/equiv/basic.lean

@@ -368,7 +368,7 @@ def arrow_punit_equiv_punit (α : Sort*) : (α → punit.{v}) ≃ punit.{w} :=
 
 /-- The sort of maps from `punit` is equivalent to the codomain. -/
 def punit_arrow_equiv (α : Sort*) : (punit.{u} → α) ≃ α :=
-⟨λ f, f punit.star, λ a u, a, λ f, by { funext x, cases x, refl }, λ u, rfl⟩
+⟨λ f, f punit.star, λ a u, a, λ f, by { ext ⟨⟩, refl }, λ u, rfl⟩
 
 /-- The sort of maps from `empty` is equivalent to `punit`. -/
 def empty_arrow_equiv_punit (α : Sort*) : (empty → α) ≃ punit.{u} :=
@@ -738,7 +738,7 @@ on `α` and on `β`. -/
 def sum_arrow_equiv_prod_arrow (α β γ : Type*) : ((α ⊕ β) → γ) ≃ (α → γ) × (β → γ) :=
 ⟨λ f, (f ∘ inl, f ∘ inr),
  λ p, sum.elim p.1 p.2,
- λ f, by { funext s, cases s; refl },
+ λ f, by { ext ⟨⟩; refl },
  λ p, by { cases p, refl }⟩
 
 /-- Type product is right distributive with respect to type sum up to an equivalence. -/

src/data/finset.lean

@@ -2448,8 +2448,7 @@ the increasing bijection `mono_of_fin s h`. For a statement assuming only that `
 lemma mono_of_fin_unique {s : finset α} {k : ℕ} (h : s.card = k) {f : fin k → α}
   (hbij : set.bij_on f set.univ ↑s) (hmono : strict_mono f) : f = s.mono_of_fin h :=
 begin
-  ext i,
-  rcases i with ⟨i, hi⟩,
+  ext ⟨i, hi⟩,
   induction i using nat.strong_induction_on with i IH,
   rcases lt_trichotomy (f ⟨i, hi⟩) (mono_of_fin s h ⟨i, hi⟩) with H|H|H,
   { have A : f ⟨i, hi⟩ ∈ ↑s := hbij.maps_to (set.mem_univ _),

src/data/seq/computation.lean

@@ -504,7 +504,7 @@ by apply s.cases_on; intro; simp
 | ⟨f, al⟩ := begin
   apply subtype.eq; simp [map, function.comp],
   have e : (@option.rec α (λ_, option α) none some) = id,
-  { funext x, cases x; refl },
+  { ext ⟨⟩; refl },
   simp [e, stream.map_id]
 end
 
@@ -514,7 +514,7 @@ theorem map_comp (f : α → β) (g : β → γ) :
   apply subtype.eq; dsimp [map],
   rw stream.map_map,
   apply congr_arg (λ f : _ → option γ, stream.map f s),
-  funext x, cases x with x; refl
+  ext ⟨⟩; refl
 end
 
 @[simp] theorem ret_bind (a) (f : α → computation β) :

src/data/seq/seq.lean

@@ -516,7 +516,7 @@ theorem map_comp (f : α → β) (g : β → γ) : ∀ (s : seq α), map (g ∘
   apply subtype.eq; dsimp [map],
   rw stream.map_map,
   apply congr_arg (λ f : _ → option γ, stream.map f s),
-  funext x, cases x with x; refl
+  ext ⟨⟩; refl
 end
 
 @[simp] theorem map_append (f : α → β) (s t) : map f (append s t) = append (map f s) (map f t) :=
@@ -594,7 +594,7 @@ end
   of_list (a :: l) = cons a (of_list l) :=
 begin
   apply subtype.eq, simp [of_list, cons],
-  funext n, cases n; simp [list.nth, stream.cons]
+  ext ⟨⟩; simp [list.nth, stream.cons]
 end
 
 @[simp] theorem of_stream_cons (a : α) (s) :

src/data/seq/wseq.lean

@@ -556,8 +556,7 @@ theorem destruct_tail (s : wseq α) :
   destruct (tail s) = destruct s >>= tail.aux :=
 begin
   dsimp [tail], simp, rw [← bind_pure_comp_eq_map, is_lawful_monad.bind_assoc],
-  apply congr_arg, funext o,
-  rcases o with _|⟨a, s⟩;
+  apply congr_arg, ext (_|⟨a, s⟩);
   apply (@pure_bind computation _ _ _ _ _ _).trans _; simp
 end
 
@@ -1007,7 +1006,7 @@ theorem map_comp (f : α → β) (g : β → γ) (s : wseq α) :
 begin
   dsimp [map], rw ←seq.map_comp,
   apply congr_fun, apply congr_arg,
-  funext o, cases o; refl
+  ext ⟨⟩; refl
 end
 
 theorem mem_map (f : α → β) {a : α} {s : wseq α} : a ∈ s → f a ∈ map f s :=

src/data/set/countable.lean

@@ -176,8 +176,7 @@ begin
   haveI : encodable t := ht.to_encodable,
   haveI : encodable (s × t) := by apply_instance,
   have : range (λp, ⟨p.1, p.2⟩ : s × t → α × β) = set.prod s t,
-  { ext z,
-    rcases z with ⟨x, y⟩,
+  { ext ⟨x, y⟩,
     simp only [exists_prop, set.mem_range, set_coe.exists, prod.mk.inj_iff,
                set.prod_mk_mem_set_prod_eq, subtype.coe_mk, prod.exists],
     split,

src/ring_theory/noetherian.lean

@@ -242,7 +242,7 @@ begin
     { intros, ext, refl },
     { intros, ext, refl },
     { exact λ f i, f i.1 },
-    { intro, ext i, cases i, refl },
+    { intro, ext ⟨⟩, refl },
     { intro, ext i, refl } },
   intro s,
   induction s using finset.induction with a s has ih,
@@ -266,11 +266,11 @@ begin
   { exact λ f, (f ⟨a, finset.mem_insert_self _ _⟩, λ i, f ⟨i.1, finset.mem_insert_of_mem i.2⟩) },
   { intro f, apply prod.ext,
     { simp only [or.by_cases, dif_pos] },
-    { ext i, cases i with i his,
+    { ext ⟨i, his⟩,
       have : ¬i = a, { rintro rfl, exact has his },
       dsimp only [or.by_cases], change i ∈ s at his,
       rw [dif_neg this, dif_pos his] } },
-  { intro f, ext i, cases i with i hi,
+  { intro f, ext ⟨i, hi⟩,
     rcases finset.mem_insert.1 hi with rfl | h,
     { simp only [or.by_cases, dif_pos], refl },
     { have : ¬i = a, { rintro rfl, exact has h },

src/tactic/ext.lean

@@ -400,6 +400,8 @@ ext1 xs $> ()
 - `ext` applies as many extensionality lemmas as possible;
 - `ext ids`, with `ids` a list of identifiers, finds extentionality and applies them
   until it runs out of identifiers in `ids` to name the local constants.
+- `ext` can also be given an `rcases` pattern in place of an identifier.
+  This will destruct the introduced local constant.
 
 When trying to prove:
 
@@ -421,6 +423,26 @@ y : β
 
 by applying functional extensionality and set extensionality.
 
+When trying to prove:
+
+```lean
+α β γ : Type
+f g : α × β → γ
+⊢ f = g
+```
+
+applying `ext ⟨a, b⟩` yields:
+
+```lean
+α β γ : Type,
+f g : α × β → γ,
+a : α,
+b : β
+⊢ f (a, b) = g (a, b)
+```
+
+by applying functional extensionality and destructing the introduced pair.
+
 A maximum depth can be provided with `ext x y z : 3`.
 -/
 meta def interactive.ext : parse ext_parse → parse (tk ":" *> small_nat)? → tactic unit
@@ -429,15 +451,17 @@ meta def interactive.ext : parse ext_parse → parse (tk ":" *> small_nat)? →
  | xs n        := tactic.ext xs n
 
 /--
- * `ext1 id` selects and apply one extensionality lemma (with
-    attribute `ext`), using `id`, if provided, to name a
-    local constant introduced by the lemma. If `id` is omitted, the
-    local constant is named automatically, as per `intro`.
-
- * `ext` applies as many extensionality lemmas as possible;
- * `ext ids`, with `ids` a list of identifiers, finds extensionality lemmas
-    and applies them until it runs out of identifiers in `ids` to name
-    the local constants.
+* `ext1 id` selects and apply one extensionality lemma (with
+  attribute `ext`), using `id`, if provided, to name a
+  local constant introduced by the lemma. If `id` is omitted, the
+  local constant is named automatically, as per `intro`.
+
+* `ext` applies as many extensionality lemmas as possible;
+* `ext ids`, with `ids` a list of identifiers, finds extensionality lemmas
+  and applies them until it runs out of identifiers in `ids` to name
+  the local constants.
+* `ext` can also be given an `rcases` pattern in place of an identifier.
+  This will destruct the introduced local constant.
 
 When trying to prove:
 
@@ -456,9 +480,28 @@ x : α,
 y : β
 ⊢ y ∈ f x ↔ y ∈ g x
 ```
-
 by applying functional extensionality and set extensionality.
 
+When trying to prove:
+
+```lean
+α β γ : Type
+f g : α × β → γ
+⊢ f = g
+```
+
+applying `ext ⟨a, b⟩` yields:
+
+```lean
+α β γ : Type,
+f g : α × β → γ,
+a : α,
+b : β
+⊢ f (a, b) = g (a, b)
+```
+
+by applying functional extensionality and destructing the introduced pair.
+
 A maximum depth can be provided with `ext x y z : 3`.
 -/
 add_tactic_doc

src/topology/constructions.lean

@@ -747,8 +747,7 @@ begin
   choose t ht using this,
   apply is_open_induced_iff.mpr,
   refine ⟨⋃ i, sigma.mk i '' t i, is_open_Union (λ i, is_open_map_sigma_mk _ (ht i).1), _⟩,
-  ext p,
-  rcases p with ⟨i, x⟩,
+  ext ⟨i, x⟩,
   change (sigma.mk i (f i x) ∈ ⋃ (i : ι), sigma.mk i '' t i) ↔ x ∈ sigma.mk i ⁻¹' s,
   rw [←(ht i).2, mem_Union],
   split,