Card agreeing cells notin D

lemma card_agreeing_cells_notin_D {U₀ U₁ : InterleavedWord A (Fin m) ι} {V₀ V₁ : MC^⋈(Fin m)}    {e : ℕ} (D : Finset ι)    (h_D_def : D = disagreementSet U₀ U₁ V₀.val V₁.val) :    (R_star_star_filter_columns_not_in_D MC U₀ U₁ V₀ V₁ e D).card    = (R_star (A := A) (F := F) (ι := ι) (C := MC) (e := e) U₀ U₁).card      * (Fintype.card ι - D.card) := by  -- sorry  classical  let n := Fintype.card ι  let D_compl := Finset.univ \ D-- Define local abbreviations  let n := Fintype.card ι  let D_compl := Finset.univ \ D  let R_s := R_star (F := F) (A := A) (ι := ι) (C := MC) (e := e) U₀ U₁  let R_ss_not_D := R_star_star_filter_columns_not_in_D MC U₀ U₁ V₀ V₁ e D  -- 1. Prove that R_ss_not_D is equal to the product R_s ×ˢ D_compl  have h_set_eq : R_ss_not_D = R_s ×ˢ D_compl := by    -- We prove equality by showing element-wise equivalence    ext p    rcases p with ⟨r, j⟩    -- Unfold all definitions    simp only [R_star_star_filter_columns_not_in_D, R_star_star, mem_filter, mem_product, mem_univ,      and_true, R_ss_not_D, R_s, D_compl]    constructor    · rintro ⟨⟨hr, _⟩, hj⟩      exact ⟨hr, mem_sdiff.mpr ⟨mem_univ _, hj⟩⟩    · rintro ⟨hr, hj⟩      have hj' := (mem_sdiff.mp hj).2      refine ⟨⟨hr, ?_⟩, hj'⟩      have h_agree : U₀ j = V₀.val j ∧ U₁ j = V₁.val j := by        simp only [h_D_def, disagreementSet, mem_filter, mem_univ, true_and,          not_or, not_not] at hj'        exact hj'      unfold affineLineEvaluation      simp only [Pi.add_apply, Pi.smul_apply, h_agree.1, h_agree.2]  have h_set_card_eq : R_ss_not_D.card = R_s.card * D_compl.card := by    rw [h_set_eq]    simp only [card_product]  -- 2. Now calculate the cardinality using the set equality  grind only [usr le_card_sdiff, = card_sdiff_of_subset, = card_univ, = subset_iff, ← mem_univ]