View indist of tail Sampler

theorem view_indist_of_tailSampler (params : Params F Party)    (sampler : TailSampler params) :    ∀ (s : Finset Party), ¬ authorized params s → ∀ secret₀ secret₁ : F,      viewDistOf sampler.gen (share params) s secret₀ =        viewDistOf sampler.gen (share params) s secret₁ := by  intro s hs secret₀ secret₁  have hcard : s.card ≤ params.threshold := by    have hs' : ¬ params.threshold + 1 ≤ s.card := by      simpa [authorized] using hs    exact Nat.lt_succ_iff.mp (Nat.not_le.mp hs')  unfold viewDistOf  calc    PMF.map (fun coeffs : Randomness params =>        (fun i : s => share params coeffs secret₀ i : s → F)) sampler.gen =      PMF.map        (fun coeffs : Randomness params => (fun i : s =>          share params            (coeffs + privacyCorrection (F := F) params s hcard secret₀ secret₁)            secret₁ i : s → F)) sampler.gen := by        congr 1        funext coeffs        exact view_eq_view_add_privacyCorrection          (F := F) params s hcard secret₀ secret₁ coeffs    _ = PMF.map (fun coeffs : Randomness params =>          (fun i : s => share params coeffs secret₁ i : s → F))        (PMF.map          (fun coeffs => coeffs + privacyCorrection (F := F) params s hcard secret₀ secret₁)          sampler.gen) := by          rw [PMF.map_comp]          rfl    _ = PMF.map (fun coeffs : Randomness params =>          (fun i : s => share params coeffs secret₁ i : s → F)) sampler.gen := by          rw [sampler.map_add_eq_self]