feat(tactics/ext): use applyc _ {new_goals := new_goals.all}

This causes goals to appear in the same order they appear as hypotheses of the
`@[extensionality]` lemma, rather than being reordered to put dependent
goals first.

This doesn't appear to affect any uses of `ext` in mathlib,
but is occasionally helpful in the development of category theory.

(Indeed, I have been running into tactic mode proofs that fail to
typecheck, when using ext, and this avoids the problem)

tactic/ext.lean

@@ -162,9 +162,9 @@ meta def ext1 (xs : ext_patt) : tactic ext_patt :=
 do subject ← target >>= get_ext_subject,
    m ← extensional_attribute.get_cache,
    do { rule ← m.find subject,
-        applyc rule } <|>
+        applyc rule {new_goals := new_goals.all} } <|>
      do { ls ← attribute.get_instances `extensionality,
-          ls.any_of applyc } <|>
+          ls.any_of (λ n, applyc n {new_goals := new_goals.all}) } <|>
      fail format!"no applicable extensionality rule found for {subject}",
    try_intros xs
 

tests/tactics.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Scott Morrison
 -/
-import tactic data.set.lattice data.prod
+import tactic data.set.lattice data.prod data.vector
        tactic.rewrite data.stream.basic
 
 section solve_by_elim
@@ -478,6 +478,31 @@ begin
   trivial
 end
 
+structure dependent_fields :=
+(a : bool)
+(v : if a then ℕ else ℤ)
+
+@[extensionality] lemma df.ext (s t : dependent_fields) (h : s.a = t.a)
+ (w : (@eq.rec _ s.a (λ b, if b then ℕ else ℤ) s.v t.a h) = t.v): s = t :=
+begin
+  cases s, cases t,
+  dsimp at *,
+  congr,
+  exact h,
+  subst h,
+  simp,
+  simp at w,
+  exact w,
+end
+
+example (s : dependent_fields) : s = s :=
+begin
+  ext,
+  guard_target s.a = s.a,
+  refl,
+  refl,
+end
+
 end ext
 
 section apply_rules