Dist affine Combination le dist interleaved₂

theorem dist_affineCombination_le_dist_interleaved₂    (u₀ u₁ v₀ v₁ : Word A ι) (r : F) :    Δ₀( affineLineEvaluation (F := F) u₀ u₁ r, affineLineEvaluation (F := F) v₀ v₁ r) ≤      Δ₀(u₀ ⋈₂ u₁, v₀ ⋈₂ v₁) := by  -- The goal is to prove card(filter L) ≤ card(filter R)  -- We prove this by showing filter L ⊆ filter R  apply Finset.card_le_card  -- Use `monotone_filter_right` or prove subset directly  intro j  -- Assume j is in the filter set on the LHS  simp only [Finset.mem_filter, Finset.mem_univ, true_and]  intro hj_row_diff  -- Goal: Show j is in the filter set on the RHS  unfold affineLineEvaluation at hj_row_diff  -- hj_row_diff : ((1 - r) • u₀ + r • u₁) j ≠ ((1 - r) • v₀ + r • v₁) j  -- ⊢ (u₀⋈₂u₁) j ≠ (v₀⋈₂v₁) j  -- We prove this by contradiction  by_contra h_cols_eq  -- h_cols_eq : (u₀ ⋈₂ u₁) j = (v₀ ⋈₂ v₁) j  -- `h_cols_eq` is a function equality. Apply it to row indices 0 and 1  have h_row0_eq : (u₀ ⋈₂ u₁) j = (v₀ ⋈₂ v₁) j := by exact h_cols_eq  simp only [Pi.add_apply, Pi.smul_apply, ne_eq] at hj_row_diff  have h_row0_eq : (u₀ ⋈₂ u₁) j 0 = (v₀ ⋈₂ v₁) j 0 := congrFun h_cols_eq 0  have h_row1_eq : (u₀ ⋈₂ u₁) j 1 = (v₀ ⋈₂ v₁) j 1 := congrFun h_cols_eq 1  have h_row0 : u₀ j = v₀ j := by exact h_row0_eq  have h_row1 : u₁ j = v₁ j := by exact h_row1_eq  rw [h_row0, h_row1] at hj_row_diff  exact hj_row_diff rfl