chore: drop use of trivial in use (#1153)

After filling an existential, `use` will resolve the remaining goals if they are "easy".  Before this PR this was done by trying `trivial`.  I have downgraded to `with_reducible rfl`.  This means `use` will no longer solve goals which are
- definitional equalities which require the unfolding of non-reducible definitions
- tactics other than `rfl` which are called by `trivial` (notably `decide`, which can get slow)

Note that this brings `use` closer to the mathlib3 version:  there it tried the `trivial'` tactic, which again only looked at definitional equality up to reducible definitions, and whose kitchen-sink did not include `decide`. 

See discussion:
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/use

Mathlib/Data/List/Basic.lean

@@ -924,6 +924,7 @@ theorem mem_getLast?_eq_getLast : ∀ {l : List α} {x : α}, x ∈ l.getLast? 
     rw [getLast?_cons_cons] at hx
     rcases mem_getLast?_eq_getLast hx with ⟨_, h₂⟩
     use cons_ne_nil _ _
+    assumption
 #align list.mem_last'_eq_last List.mem_getLast?_eq_getLast
 
 theorem getLast?_eq_getLast_of_ne_nil : ∀ {l : List α} (h : l ≠ []), l.getLast? = some (l.getLast h)

Mathlib/Data/Set/Image.lean

@@ -979,14 +979,15 @@ theorem range_subtype_map {p : α → Prop} {q : β → Prop} (f : α → β) (h
   ext ⟨x, hx⟩
   rw [mem_preimage, mem_range, mem_image, Subtype.exists, Subtype.coe_mk]
   apply Iff.intro
-  { rintro ⟨a, b, hab⟩
+  . rintro ⟨a, b, hab⟩
     rw [Subtype.map, Subtype.mk.injEq] at hab
-    use a }
-  { rintro ⟨a, b, hab⟩
+    use a
+    trivial
+  . rintro ⟨a, b, hab⟩
     use a
     use b
     rw [Subtype.map, Subtype.mk.injEq]
-    exact hab }
+    exact hab
   -- Porting note: `simp_rw` fails here
   -- simp_rw [mem_preimage, mem_range, mem_image, Subtype.exists, Subtype.map, Subtype.coe_mk,
   --   mem_set_of, exists_prop]
@@ -1099,14 +1100,15 @@ theorem range_inclusion (h : s ⊆ t) : range (inclusion h) = { x : t | (x : α)
   ext ⟨x, hx⟩
   -- Porting note: `simp [inclusion]` doesn't solve goal
   apply Iff.intro
-  { rw [mem_range]
+  . rw [mem_range]
     rintro ⟨a, ha⟩
     rw [inclusion, Subtype.mk.injEq] at ha
     rw [mem_setOf, Subtype.coe_mk, ← ha]
-    exact Subtype.coe_prop _ }
-  { rw [mem_setOf, Subtype.coe_mk, mem_range]
+    exact Subtype.coe_prop _
+  . rw [mem_setOf, Subtype.coe_mk, mem_range]
     intro hx'
-    use ⟨x, hx'⟩ }
+    use ⟨x, hx'⟩
+    trivial
   -- simp_rw [inclusion, mem_range, Subtype.mk_eq_mk]
   -- rw [SetCoe.exists, Subtype.coe_mk, exists_prop, exists_eq_right, mem_set_of, Subtype.coe_mk]
 #align set.range_inclusion Set.range_inclusion

Mathlib/Tactic/Use.lean

@@ -19,7 +19,7 @@ namespace Mathlib.Tactic
 
 /--
 `use e₁, e₂, ⋯` applies the tactic `refine ⟨e₁, e₂, ⋯, ?_⟩` and then tries
-to close the goal with `trivial` (which may or may not close it). It's
+to close the goal with `with_reducible rfl` (which may or may not close it). It's
 useful, for example, to advance on existential goals, for which terms as
 well as proofs of some claims about them are expected.
 
@@ -35,4 +35,4 @@ example : ∃ x : String × String, x.1 = x.2 := by use ("forty-two", "forty-two
 -/
 -- TODO extend examples in doc-string once mathlib3 parity is achieved.
 macro "use " es:term,+ : tactic =>
-  `(tactic|(refine ⟨$es,*, ?_⟩; try trivial))
+  `(tactic|(refine ⟨$es,*, ?_⟩; try with_reducible rfl))

test/Use.lean

@@ -18,17 +18,19 @@ example : ∃ x : Nat, x = x := by
   exact 42
   rfl
 
-example (α : Type) : ∃ S : List α, S = S :=
-by use ∅
+example (α : Type) : ∃ S : List α, S = S := by use ∅
 
-example : ∃ x : Int, x = x :=
-by use 42
+example : ∃ x : Int, x = x := by use 42
 
-example : ∃ a b c : Int, a + b + c = 6 :=
-by use 1, 2, 3
+example : ∃ a b c : Int, a + b + c = 6 := by
+  use 1, 2, 3
+  rfl
+
+example : ∃ p : Int × Int, p.1 = 1 := by use ⟨1, 42⟩
 
-example : ∃ p : Int × Int, p.1 = 1 :=
-by use ⟨1, 42⟩
+example : ∃ n : Int, n * 3 = 3 * 2 := by
+  use 2
+  rfl
 
 -- FIXME Failing tests ported from mathlib3