Prob coeff eq prob affine

theorem prob_coeff_eq_prob_affine {k : ℕ} [NeZero k]    (u0 : ι → F) (dirs : Fin k → ι → F)    (P : (ι → F) → Prop) :    Pr_{let r ← $ᵖ (Fin k → F)}[P (u0 + ∑ i : Fin k, r i • dirs i)] =    Pr_{let y ← $ᵖ (Affine.affineSubspaceAtOrigin (F := F) u0 dirs)}[P ↑y] := by  classical  -- Reduce both sides to cardinality fractions via prob_uniform_eq_card_filter_div_card.  rw [prob_uniform_eq_card_filter_div_card (fun r : Fin k → F => P (u0 + ∑ i, r i • dirs i))]  rw [prob_uniform_eq_card_filter_div_card    (fun y : ↥(Affine.affineSubspaceAtOrigin (F := F) u0 dirs) => P ↑y)]  -- Define the map g : (Fin k → F) → affineSubspaceAtOrigin  set A := Affine.affineSubspaceAtOrigin (F := F) u0 dirs with hA_def  have hg_mem : ∀ r : Fin k → F, u0 + ∑ i, r i • dirs i ∈ A := fun r =>    (Affine.mem_affineSubspaceFrom_iff (F := F) u0 dirs _).mpr ⟨r, rfl⟩  let g : (Fin k → F) → A := fun r => ⟨u0 + ∑ i, r i • dirs i, hg_mem r⟩  -- Key: g r₁ = g r₂ ↔ linear parts equal  have hg_eq : ∀ r₁ r₂ : Fin k → F,      g r₁ = g r₂ ↔ ∑ i, r₁ i • dirs i = ∑ i, r₂ i • dirs i := by    intro r₁ r₂    constructor    · intro h; exact add_left_cancel (congrArg Subtype.val h)    · intro h; exact Subtype.ext (congrArg (u0 + ·) h)  -- Auxiliary: linear part of (r - r₀)  have hlin_sub : ∀ (r r₀ : Fin k → F),      ∑ i, (r - r₀) i • dirs i = ∑ i, r i • dirs i - ∑ i, r₀ i • dirs i := by    intro r r₀; simp [Pi.sub_apply, sub_smul, Finset.sum_sub_distrib]  -- g is surjective  have hg_surj : Function.Surjective g := by    intro ⟨y, hy⟩    obtain ⟨β, rfl⟩ := (Affine.mem_affineSubspaceFrom_iff (F := F) u0 dirs y).mp hy    exact ⟨β, rfl⟩  -- Fiber cardinality is constant: use translation r ↦ r - r₀ to biject fibers.  set K := ((Finset.univ : Finset (Fin k → F)).filter (g · = g 0)).card with hK_def  have hg_fib : ∀ b ∈ Finset.univ.image g,      ((Finset.univ : Finset (Fin k → F)).filter (g · = b)).card = K := by    intro b hb    obtain ⟨r₀, _, hr₀⟩ := Finset.mem_image.mp hb    subst hr₀    -- Bijection: fiber(g r₀) ≃ fiber(g 0) via r ↦ r - r₀    apply Finset.card_equiv (Equiv.subRight r₀)    intro r    simp only [Finset.mem_filter, Finset.mem_univ, true_and, Equiv.subRight_apply]    constructor    · intro h      rw [hg_eq] at h ⊢; rw [hlin_sub]      simp only [Pi.zero_apply, zero_smul, Finset.sum_const_zero]      rw [h]; abel    · intro h      rw [hg_eq] at h ⊢; rw [hlin_sub] at h      simp only [Pi.zero_apply, zero_smul, Finset.sum_const_zero] at h      have := sub_eq_zero.mp h; rw [this]  -- K > 0 since fibers are nonempty  have hK_pos : 0 < K := by    rw [hK_def]    exact Finset.card_pos.mpr ⟨0, Finset.mem_filter.mpr ⟨Finset.mem_univ _, rfl⟩⟩  -- Step 1: |Fin k → F| = K * |A|  have hcard_eq : Fintype.card (Fin k → F) = K * Fintype.card A := by    rw [show Fintype.card (Fin k → F) = (Finset.univ : Finset (Fin k → F)).card from rfl]    rw [Finset.card_eq_sum_card_image g Finset.univ, Finset.sum_const_nat hg_fib,        Finset.image_univ_of_surjective hg_surj, Finset.card_univ, mul_comm]  -- Step 2: LHS filter = K * RHS filter  have hfilt_eq :      (Finset.filter (fun r : Fin k → F => P (u0 + ∑ i, r i • dirs i)) Finset.univ).card =      K * (Finset.filter (fun y : A => P ↑y) Finset.univ).card := by    -- Rewrite LHS as filter by g    have hfilt_rw :        (Finset.filter (fun r : Fin k → F => P (u0 + ∑ i, r i • dirs i)) Finset.univ) =        (Finset.filter (fun r => P (g r).val) Finset.univ) := by      ext r; simp only [Finset.mem_filter, Finset.mem_univ, true_and, g]    rw [hfilt_rw, Finset.card_eq_sum_card_image g _]    -- For each b in image of the filter, inner filter card = K    have hfib_K : ∀ b ∈ (Finset.filter (fun r => P (g r).val) Finset.univ).image g,        ((Finset.filter (fun r => P (g r).val) Finset.univ).filter (g · = b)).card = K := by      intro b hb      obtain ⟨r₀, hr₀_mem, hr₀_eq⟩ := Finset.mem_image.mp hb      have hPb : P (g r₀).val := (Finset.mem_filter.mp hr₀_mem).2      subst hr₀_eq      have : (Finset.filter (fun r => P (g r).val) Finset.univ).filter (g · = g r₀) =          Finset.univ.filter (g · = g r₀) := by        ext r; simp only [Finset.mem_filter, Finset.mem_univ, true_and]        constructor        · exact And.right        · intro hr; exact ⟨by rwa [show (g r).val = (g r₀).val from congrArg Subtype.val hr], hr⟩      rw [this]      exact hg_fib (g r₀) (Finset.mem_image_of_mem g (Finset.mem_univ r₀))    rw [Finset.sum_const_nat hfib_K]    -- Show: image of {r | P(g r)} under g = {y ∈ A | P ↑y}    have himg : (Finset.filter (fun r => P (g r).val) Finset.univ).image g =        Finset.filter (fun y : A => P ↑y) Finset.univ := by      ext ⟨y, hy⟩      simp only [Finset.mem_image, Finset.mem_filter, Finset.mem_univ, true_and]      constructor      · rintro ⟨r, hPr, hr_eq⟩        rwa [show (g r).val = y from congrArg Subtype.val hr_eq] at hPr      · intro hPy        obtain ⟨r, hr⟩ := hg_surj ⟨y, hy⟩        exact ⟨r, by rwa [show (g r).val = y from congrArg Subtype.val hr], hr⟩    rw [himg]; ring  -- Step 3: The probabilities are card fractions that simplify.  simp only [hfilt_eq, hcard_eq]  push_cast  exact ENNReal.mul_div_mul_left _ _ (by exact_mod_cast hK_pos.ne') (ENNReal.natCast_ne_top K)