From 3fda1b61d5e17f69a7a7bed1e5022a4529a4975e Mon Sep 17 00:00:00 2001
From: zhangtengyu0523 <zhangtengyu0523@ruc.edu.cn>
Date: Thu, 27 Feb 2025 20:05:34 +0800
Subject: [PATCH] 2025/2/27 test4

---
 Game/Levels/World_two/L08_exercise.lean | 33 ++++---------------------
 Game/Levels/World_two/L09_subgroup.lean | 13 ++++++++++
 2 files changed, 18 insertions(+), 28 deletions(-)
 create mode 100644 Game/Levels/World_two/L09_subgroup.lean

diff --git a/Game/Levels/World_two/L08_exercise.lean b/Game/Levels/World_two/L08_exercise.lean
index 435d528..003763a 100644
--- a/Game/Levels/World_two/L08_exercise.lean
+++ b/Game/Levels/World_two/L08_exercise.lean
@@ -4,36 +4,13 @@ World "World_Two"
 Level 8
 Title "Exercise"
 
-Statement {α : Type*} (s t r : Set α): (s ∪ t) ∪ r = s ∪ (t ∪ r) := by
+Statement {α : Type*} (s t : Set α) : s ⊆ t → s ∩ t = s := by
+  intro h
   ext x
-  rw [Set.mem_union]
+  rw [Set.mem_inter_iff]
   constructor
-  · rintro (h | h)
-    · rw [Set.mem_union] at *
-      rcases h with h | h
-      · left
-        exact h
-      · right
-        rw [Set.mem_union]
-        left
-        exact h
-    · rw [Set.mem_union, Set.mem_union]
-      right
-      right
-      exact h
-  · rintro (h | h)
-    · left
-      rw [Set.mem_union]
-      left
-      exact h
-    · rw [Set.mem_union] at *
-      rcases h with h | h
-      left
-      right
-      exact h
-      right
-      exact h
+  exact fun ha ↦ ha.1
+  exact fun ha ↦ ⟨ha, h ha⟩
 
 
 Conclusion "Level Completed!"
-NewTactic left right
diff --git a/Game/Levels/World_two/L09_subgroup.lean b/Game/Levels/World_two/L09_subgroup.lean
new file mode 100644
index 0000000..54ebcde
--- /dev/null
+++ b/Game/Levels/World_two/L09_subgroup.lean
@@ -0,0 +1,13 @@
+import Game.Metadata
+
+World "World_Two"
+Level 9
+Title "Exercise"
+
+Statement {G : Type*} [Group G] (H : Subgroup G) : H.carrier ⊆ ⊤ := by
+  intro x _
+  exact trivial
+
+
+Conclusion "Level Completed!"
+NewTheorem trivial