feat(logic/basic): add eq_iff_true_of_subsingleton (#3308)

I'm surprised we didn't have this already.
```lean
example (x y : unit) : x = y := by simp
```


Co-authored-by: Johan Commelin <johan@commelin.net>

Author: gebner

src/linear_algebra/basis.lean

@@ -1286,9 +1286,7 @@ begin
   apply (is_basis_fun₀ R η).comp (λ i, ⟨i, punit.star⟩),
   apply bijective_iff_has_inverse.2,
   use sigma.fst,
-  suffices : ∀ (a : η) (b : unit), punit.star = b,
-  { simpa [function.left_inverse, function.right_inverse] },
-  exact λ _, punit_eq _
+  simp [function.left_inverse, function.right_inverse]
 end
 
 end

src/logic/basic.lean

@@ -50,6 +50,10 @@ instance psum.inhabited_right {α β} [inhabited β] : inhabited (psum α β) :=
   {α} [subsingleton α] : decidable_eq α
 | a b := is_true (subsingleton.elim a b)
 
+@[simp] lemma eq_iff_true_of_subsingleton [subsingleton α] (x y : α) :
+  x = y ↔ true :=
+by cc
+
 /-- Add an instance to "undo" coercion transitivity into a chain of coercions, because
    most simp lemmas are stated with respect to simple coercions and will not match when
    part of a chain. -/

src/tactic/fin_cases.lean

@@ -46,8 +46,9 @@ meta def fin_cases_at_aux : Π (with_list : list expr) (e : expr), tactic unit
                         (to_rhs >> conv.interactive.change (to_pexpr h))
         -- Otherwise, call `norm_num`. We let `norm_num` unfold `max` and `min`
         -- because it's helpful for the `interval_cases` tactic.
-        | _ := try $ tactic.interactive.norm_num
-                 [simp_arg_type.expr ``(max), simp_arg_type.expr ``(min)] (loc.ns [some sn])
+        | _ := try $ tactic.interactive.conv (some sn) none $
+               to_rhs >> conv.interactive.norm_num
+                 [simp_arg_type.expr ``(max), simp_arg_type.expr ``(min)]
         end,
         s ← get_local sn,
         try `[subst %%s],

src/tactic/norm_num.lean

@@ -1442,6 +1442,6 @@ where `A` and `B` are numerical expressions.
 It also has a relatively simple primality prover. -/
 meta def norm_num (hs : parse simp_arg_list) : conv unit :=
 repeat1 $ orelse' norm_num1 $
-simp_core {} norm_num1 ff hs [] (loc.ns [none])
+conv.interactive.simp ff hs [] { discharger := tactic.interactive.norm_num1 (loc.ns [none]) }
 
 end conv.interactive

test/fin_cases.lean

@@ -15,6 +15,15 @@ begin
   simp, assumption,
 end
 
+example (f : ℕ → Prop) (p : fin 0) : f p.val :=
+by fin_cases *
+
+example (f : ℕ → Prop) (p : fin 1) (h : f 0) : f p.val :=
+begin
+  fin_cases p,
+  assumption
+end
+
 example (x2 : fin 2) (x3 : fin 3) (n : nat) (y : fin n) : x2.val * x3.val = x3.val * x2.val :=
 begin
   fin_cases x2;

test/tidy.lean

@@ -11,13 +11,6 @@ namespace tidy.test
 
 meta def interactive_simp := `[simp]
 
-def tidy_test_0 : ∀ x : unit, x = unit.star :=
-begin
-  success_if_fail { chain [ interactive_simp ] },
-  intro1,
-  induction x,
-  refl
-end
 def tidy_test_1 (a : string) : ∀ x : unit, x = unit.star :=
 begin
   tidy -- intros x, exact dec_trivial