diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean
index d680f60..9b325a9 100644
--- a/VerifiedCommitments/PedersenHiding.lean
+++ b/VerifiedCommitments/PedersenHiding.lean
@@ -2,6 +2,10 @@ import VerifiedCommitments.PedersenScheme
 import VerifiedCommitments.ZModUtil
 import Mathlib -- Would like to trim down this import but the Units.mk0 (a.val : ZMod q) a.2 line is a problem
 
+-- Temporary
+import VerifiedCommitments.«scratch-skip-bind»
+
+
 variable {G: Type} [Fintype G] [Group G]
 variable (q : ℕ) [Fact (Nat.Prime q)]
 variable (G_card_q : Fintype.card G = q)
@@ -9,6 +13,9 @@ variable (g : G) (g_gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g)
 include G_card_q
 include g_gen_G
 
+-- Temporary?
+variable [IsCyclic G] [DecidableEq G] (hq_prime : Nat.Prime q)
+
 lemma ordg_eq_q : orderOf g = q := by
   have h_card_zpow : Fintype.card (Subgroup.zpowers g) = orderOf g := Fintype.card_zpowers
     -- zpowers g has the same cardinality as G since g generates G
@@ -22,30 +29,34 @@ lemma ordg_eq_q : orderOf g = q := by
     exact Fintype.card_of_bijective this
   rw [← h_card_zpow, h_card_eq, G_card_q]
 
-lemma exp_bij (a : ZModMult q) (m : ZMod q) : Function.Bijective fun (r : ZMod q) => g^((m + (val a) * r : ZMod q).val : ℤ) := by
+
+lemma exp_bij' (a : ZModMult q) (m : ZMod q) : Function.Bijective fun (r : ZMod q) => g^((m + (val a) * r : ZMod q).val : ℤ) := by
   apply (Fintype.bijective_iff_surjective_and_card _).mpr
   simp [G_card_q]
-  intro y
-  obtain ⟨k, hk⟩ := g_gen_G y
+  intro c --So take any cc ∈ GG
+  obtain ⟨k, hk⟩ := g_gen_G c
   simp only at hk
   simp only
 
-  let k' : ZMod q := (k : ZMod q)
-  have hk' : g ^ (k'.val : ℤ) = y := by
+  let z : ZMod q := (k : ZMod q) -- Since g is a generator we have c = g^z for some z ∈ Zq
+  have hk' : g ^ (z.val : ℤ) = c := by
     rw [←hk]
     simp only [ZMod.natCast_val]
     rw [ZMod.coe_intCast]
     rw [← G_card_q]
     rw [@zpow_mod_card]
 
+  -- we need g^m+a^r = g^z
+  -- This is the case iff m + ar ≡ z (mod q)
+  -- This is the case iff t ≡ a^−1 * (z − m) (mod q)
   let a_unit := Units.mk0 (a.val : ZMod q) a.2
-  let r : ZMod q := (a_unit⁻¹ : ZMod q) * (k' - m)
-  have h_mod : (m + a_unit * r) = k' := by
+  let r : ZMod q := (a_unit⁻¹ : ZMod q) * (z - m)
+  have h_mod : (m + a_unit * r) = z := by
     subst r
-    rw [IsUnit.mul_inv_cancel_left (Exists.intro a_unit rfl) (k' - m)]
+    rw [IsUnit.mul_inv_cancel_left (Exists.intro a_unit rfl) (z - m)]
     simp
 
-  have h_pow : g^((m + a_unit * r).val : ℤ) = y := by
+  have h_pow : g^((m + a_unit * r).val : ℤ) = c := by
     rw [←hk']
     subst r
     rw [h_mod]
@@ -53,219 +64,184 @@ lemma exp_bij (a : ZModMult q) (m : ZMod q) : Function.Bijective fun (r : ZMod q
   rw [←ZMod.cast_eq_val] at h_pow -- Transfer ↑ and .val back to .cast
   exact Exists.intro (r) h_pow
 
-lemma pedersen_uniform_for_fixed_a
-   {a : ZMod q} (ha : a ≠ 0) (m : ZMod q) [DecidableEq G] (c : G) :
-   (Finset.card { t : ZMod q | g ^ ((m + a * t : ZMod q).val : ℤ) = c }) / (Finset.card ( (⊤ : Finset G) ) : ℚ)
-   = 1 / (Fintype.card G) := by
-    have h_bij := exp_bij q G_card_q g g_gen_G ⟨a, ha⟩ m
-    have h_card : Finset.card { t : ZMod q | g ^ ((m + a * t : ZMod q).val : ℤ) = c } = 1 := by
-      rw [Finset.card_eq_one]
-      obtain ⟨r, hr⟩ := h_bij.surjective c
-      use r
-      ext t
-      simp only [Finset.mem_singleton, Finset.mem_filter, Finset.mem_univ, true_and]
-      constructor
-      · intro ht
-        have : g ^ ((m + a * t : ZMod q).val : ℤ) = g ^ ((m + a * r : ZMod q).val : ℤ) := by
-          rw [ht, ← hr]
-          simp only [val]
-        exact h_bij.injective this
-      · intro ht
-        rw [ht, ← hr]
-        simp only [val]
-    rw [h_card]
-    exact rfl
-
-lemma pedersen_uniform_for_fixed_a'
-  {a : ZMod q} (ha : a ≠ 0) (m : ZMod q) [DecidableEq G] (c : G) :
-  Finset.card { r : ZMod q | c = g ^ m.val * (g ^ a.val) ^ r.val } = 1 := by
-    have h_ratio := pedersen_uniform_for_fixed_a q G_card_q g g_gen_G ha m c
-    have h_card : Finset.card { t : ZMod q | g ^ ((m + a * t : ZMod q).val : ℤ) = c } = 1 := by
-      have h_pos : (0 : ℚ) < Finset.card (⊤ : Finset G) := by simp; exact Fintype.card_pos
-      have h_eq : (Finset.card { t : ZMod q | g ^ ((m + a * t : ZMod q).val : ℤ) = c } : ℚ) =
-             (Finset.card (⊤ : Finset G) : ℚ) / (Fintype.card G : ℚ) := by
-        grind --only [= Finset.card_univ, usr Finset.card_filter_le, cases Or]
-      have h_top : Finset.card (⊤ : Finset G) = Fintype.card G := by rfl
-      have : (Finset.card { t : ZMod q | g ^ ((m + a * t : ZMod q).val : ℤ) = c } : ℚ) = (1 : ℚ) := by
-        grind
-      exact Nat.cast_injective (R := ℚ) this
-    convert h_card using 2
-    ext t
-    simp only [Finset.mem_filter, Finset.mem_univ, true_and]
-    have key : g ^ ((m + a * t).val : ℤ) = g ^ m.val * (g ^ a.val) ^ t.val := by
-      have : (g ^ m.val * (g ^ a.val) ^ t.val : G) = g ^ m.val * g ^ (a.val * t.val) := by
-        rw [← pow_mul]
-      rw [this]
-      rw [← pow_add]
-      have h_order : orderOf g = q := by
-        · expose_names; exact ordg_eq_q q G_card_q g g_gen_G
-      have h_val_eq : (m + a * t).val = (m.val + a.val * t.val) % q := by
-        have h_eq : (m + a * t : ZMod q) = ((m.val + a.val * t.val) : ℕ) := by
-          simp only [Nat.cast_add, ZMod.natCast_val, ZMod.cast_id', id_eq, Nat.cast_mul]
-        rw [h_eq, ZMod.val_natCast]
-      rw [h_val_eq]
-      show g ^ (((m.val + a.val * t.val) % q : ℕ) : ℤ) = g ^ (m.val + a.val * t.val : ℕ)
-      rw [← zpow_natCast]
-      have : (g : G) ^ (((m.val + a.val * t.val) % q : ℕ) : ℤ) = g ^ ((m.val + a.val * t.val : ℕ) : ℤ) := by
-        have : ((m.val + a.val * t.val : ℕ) : ℤ) % (orderOf g : ℤ) = ((m.val + a.val * t.val) % q : ℕ) := by
-          grind
-        rw [← this, zpow_mod_orderOf]
-      assumption
-    rw [key, eq_comm]
+
+-- Fintype instance for commit
+instance {C O : Type} [Fintype C] [Fintype O] : Fintype (commit C O) :=
+  Fintype.ofEquiv (C × O) {
+    toFun := fun ⟨c, o⟩ => ⟨c, o⟩
+    invFun := fun ⟨c, o⟩ => ⟨c, o⟩
+    left_inv := fun _ => rfl
+    right_inv := fun x => by cases x; rfl
+  }
+
+noncomputable def expEquiv (a : ZModMult q) (m : ZMod q) : ZMod q ≃ G :=
+Equiv.ofBijective (fun (r : ZMod q) => g^((m + (val a) * r : ZMod q).val : ℤ)) (exp_bij' q G_card_q g g_gen_G a m)
+
+
+#check expEquiv q G_card_q g g_gen_G
+
+lemma expEquiv_unfold (a : ZModMult q) (m r : ZMod q) :
+  expEquiv q G_card_q g g_gen_G a m r = g^m.val * (g^(val a).val)^r.val := by
+  unfold expEquiv
+  simp only [Equiv.ofBijective, Equiv.coe_fn_mk]
+
+  have h_pow : (g^(val a).val)^r.val = g^((val a).val * r.val) := (pow_mul g (val a).val r.val).symm
+  rw [h_pow]
+
+  simp only [← zpow_natCast]
+  rw [← zpow_add]
+
+  have hord : orderOf g = q := ordg_eq_q q G_card_q g g_gen_G
+  conv_lhs => rw [← zpow_mod_orderOf, hord]
+
+  suffices h : (((m + (val a) * r).val : ℤ) % ↑q) = ((m.val : ℤ) + ((val a).val * r.val : ℤ)) % ↑q by
+    conv_rhs => rw [← zpow_mod_orderOf, hord]
+    rw [h]
+    congr 1
+
+  conv_lhs => rw [ZMod.val_add, ZMod.val_mul]
+  norm_cast
+  rw [Nat.add_mod, Nat.mul_mod]
+  simp
+
+
+open Classical -- needed here or α must be DecidableEq
+/-! ### 2.  Mapping a uniform PMF through a bijection stays uniform -------------/
+-- Courtesy of formalmethods.io
+lemma map_uniformOfFintype_equiv
+    {α β : Type*} [Fintype α] [Fintype β] [DecidableEq β] [Nonempty α] [Nonempty β]
+    (e : α ≃ β) :
+    PMF.map e (PMF.uniformOfFintype α) = PMF.uniformOfFintype β := by
+  -- Prove equality of PMFs by showing they assign the same probability to each element
+  ext b
+  -- Goal: (PMF.map e (uniformOfFintype α)) b = (uniformOfFintype β) b
+
+  -- Step 1: Simplify the LHS using PMF.map_apply
+  rw [PMF.map_apply]
+  -- This gives us: ∑' (a : α), if b = e a then (uniformOfFintype α) a else 0
+
+  -- Step 2: Simplify the uniform distribution on α
+  simp only [PMF.uniformOfFintype_apply]
+  -- Goal: ∑' (a : α), if b = e a then (↑(card α))⁻¹ else 0 = (↑(card β))⁻¹
+
+  -- Step 3: The sum has exactly one non-zero term when a = e.symm b
+  -- We can rewrite this as a sum over the singleton {e.symm b}
+  have h_equiv : (∑' (a : α), if b = e a then (↑(Fintype.card α : ENNReal))⁻¹ else 0) =
+                 (∑' (a : α), if a = e.symm b then (↑(Fintype.card α))⁻¹ else 0) := by
+    congr 1
+    ext a
+    -- Show: (if b = e a then (↑(card α))⁻¹ else 0) = (if a = e.symm b then (↑(card α))⁻¹ else 0)
+    by_cases h : b = e a
+    · -- Case: b = e a
+      rw [if_pos h, if_pos]
+      -- Need to show a = e.symm b
+      rw [←Equiv.symm_apply_apply e a]
+      rw [h]
+    · -- Case: b ≠ e a
+      rw [if_neg h, if_neg]
+      -- Need to show a ≠ e.symm b
+      intro contra
+      subst contra
+      rw [Equiv.apply_symm_apply e] at h
+      apply h
+      rfl
+
+  -- Step 4: Apply the equivalence and simplify
+  rw [h_equiv]
+  rw [tsum_ite_eq]
+  -- Goal: (↑(card α))⁻¹ = (↑(card β))⁻¹
+
+  -- Step 5: Use the fact that equivalent finite types have the same cardinality
+  congr 1
+  rw [Fintype.card_congr e]
+
+lemma bind_eq_map
+    {α β : Type*} [Fintype α] [Fintype β] [DecidableEq β] [Nonempty α] [Nonempty β]
+    (e : α ≃ β) :
+    PMF.map e (PMF.uniformOfFintype α) = PMF.bind (PMF.uniformOfFintype α) (fun a => pure (e a)) := by
+    rfl
+
+lemma bind_eq_map' : ∀ (fixed_a : ZModMult q) (fixed_m : ZMod q),
+  PMF.map (expEquiv q G_card_q g g_gen_G fixed_a fixed_m) (PMF.uniformOfFintype (ZMod q)) =
+  PMF.bind (PMF.uniformOfFintype (ZMod q)) (fun a => PMF.pure (expEquiv q G_card_q g g_gen_G fixed_a fixed_m a))
+  := by
+  intros
+  exact rfl
 
 
 -- Temporary?
 variable [IsCyclic G] [DecidableEq G] (hq_prime : Nat.Prime q)
 
--- This is presumably a more convenient approach rather than including the do-block directly in a the type of pedersen_commitment_uniform
-noncomputable def generate_a : PMF $ ZMod q :=
-  do
-    let a ← PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2
-    return a
-
--- lemma sum_indicator_uniform {α : Type} [Fintype α] (p : α → Prop) [DecidablePred p] (h : (Finset.filter p Finset.univ).card = 1) :
---   ∑' (x : α), if p x then (↑(Fintype.card α))⁻¹ else 0 = (↑(Fintype.card α))⁻¹ := by
---     sorry
-
-lemma pedersen_commitment_uniform' (m : ZMod q) [DecidableEq G] (c : G) :
-  (PMF.bind (generate_a q hq_prime)
-    (fun a => PMF.bind (PMF.uniformOfFintype (ZMod q))
-      (fun r => PMF.pure (g^m.val * (g^a.val)^r.val)))) c = 1 / Fintype.card G := by
-      -- The key insight: for each non-zero a, the inner distribution is uniform over G
-      -- We'll show that the result doesn't depend on which a we sample
-      have h_uniform_inner : ∀ (a : ZMod q), a ≠ 0 →
-        (PMF.bind (PMF.uniformOfFintype (ZMod q))
-          (fun r => PMF.pure (g^m.val * (g^a.val)^r.val))) c = 1 / Fintype.card G := by
-        intro a ha
-        rw [PMF.bind_apply]
-        conv_lhs => arg 1; ext r; rw [PMF.pure_apply]
-        simp only [PMF.uniformOfFintype_apply, ZMod.card]
-        -- Need to show: ∑' r, (1/q) * (if c = g^m.val * (g^a.val)^r.val then 1 else 0) = 1 / |G|
-        -- Since |G| = q, this reduces to showing the sum of indicators equals 1
-        rw [ENNReal.tsum_mul_left, G_card_q, one_div]
-        -- Now need to show: q^{-1} * (sum of indicators) = q^{-1}
-        -- Equivalently: sum of indicators = 1
-        -- Convert to finset sum
-        rw [tsum_eq_sum (s := {r : ZMod q | c = g ^ m.val * (g ^ a.val) ^ r.val}.toFinset)]
-        swap
-        · simp only [Set.toFinset_setOf, Finset.mem_filter, Finset.mem_univ, true_and,
-          ite_eq_right_iff, one_ne_zero, imp_false, imp_self, implies_true]--intro r hr
-        -- The sum equals the cardinality
-        trans ((q : ENNReal)⁻¹ * ↑{r : ZMod q | c = g ^ m.val * (g ^ a.val) ^ r.val}.toFinset.card)
-        · congr 1
-          trans (∑ b ∈ {r : ZMod q | c = g ^ m.val * (g ^ a.val) ^ r.val}.toFinset, (1 : ENNReal))
-          · apply Finset.sum_congr rfl
-            intro b hb
-            simp only [Set.mem_toFinset, Set.mem_setOf_eq] at hb
-            simp [hb]
-          · rw [Finset.sum_const, nsmul_eq_mul, mul_one]
-        rw [Set.toFinset_card]
-        -- Now use pedersen_uniform_for_fixed_a to show the cardinality is 1
-        -- The cardinality of the set is 1, so q^{-1} * 1 = q^{-1}
-        have h_card : Fintype.card {r : ZMod q | c = g ^ m.val * (g ^ a.val) ^ r.val} = 1 := by
-          have h_finset : ({r : ZMod q | c = g ^ m.val * (g ^ a.val) ^ r.val} : Set (ZMod q)).toFinset.card = 1 := by
-            convert pedersen_uniform_for_fixed_a' q G_card_q g g_gen_G ha m c using 2
-            ext r
-            simp only [Set.toFinset_setOf, Finset.mem_filter, Finset.mem_univ, true_and]
-          have : Fintype.card {r : ZMod q | c = g ^ m.val * (g ^ a.val) ^ r.val} =
-                 ({r : ZMod q | c = g ^ m.val * (g ^ a.val) ^ r.val} : Set (ZMod q)).toFinset.card := by
-            simp only [Set.toFinset_card]
-          grind only
-        simp_all
-
-      -- Now use bind_skip_const' since the inner bind always gives the same distribution
-      have h_uniform_inner_gen : ∀ (a : ZMod q) (c' : G), a ≠ 0 →
-        (PMF.bind (PMF.uniformOfFintype (ZMod q))
-          (fun r => PMF.pure (g^m.val * (g^a.val)^r.val))) c' = 1 / Fintype.card G := by
-        intro a c' ha
-        -- This is the same proof as h_uniform_inner but for c' instead of c
-        rw [PMF.bind_apply]
-        conv_lhs => arg 1; ext r; rw [PMF.pure_apply]
-        simp only [PMF.uniformOfFintype_apply, ZMod.card]
-        rw [ENNReal.tsum_mul_left, G_card_q, one_div]
-        rw [tsum_eq_sum (s := {r : ZMod q | c' = g ^ m.val * (g ^ a.val) ^ r.val}.toFinset)]
-        swap
-        · intro r hr
-          simp only [Set.mem_toFinset, Set.mem_setOf_eq] at hr
-          simp [hr]
-        trans ((q : ENNReal)⁻¹ * ↑{r : ZMod q | c' = g ^ m.val * (g ^ a.val) ^ r.val}.toFinset.card)
-        · congr 1
-          trans (∑ b ∈ {r : ZMod q | c' = g ^ m.val * (g ^ a.val) ^ r.val}.toFinset, (1 : ENNReal))
-          · apply Finset.sum_congr rfl
-            intro b hb
-            simp only [Set.mem_toFinset, Set.mem_setOf_eq] at hb
-            simp [hb]
-          · rw [Finset.sum_const, nsmul_eq_mul, mul_one]
-        rw [Set.toFinset_card]
-        have h_card : Fintype.card {r : ZMod q | c' = g ^ m.val * (g ^ a.val) ^ r.val} = 1 := by
-          have h_finset : ({r : ZMod q | c' = g ^ m.val * (g ^ a.val) ^ r.val} : Set (ZMod q)).toFinset.card = 1 := by
-            convert pedersen_uniform_for_fixed_a' q G_card_q g g_gen_G ha m c' using 2
-            ext r
-            simp [Set.mem_toFinset]
-          have : Fintype.card {r : ZMod q | c' = g ^ m.val * (g ^ a.val) ^ r.val} =
-                 ({r : ZMod q | c' = g ^ m.val * (g ^ a.val) ^ r.val} : Set (ZMod q)).toFinset.card := by
-            simp only [Set.toFinset_card]
-          rw [this, h_finset]
-        rw [h_card]
-        simp
-      have h_const : ∀ a, a ∈ ((Finset.univ : Finset (ZMod q)).erase 0) →
-        (PMF.bind (PMF.uniformOfFintype (ZMod q))
-          (fun r => PMF.pure (g^m.val * (g^a.val)^r.val))) = PMF.uniformOfFintype G := by
-        intro a ha
-        ext c'
-        simp [Finset.mem_erase] at ha
-        rw [h_uniform_inner_gen a c' ha]
-        simp [PMF.uniformOfFintype_apply]
-      rw [generate_a]
-      rw [bind_pure_comp]
-      rw [id_map']
-
-      have : (PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2).bind
-          (fun a => (PMF.uniformOfFintype (ZMod q)).bind fun r => PMF.pure (g^m.val * (g^a.val)^r.val)) =
-        PMF.uniformOfFintype G := by
-        ext x
-        rw [PMF.bind_apply]
-        simp only [PMF.uniformOfFinset_apply]
-        trans (∑' a, (if a ∈ (nonzeroElements hq_prime).1 then ((nonzeroElements hq_prime).1.card : ENNReal)⁻¹ * (PMF.uniformOfFintype G) x else 0))
-        · apply tsum_congr
-          intro a
-          by_cases ha : a ∈ (nonzeroElements hq_prime).1
-          · simp only [ha, ite_true]
-            rw [h_const a ha]
-          · simp only [ha, ite_false, zero_mul]
-        · rw [tsum_eq_sum (s := (nonzeroElements hq_prime).1)]
-          · have : ∑ b ∈ (nonzeroElements hq_prime).1, (if b ∈ (nonzeroElements hq_prime).1 then ((nonzeroElements hq_prime).1.card : ENNReal)⁻¹ * (PMF.uniformOfFintype G) x else 0) =
-                   ∑ b ∈ (nonzeroElements hq_prime).1, ((nonzeroElements hq_prime).1.card : ENNReal)⁻¹ * (PMF.uniformOfFintype G) x := by
-              apply Finset.sum_congr rfl
-              intro b hb
-              simp only [hb, ite_true]
-            rw [this, Finset.sum_const, nsmul_eq_mul, PMF.uniformOfFintype_apply]
-            -- Goal: (nonzeroElements hq_prime).1.card * (((nonzeroElements hq_prime).1.card)⁻¹ * (Fintype.card G)⁻¹) = (Fintype.card G)⁻¹
-            calc ((nonzeroElements hq_prime).1.card : ENNReal) * (((nonzeroElements hq_prime).1.card : ENNReal)⁻¹ * (Fintype.card G : ENNReal)⁻¹)
-              _ = (((nonzeroElements hq_prime).1.card : ENNReal) * ((nonzeroElements hq_prime).1.card : ENNReal)⁻¹) * (Fintype.card G : ENNReal)⁻¹ := by
-                ring_nf
-              _ = 1 * (Fintype.card G : ENNReal)⁻¹ := by
-                congr 1
-                apply ENNReal.mul_inv_cancel
-                · simp
-                  exact Finset.Nonempty.ne_empty (nonzeroElements hq_prime).2
-                · exact ENNReal.natCast_ne_top _
-              _ = (Fintype.card G : ENNReal)⁻¹ := by rw [one_mul]
-          · intro a ha
-            simp [ha]
-      conv_lhs => rw [this]
-      simp [PMF.uniformOfFintype_apply]
-
-
-
-lemma pedersen_commitment_uniform (m : ZMod q) [DecidableEq G] (c : G) :
-  (do
-    let a ← PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2
-    let r ← PMF.uniformOfFintype (ZMod q)
-    return g^m.val * (g^a.val)^r.val : PMF G) c = 1 / Fintype.card G := by
-      sorry
+noncomputable def generate_a : PMF (ZModMult q) :=
+  PMF.uniformOfFintype (ZModMult q)
+
+lemma bij_uniform_for_fixed_a (a : ZModMult q) (m : ZMod q) :
+  PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q)) = (PMF.uniformOfFintype G) := by
+  · expose_names;
+    exact map_uniformOfFintype_equiv q G_card_q g g_gen_G (expEquiv q G_card_q g g_gen_G a m)
+
+lemma bij_uniform_for_uniform_a (m : ZMod q) :
+  (PMF.bind (generate_a q)
+    (fun a => PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q)))) = (PMF.uniformOfFintype G) := by
+  unfold generate_a
+  apply bind_skip_const'
+  intro a
+  · expose_names; exact bij_uniform_for_fixed_a q G_card_q g g_gen_G a m
+
+
+lemma pedersen_uniform_for_fixed_a_probablistic' (a : ZModMult q) (m : ZMod q) :
+  (Pedersen.commit G g q hq_prime (g^(val a).val) m) =
+  PMF.uniformOfFintype G := by
+  rw [← bij_uniform_for_fixed_a q G_card_q g g_gen_G a m]
+  -- Unfold Pedersen.commit
+  unfold Pedersen.commit
+  simp only [bind_pure_comp]
+  -- Now both sides are PMF.map over uniformOfFintype (ZMod q)
+  congr 1
+  funext r
+  exact (expEquiv_unfold q G_card_q g g_gen_G a m r).symm
+
+
+lemma bij_fixed_a_equiv_pedersen_commit (m : ZMod q) (a : ZModMult q) :
+  PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q)) =
+  (Pedersen.commit G g q hq_prime (g^(val a).val) m) := by
+  rw [bij_uniform_for_fixed_a q G_card_q g g_gen_G a m]
+  rw [← pedersen_uniform_for_fixed_a_probablistic' q G_card_q g g_gen_G hq_prime a m]
 
 
+lemma bij_random_a_equiv_pedersen_commit (m : ZMod q) :
+  PMF.bind (generate_a q)
+    (fun a => PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q))) =
+  PMF.bind (generate_a q)
+    (fun a => (Pedersen.commit G g q hq_prime (g^(val a).val) m)) := by
+  congr 1
+  funext a
+  exact bij_fixed_a_equiv_pedersen_commit q G_card_q g g_gen_G hq_prime m a
+
+
+-- for fixed aa ∈ {1, ... , q − 1}, and for any m ∈ Zq, if t ← Zq, then  g^m*h^r is uniformly distributed over G
+-- We can do this by proving t ↦ g^m*h^r is a bijection - see exp_bij above
+-- g^((m + (val a) * r : ZMod q).val : ℤ)
+lemma pedersen_uniform_for_fixed_a_probablistic
+  (a : ZModMult q) (m : ZMod q) [DecidableEq G] (c' : G) :
+  PMF.map commit.c ((Pedersen.scheme G g q hq_prime).commit (g^(val a).val) m) c' = 1 / (Fintype.card G) := by sorry
+
+
+
+
+-- lemma pedersen_commitment_uniform'' (m : ZMod q) [DecidableEq G] (c : G) :
+--   (PMF.bind (generate_a q)
+--     (fun a => PMF.bind (PMF.uniformOfFintype (ZMod q))
+--       (fun r => PMF.pure (g^m.val * (g^((val a).val))^r.val)))) c = 1 / Fintype.card G := by
+--       --have h_expEquiv : PMF.uniformOfFintype (ZMod q)).bind fun r ↦ PMF.pure (g ^ m.val * (g ^ (val a).val) ^ r.val
+--       unfold generate_a
+--       simp [PMF.bind_apply]
+--       rw [tsum_fintype]
+--       simp_rw [tsum_fintype]
+--       conv_lhs => arg 1; arg 2; rw [←bind_eq_map' q G_card_q g g_gen_G a m] --do I need to first get a version of expEquiv and unfold to match the def?
+
+--       sorry
+
 theorem Pedersen.perfect_hiding : ∀ (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G)
   (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q),
   perfect_hiding (Pedersen.scheme G g q hq_prime) := by
@@ -278,7 +254,3 @@ theorem Pedersen.perfect_hiding : ∀ (G : Type) [Fintype G] [Group G] [IsCyclic
     rw [Monad.toBind, PMF.instMonad]
 
     sorry
-
-
--- Collection of uniform distrbutions and need to choose uniformly among them
--- Seems that this is the work of a bind to map across two distributions
diff --git a/VerifiedCommitments/PedersenScheme.lean b/VerifiedCommitments/PedersenScheme.lean
index cfa503c..7d6d2ea 100644
--- a/VerifiedCommitments/PedersenScheme.lean
+++ b/VerifiedCommitments/PedersenScheme.lean
@@ -7,7 +7,7 @@ namespace Pedersen
     (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G)
       (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q) :
       CommitmentScheme (ZMod q) G (ZMod q) G := {
-    setup := --setup q hq g,
+    setup := -- PMF.bind (PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2) (fun a => return g^a.val), --setup q hq g,
     do
       let a ← PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2
       return g^a.val,
@@ -18,4 +18,14 @@ namespace Pedersen
     verify := fun h m c o => if c = g^m.val * h^o.val then 1 else 0  --verify h m c o g
   }
 
+  noncomputable def setup (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G)
+      (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q) : PMF G :=
+      PMF.bind (PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2) (fun a => return g^a.val)
+
+  noncomputable def commit (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G)
+      (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q) (h : G) (m : ZMod q) : PMF G :=
+      do
+        let r ← PMF.uniformOfFintype (ZMod q)
+        return g^m.val * h^r.val
+
 end Pedersen
diff --git a/VerifiedCommitments/ZModUtil.lean b/VerifiedCommitments/ZModUtil.lean
index 8467efb..3d4fa04 100644
--- a/VerifiedCommitments/ZModUtil.lean
+++ b/VerifiedCommitments/ZModUtil.lean
@@ -18,3 +18,9 @@ def ZModMult (q : ℕ) [NeZero q] := {a : ZMod q // a ≠ 0}
 
 -- Helper function to extract the value from ZModMult
 def val {q : ℕ} [NeZero q] (a : ZModMult q) : ZMod q := a.val
+
+-- Fintype instance for ZModMult
+instance {q : ℕ} [NeZero q] : Fintype (ZModMult q) :=
+  Fintype.subtype ((Finset.univ : Finset (ZMod q)).erase 0) (by simp [Finset.mem_erase])
+
+instance {q : ℕ} [NeZero q] : Nonempty (ZModMult q) := sorry