chore([normed/charted]_space): Eliminate finish (#11126)

Removing uses of `finish`, as discussed in this Zulip thread (https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib.20sat.20solvers)




Co-authored-by: Patrick Massot <patrickmassot@free.fr>

src/analysis/normed_space/add_torsor_bases.lean

@@ -103,7 +103,7 @@ begin
   have hεyq : ∀ (y ∉ s), ε / 2 / dist y q ≠ 0,
   { simp only [ne.def, div_eq_zero_iff, or_false, dist_eq_zero, bit0_eq_zero, one_ne_zero,
       not_or_distrib, ne_of_gt hε, true_and, not_false_iff],
-    finish, },
+    exact λ y h1 h2, h1 (h2.symm ▸ hq) },
   classical,
   let w : t → units ℝ := λ p, if hp : (p : P) ∈ s then 1 else units.mk0 _ (hεyq ↑p hp),
   refine ⟨set.range (λ (p : t), line_map q p (w p : ℝ)), _, _, _, _⟩,

src/analysis/normed_space/lattice_ordered_group.lean

@@ -95,7 +95,7 @@ instance : normed_lattice_add_comm_group (order_dual α) :=
     intros a b h₂,
     apply dual_solid,
     rw ← order_dual.dual_le at h₂,
-    finish,
+    exact h₂,
   end, }
 
 lemma norm_abs_eq_norm (a : α) : ∥|a|∥ = ∥a∥ :=

src/geometry/manifold/charted_space.lean

@@ -216,7 +216,7 @@ def id_groupoid (H : Type u) [topological_space H] : structure_groupoid H :=
   end,
   symm' := λe he, begin
     cases (mem_union _ _ _).1 he with E E,
-    { finish },
+    { simp [mem_singleton_iff.mp E] },
     { right,
       simpa only [e.to_local_equiv.image_source_eq_target.symm] with mfld_simps using E},
   end,