From 121b18f40af90c0b798567e57499219ee5cd7f78 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Wed, 21 Sep 2022 23:36:09 -0400
Subject: [PATCH] chore: add test

---
 tests/lean/run/generalize.lean | 53 +++++++++++++++-------------------
 1 file changed, 24 insertions(+), 29 deletions(-)

diff --git a/tests/lean/run/generalize.lean b/tests/lean/run/generalize.lean
index 6765a5d24e..e6a89d1293 100644
--- a/tests/lean/run/generalize.lean
+++ b/tests/lean/run/generalize.lean
@@ -1,35 +1,30 @@
 
 
-theorem tst0 (x : Nat) : x + 0 = x + 0 :=
-by {
-  generalize x + 0 = y;
-  exact (Eq.refl y)
-}
+example (x : Nat) : x + 0 = x + 0 := by
+  generalize x + 0 = y
+  rfl
 
-theorem tst1 (x : Nat) : x + 0 = x + 0 :=
-by {
-  generalize h : x + 0 = y;
-  exact (Eq.refl y)
-}
+example (x : Nat) : x + 0 = x + 0 := by
+  generalize h : x + 0 = y
+  rfl
 
-theorem tst2 (x y w : Nat) (h : y = w) : (x + x) + w  = (x + x) + y :=
-by {
-  generalize h' : x + x = z;
-  subst y;
-  exact Eq.refl $ z + w
-}
+example (x y w : Nat) (h : y = w) : (x + x) + w = (x + x) + y := by
+  generalize h' : x + x = z
+  subst y
+  rfl
 
-theorem tst3 (x y w : Nat) (h : x + x = y) : (x + x) + (x+x)  = (x + x) + y :=
-by {
-  generalize h' : x + x = z;
-  subst z;
-  subst y;
-  exact rfl
-}
+example (x y w : Nat) (h : x + x = y) : (x + x) + (x+x) = (x + x) + y := by
+  generalize h' : x + x = z
+  subst z
+  subst y
+  rfl
 
-theorem tst4 (x y w : Nat) (h : y = w) : (x + x) + w  = (x + x) + y :=
-by {
-  generalize h' : x + y = z; -- just add equality
-  subst h;
-  exact rfl
-}
+example (x y w : Nat) (h : y = w) : (x + x) + w = (x + x) + y := by
+  generalize h' : x + y = z -- just add equality
+  subst h
+  rfl
+
+example (x y w : Nat) (h : y = w) (H : (x + x) + w = (x + x) + y) :
+    (x + x) + w = (x + x) + y := by
+  generalize h' : x + x = z at H
+  exact H