Golfed proofs using grind

Author: YuvalFilmus

Mathlib/Data/Finset/Powerset.lean

@@ -75,39 +75,16 @@ theorem powerset_eq_singleton_empty : s.powerset = {∅} ↔ s = ∅ := by
 
 theorem image_injOn_powerset_of_injOn {β : Type*} [DecidableEq β] {f : α → β} (H : Set.InjOn f s) :
     Set.InjOn (fun (x : Finset α) => x.image f) s.powerset := by
-  intro x hx y hy h
-  rw [mem_coe, mem_powerset] at hx hy
-  dsimp at h
-  ext a
-  by_cases a ∈ s
-  case pos ha =>
-    have {z : Finset α} (hz : z ⊆ s) : a ∈ z ↔ f a ∈ z.image f := by
-      refine ⟨fun b => mem_image_of_mem f b, fun h => ?_⟩
-      obtain ⟨b, hb₁, hb₂⟩ := mem_image.mp h
-      suffices b = a by rwa [this] at hb₁
-      exact (H.eq_iff (hz hb₁) ha).mp hb₂
-    rw [this hx, this hy, h]
-  case neg ha => tauto
+  have {z a} (_ : z ⊆ s) (_ : a ∈ s) : a ∈ z ↔ f a ∈ z.image f := by grind [H.eq_iff]
+  exact fun _ _ _ _ _ => by grind
 
 theorem image_surjOn_powerset {β : Type*} [DecidableEq β] {f : α → β} :
-    Set.SurjOn (fun (x : Finset α) => x.image f) s.powerset (s.image f).powerset := by
-  intro t ht
-  rw [mem_coe, mem_powerset] at ht
-  simp_rw [Set.mem_image, mem_coe, mem_powerset]
-  use { x ∈ s | f x ∈ t}
-  grind
+    Set.SurjOn (fun (x : Finset α) => x.image f) s.powerset (s.image f).powerset :=
+  fun t ht => ⟨{ x ∈ s | f x ∈ t}, by grind⟩
 
 theorem powerset_image {β : Type*} [DecidableEq β] {f : α → β} :
-    (s.image f).powerset = s.powerset.image (fun x => x.image f) := by
-  ext a
-  rw [mem_powerset, mem_image]
-  refine ⟨fun ha => ?_, fun ha => ?_⟩
-  · use { x ∈ s | f x ∈ a }
-    grind
-  · obtain ⟨b, hb₁, hb₂⟩ := ha
-    rw [mem_powerset] at hb₁
-    rw [← hb₂]
-    exact image_subset_image hb₁
+    (s.image f).powerset = s.powerset.image (fun x => x.image f) :=
+  ext fun a => ⟨fun _ => mem_image.mpr ⟨{ x ∈ s | f x ∈ a}, by grind⟩, by grind⟩
 
 /-- **Number of Subsets of a Set** -/
 @[simp]