Card agreeing cells in D le

lemma card_agreeing_cells_in_D_le    {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_in_D MC U₀ U₁ V₀ V₁ e D).card ≤ D.card := by  classical  -- Let R_ss_in_D be the set of agreeing cells (r, j) with j ∈ D  let R_ss_in_D := R_star_star_filter_columns_in_D MC U₀ U₁ V₀ V₁ e D  -- 1. The card of a set is bounded by the sum of the cardinalities of its fibers  --    (We are "slicing" the set by its second component, the column index j)  have h_card_eq_sum_fibers : R_ss_in_D.card    = ∑ j ∈ D, ((R_ss_in_D.filter (fun p => p.2 = j)).card) := by      apply Finset.card_eq_sum_card_fiberwise (f := Prod.snd) (t := D)      -- We must show that every element in R_ss_in_D maps to an element in D      -- Goal: `Set.MapsTo (Prod.snd) R_ss_in_D D`, this means: `∀ p ∈ R_ss_in_D, p.2 ∈ D`      intro p hp_in_Rss      -- This is true by the very definition of R_ss_in_D!      unfold R_ss_in_D R_star_star_filter_columns_in_D at hp_in_Rss      simp only [coe_filter, Set.mem_setOf_eq] at hp_in_Rss      -- hp_in_Rss is `p ∈ R_star_star ∧ p.2 ∈ D`      exact hp_in_Rss.2  -- 2. We prove that each fiber (for a fixed j) has cardinality at most 1  have h_fibers_le_one_sum :    ∑ j ∈ D, ((R_ss_in_D.filter (fun p => p.2 = j)).card) ≤ ∑ j ∈ D, 1 := by    apply Finset.sum_le_sum    intro j hj_in_D -- For any column j that is in the disagreement set D    -- Goal for this term: (R_ss_in_D.filter (fun p => p.2 = j)).card ≤ 1    apply Finset.card_le_one_iff.mpr    -- Goal: ∀ p1 p2, p1 ∈ ... → p2 ∈ ... → p1 = p2    -- We MUST introduce two elements (p1, p2) and their two proofs (hp1, hp2)    intro p1 p2 hp1 hp2    rcases p1 with ⟨r₁, j₁⟩    rcases p2 with ⟨r₂, j₂⟩    -- ⊢ (r₁, j₁) = (r₂, j₂)    apply Prod.ext    · -- Goal 1: Prove r₁ = r₂: We need to extract the agreement properties from the hypotheses      have h1_in_Rss : (r₁, j₁) ∈ R_ss_in_D := (Finset.mem_filter.mp hp1).1      have h1_j_eq : j₁ = j := (Finset.mem_filter.mp hp1).2      have h2_in_Rss : (r₂, j₂) ∈ R_ss_in_D := (Finset.mem_filter.mp hp2).1      have h2_j_eq : j₂ = j := (Finset.mem_filter.mp hp2).2      -- Get the agreement properties from R_ss_in_D      have h1_agree : affineLineEvaluation U₀ U₁ r₁ j = affineLineEvaluation (↑V₀) (↑V₁) r₁ j := by        -- Unfold R_ss_in_D and R_star_star to find the agreement        unfold R_ss_in_D R_star_star_filter_columns_in_D at h1_in_Rss        simp only [R_star_star, mem_filter, mem_product, mem_univ, and_true] at h1_in_Rss        rw [← h1_j_eq] -- Use j₁ = j        exact h1_in_Rss.1.2      have h2_agree : affineLineEvaluation U₀ U₁ r₂ j = affineLineEvaluation (↑V₀) (↑V₁) r₂ j := by        unfold R_ss_in_D R_star_star_filter_columns_in_D at h2_in_Rss        simp only [R_star_star, mem_filter, mem_product, mem_univ, and_true] at h2_in_Rss        rw [← h2_j_eq] -- Use j₂ = j        exact h2_in_Rss.1.2 -- This is the `Uᵣ j = Vᵣ j` part      -- linear algebra argument      let W₀ := U₀ j - V₀.val j      let W₁ := U₁ j - V₁.val j      have h_eq_r1 : W₀ + r₁ • (W₁ - W₀) = 0 := by        unfold affineLineEvaluation at h1_agree        rw [← sub_eq_zero] at h1_agree        rw [← h1_agree]        unfold W₀ W₁        -- ⊢ U₀ j - ↑V₀ j + r₁ • (U₁ j - ↑V₁ j - (U₀ j - ↑V₀ j)) = ((1 - r₁) • U₀ + r₁ • U₁) j          -- - ((1 - r₁) • ↑V₀ + r₁ • ↑V₁) j        simp only [Pi.add_apply, Pi.smul_apply]        rw [sub_smul, sub_smul]; rw [smul_sub, smul_sub, smul_sub]        simp only [one_smul]        abel_nf      have h_eq_r2 : W₀ + r₂ • (W₁ - W₀) = 0 := by        unfold affineLineEvaluation at h2_agree        rw [← sub_eq_zero] at h2_agree        rw [← h2_agree]        unfold W₀ W₁        simp only [Pi.add_apply, Pi.smul_apply]        rw [sub_smul, sub_smul]; rw [smul_sub, smul_sub, smul_sub]        simp only [one_smul]        abel_nf      have h_j_in_D : W₀ ≠ 0 ∨ W₁ ≠ 0 := by        simp only [h_D_def, disagreementSet, ne_eq, mem_filter, mem_univ, true_and] at hj_in_D        by_cases h₀_ne: ¬U₀ j = V₀.val j        · left          dsimp only [W₀]          exact sub_ne_zero_of_ne h₀_ne        · simp only [h₀_ne, false_or] at hj_in_D          right          dsimp only [W₁]          exact sub_ne_zero_of_ne hj_in_D      by_cases h_diff_eq_zero : W₁ - W₀ = 0      · -- Case 1: W₁ - W₀ = 0        have h_W₀_zero : W₀ = 0 := by rwa [h_diff_eq_zero, smul_zero, add_zero] at h_eq_r1        have h_W₁_zero : W₁ = 0 := by          rw [←h_diff_eq_zero, h_W₀_zero];          exact Eq.symm (sub_zero W₁)        by_cases h_W₀_ne_zero : W₀ ≠ 0        · exact False.elim (h_W₀_ne_zero h_W₀_zero)        · have h_W₁_ne_0 : W₁ ≠ 0 := by            exact h_j_in_D.resolve_left h_W₀_ne_zero          exact False.elim (h_W₀_ne_zero fun a ↦ h_W₁_ne_0 h_W₁_zero)      · -- Case 2: W₁ - W₀ ≠ 0 (this is `h_diff_eq_zero : ¬W₁ - W₀ = 0`)        -- 2 hypotheses: h_eq_r1 : W₀ + r₁ • (W₁ - W₀) = 0, h_eq_r2 : W₀ + r₂ • (W₁ - W₀) = 0        have h_eq_both : W₀ + r₁ • (W₁ - W₀) = W₀ + r₂ • (W₁ - W₀) := by          rw [h_eq_r1, h_eq_r2]        have h_smul_eq : r₁ • (W₁ - W₀) = r₂ • (W₁ - W₀) :=          (add_right_inj W₀).mp h_eq_both        have h_sub_smul_eq_zero : (r₁ - r₂) • (W₁ - W₀) = 0 := by          rw [sub_smul, sub_eq_zero]          exact h_smul_eq        rw [smul_eq_zero] at h_sub_smul_eq_zero        have h_r_sub_eq_zero : r₁ - r₂ = 0 := by          exact h_sub_smul_eq_zero.resolve_right h_diff_eq_zero        exact sub_eq_zero.mp h_r_sub_eq_zero    · -- Goal 2: Prove j₁ = j₂: This follows directly from the fiber proofs      have h1_j_eq : j₁ = j := (Finset.mem_filter.mp hp1).2      have h2_j_eq : j₂ = j := (Finset.mem_filter.mp hp2).2      rw [h1_j_eq, h2_j_eq]  -- 3. Chain the inequalities: R_ss_in_D.card ≤ (∑ j in D, 1) ≤ D.card  simp only [sum_const, smul_eq_mul, mul_one] at h_fibers_le_one_sum  exact le_trans (Nat.le_of_eq h_card_eq_sum_fibers) h_fibers_le_one_sum