diff --git a/FLT/for_mathlib/Frobenius2.lean b/FLT/for_mathlib/Frobenius2.lean
index 9ef6627b..f30eda62 100644
--- a/FLT/for_mathlib/Frobenius2.lean
+++ b/FLT/for_mathlib/Frobenius2.lean
@@ -342,11 +342,11 @@ lemma Frob_Q_eq_pow_card (x : B) : Frob A Q isGalois P x - x^(Fintype.card (A⧸
     change (Frob A Q isGalois P) • x - _ ∈ _
     rw [← smul_sub]
     nth_rw 3 [ ← fact3]
-    suffices (x - y A Q ^ n) ∈ Q by
-      exact?
-    rw [smul_mem_smul]
-    simp
-    skip
+    -- suffices (x - y A Q ^ n) ∈ Q by
+    --   exact?
+    -- rw [smul_mem_smul]
+    -- simp
+    -- skip
     sorry
 
 /- maths proof: