No index for mem_subdomain_0_iff_mem

Co-authored-by: Frantisek Silvasi <silvasi.frantisek@gmail.com>

Author: ElijahVlasov

ArkLib/Data/CodingTheory/Basic/BlockRelDistance.lean

@@ -67,15 +67,13 @@ lemma disagreementSet_k_0 :
     constructor
     · aesop
         (add simp [disagreementSet])
-        (add safe (by rw [mem_subdomain_0_iff_mem]))
     · simp only [Finset.mem_filter, mem_toFinset_iff_mem, hmem,
         true_and, disagreementSet, forall_exists_index]
       intro j hj
       have : i = j := by
         have := CosetFftDomainClass.injective φ (a₁ := i)
         aesop
       aesop
-        (add safe (by rw [mem_subdomain_0_iff_mem]))
   · aesop
       (add simp [disagreementSet, blockIdx_k_0_of_ne_mem])
 

ArkLib/Data/CodingTheory/ProximityGap/Folding.lean

@@ -97,7 +97,6 @@ lemma foldWordAux_of_k_2 [NeZero n] {i : Fin (2 ^ (n - 1))} :
       aesop (add unsafe (by apply CosetFftDomain.injective (ω := domain)))
     ext u
     simp only [mem_filter, mem_univ, true_and, ←hpre, ←h, Nat.sub_zero, mem_preimage]
-    have := @mem_subdomain_0_iff_mem (ω := domain)
     aesop
   rw [blockIdx, h]
   have hcard : Finset.card {j, j'} = 2 := by
@@ -111,13 +110,11 @@ lemma foldWordAux_of_k_2 [NeZero n] {i : Fin (2 ^ (n - 1))} :
       (fun a _ ↦ domain a)
       (fun a ha ↦ by
         simp only [Nat.sub_zero, mem_block, pow_one]
-        rw [mem_subdomain_0_iff_mem]
         simpa using ha)
       (fun _ _ _ _ h ↦ CosetFftDomain.injective h)
       (fun b hb ↦ by
         obtain ⟨⟨j, hb⟩, hb'⟩ :
           b ∈ domain ∧ b ^ 2 = (CosetFftDomain.subdomain domain 1) i := by
-          have := @mem_subdomain_0_iff_mem (ω := domain)
           aesop
         exact ⟨j, by simp [hb, hb'], by simp [hb]⟩)
   apply Polynomial.eq_of_eval_eq_degree (n := 2) (s := {y.1, -y.1})

ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024-2026 ArkLib Contributors. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Julian Sutherland, Ilia Vlasov, Aristotle (Harmonic)
+Authors: František Silváši, Julian Sutherland, Ilia Vlasov, Aristotle (Harmonic)
 -/
 
 import Mathlib.Tactic.CancelDenoms.Core
@@ -141,19 +141,20 @@ lemma mem_subdomain_of_eq_vals
 lemma subdomain_generator_pow_generator (i : ℕ) :
   (subdomain ω i).cosetGenerator = ω 0 ^ 2 ^ i := rfl
 
+set_option warning.simp.varHead false in
 /-- Membership to the `0`th subdomain is
   the same as membership to the original coset FFT domain. -/
 @[simp]
 lemma mem_subdomain_0_iff_mem :
-  x ∈ subdomain ω 0 ↔ x ∈ ω := by
-  by_cases hn : n = 0
-    <;> aesop
-          (add simp
-            [subdomain,
-             CosetFftDomainClass.subdomain_embed,
-             mkSubgroupUnit,
-             mem_def,
-             CosetFftDomain.eval_coset_fft_domain_eq_eval_generator_mul_domain])
+  no_index (x ∈ subdomain ω 0) ↔ x ∈ ω := by
+  aesop
+    (add safe cases Nat)
+    (add simp
+      [subdomain,
+       CosetFftDomainClass.subdomain_embed,
+       mkSubgroupUnit,
+       mem_def,
+       CosetFftDomain.eval_coset_fft_domain_eq_eval_generator_mul_domain])
 
 /-- The `n`th subdomain consists exactly of the single element `ω 0 ^ 2 ^ n`. -/
 lemma mem_subdomain_n_iff_eq_pow_generator :
@@ -466,7 +467,7 @@ lemma card_block_of_mem_subdomain' [DecidableEq F] {k : ℕ}
   conv_rhs =>
     rw [←h]
   apply congrArg
-  aesop (add safe (by rw [mem_subdomain_0_iff_mem]))
+  aesop
 
 end CosetFftDomainClass