From 7e1eb8fdfbffe0be1ccadd6d2946e7b4ac40aa6c Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Fri, 8 Sep 2023 18:50:44 -0600 Subject: [PATCH] Require simp to make progress. --- Bookshelf/Enderton/Set/Chapter_3.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean index b46a84a..d86e218 100644 --- a/Bookshelf/Enderton/Set/Chapter_3.lean +++ b/Bookshelf/Enderton/Set/Chapter_3.lean @@ -86,7 +86,6 @@ theorem theorem_3h_dom {F : Set.HRelation β γ} {G : Set.HRelation α β} simp only [Set.mem_setOf_eq] have ⟨z, hz⟩ := dom_exists ht refine ⟨dom_comp_imp_dom_self ht, ?_⟩ - simp only [Set.mem_setOf_eq] at hz have ⟨a, ha⟩ := hz unfold dom simp only [Set.mem_image, Prod.exists, exists_and_right, exists_eq_right] @@ -675,7 +674,6 @@ theorem exercise_3_5b {A : Set α} (B : Set β) apply And.intro · show ∀ t, t ∈ Set.prod A B → t ∈ ⋃₀ {Set.prod {x} B | x ∈ A} intro t h - simp only [Set.mem_setOf_eq] at h unfold Set.sUnion sSup Set.instSupSetSet simp only [Set.mem_setOf_eq, exists_exists_and_eq_and] unfold Set.prod at h