{Step, LeadsTo}.mk grind lemmas

Author: chenson2018

Cslib/Computability/Automata/NABuchiInter.lean

@@ -66,7 +66,6 @@ lemma inter_freq_acc_freq_acc {xs : ωSequence Symbol} {ss : ωSequence ((Π i,
   apply frequently_leadsTo_frequently h_inf
   apply leadsTo_trans (q := {s | s.snd = !i})
   · apply step_leadsTo
-    intro k
     grind
   · apply until_frequently_not_leadsTo
     · grind

Cslib/Foundations/Data/OmegaSequence/Temporal.lean

@@ -23,12 +23,22 @@ in `xs`. -/
 def Step (xs : ωSequence α) (p q : Set α) : Prop :=
   ∀ k, xs k ∈ p → xs (k + 1) ∈ q
 
+theorem Step.mk {xs : ωSequence α} (h : ∀ k, xs k ∈ p → xs (k + 1) ∈ q) : Step xs p q :=
+  h
+
+attribute [scoped grind <=] Step.mk
+
 /-- "`p` leads to `q`" means that whenever `p` holds at a position in `xs`, `q` holds at the same
 or a later position in `xs`. -/
 @[scoped grind =]
 def LeadsTo (xs : ωSequence α) (p q : Set α) : Prop :=
   ∀ k, xs k ∈ p → ∃ k', k ≤ k' ∧ xs k' ∈ q
 
+theorem LeadsTo.mk {xs : ωSequence α} (h : ∀ k, xs k ∈ p → ∃ k', k ≤ k' ∧ xs k' ∈ q) :
+    LeadsTo xs p q := h
+
+attribute [scoped grind <=] LeadsTo.mk
+
 variable {xs : ωSequence α}
 
 /-- `Step` implies `LeadsTo`. -/