chore: prefer use to refine (#129)

A few proofs that become more readable when using `use` versus `refine`.
We should in general encourage this style, especially in proofs using
`grind`, `omega`, etc.

Author: chenson2018

Cslib/Foundations/Data/Nat/Segment.lean

@@ -211,7 +211,8 @@ theorem Nat.segment'_eq_segment (hm : StrictMono f) :
   · intro n ; simp only [mem_range, Finset.coe_filter, Finset.mem_range, mem_setOf_eq, mem_image]
     rintro ⟨h_n, i, rfl⟩
     have := StrictMono.monotone hm <| zero_le i
-    refine ⟨f i - f 0, ⟨by omega, i, rfl⟩, by omega⟩
+    use f i - f 0
+    grind
 
 /-- For a strictly monotonic function `f : ℕ → ℕ`, `segment f k = 0` for all `k ≤ f 0`. -/
 theorem Nat.segment_zero' (hm : StrictMono f) {k : ℕ} (h : k ≤ f 0) :

Cslib/Languages/CombinatoryLogic/Confluence.lean

@@ -182,8 +182,7 @@ theorem parallelReduction_diamond (a a₁ a₂ : SKI) (h₁ : a ⇒ₚ a₁) (h
     case red_S a c =>
       let ⟨a'', c', h⟩ := Sab_irreducible a c a' ha'
       rw [h.2.2]
-      use a'' ⬝ b' ⬝ (c' ⬝ b')
-      refine ⟨ParallelReduction.red_S a'' c' b', ?_⟩
+      use a'' ⬝ b' ⬝ (c' ⬝ b'), ParallelReduction.red_S a'' c' b'
       apply ParallelReduction.par
       · apply ParallelReduction.par
         · exact h.1

Cslib/Languages/CombinatoryLogic/Defs.lean

@@ -126,8 +126,10 @@ def CommonReduct : SKI → SKI → Prop := Relation.Join RedSKI.MRed
 lemma commonReduct_of_single {a b : SKI} (h : a ↠ b) : CommonReduct a b := ⟨b, h, by rfl⟩
 
 theorem symmetric_commonReduct : Symmetric CommonReduct := Relation.symmetric_join
-theorem reflexive_commonReduct : Reflexive CommonReduct := fun x => by
-  refine ⟨x,?_,?_⟩ <;> rfl
+
+theorem reflexive_commonReduct : Reflexive CommonReduct := by
+  intro x
+  use x
 
 theorem commonReduct_head {x x' : SKI} (y : SKI) : CommonReduct x x' → CommonReduct (x ⬝ y) (x' ⬝ y)
   | ⟨z, hz, hz'⟩ => ⟨z ⬝ y, MRed.head y hz, MRed.head y hz'⟩