Streamline proofs

Author: GBathie

BoltLean/Boolean/Domination.lean

@@ -8,35 +8,34 @@ namespace BoolFormula
       split
       . next heq =>
           rw [←heq] at h
-          simp [dominates] at h
-          apply h v
+          apply h
+          simp
       . next hne => simp
 
 
   theorem var_replace_accepts (f1 f2: BoolFormula n_var) (i: Fin n_var) (neg: Bool):
     f1.dominates f2 -> ∀ (v: Valuation n_var), (Var i neg).accepts v -> ((Var i neg).replace f2 f1).accepts v := by
-      intro h v
+      intro h v hv
       simp [replace]
       split
       . next heq =>
           rw [←heq] at h
-          simp [dominates] at h
-          apply h v
-      . next hne => simp
+          apply h
+          exact hv
+      . next hne => assumption
 
   theorem domin_replace (f1 f2: BoolFormula n_var):
     f1.dominates f2 →
       ∀ (f: BoolFormula n_var), (f.replace f2 f1).dominates f := by
       intro hd f v ha
       induction f with
-      | True => apply true_replace_accepts; assumption
+      | True => exact true_replace_accepts f1 f2 hd v
       | False => contradiction
       | Var i neg =>
         apply var_replace_accepts
           <;> assumption
       | And g1 g2 ih1 ih2 =>
-        unfold replace
-        simp
+        simp [replace]
         split
         . next heq =>
           rw [←heq] at hd
@@ -49,8 +48,7 @@ namespace BoolFormula
           . exact ih1 ha.left
           . exact ih2 ha.right
       | Or g1 g2 ih1 ih2 =>
-        unfold replace
-        simp
+        simp [replace]
         split
         . next heq =>
           rw [←heq] at hd