diff --git a/VerifiedCommitments/CommitmentScheme.lean b/VerifiedCommitments/CommitmentScheme.lean
index 6264201..45596e7 100644
--- a/VerifiedCommitments/CommitmentScheme.lean
+++ b/VerifiedCommitments/CommitmentScheme.lean
@@ -4,13 +4,14 @@ import Mathlib.Probability.ProbabilityMassFunction.Constructions
 import Mathlib.Data.ZMod.Defs
 
 
-structure commit (C O : Type) where
-  c : C
-  o : O
+-- namespace Crypto - or similar?
+-- structure Commit (C O : Type) where
+--   c : C
+--   o : O
 
 structure CommitmentScheme (M C O K : Type) where
-  setup : PMF K
-  commit : K → M → PMF (commit C O)
+  setup : PMF (K × O)
+  commit : K → M → PMF (C × O)
   verify : K → M → C → O → ZMod 2
 
 namespace Adversary
@@ -22,13 +23,18 @@ structure guess (M C O : Type) where
   o': O
 end Adversary
 
-variable {M C O K : Type}
+
+namespace Commitment
 
 noncomputable section
+variable {M C O K : Type}
+variable (scheme : CommitmentScheme M C O K)
+
+variable (h : K)
 
 def correctness (scheme : CommitmentScheme M C O K) : Prop :=
   ∀ (h : K) (m : M),
-  PMF.bind (scheme.commit h m) (fun commit => pure $ scheme.verify h m commit.c commit.o) = pure 1
+  PMF.bind (scheme.commit h m) (fun (commit, opening_val) => pure $ scheme.verify h m commit opening_val) = pure 1
 
 -- Perfect binding
 def perfect_binding (scheme : CommitmentScheme M C O K) : Prop :=
@@ -45,23 +51,20 @@ def perfect_binding (scheme : CommitmentScheme M C O K) : Prop :=
 def comp_binding_game (scheme : CommitmentScheme M C O K)
   (A : K → PMF (C × M × M × O × O)) : PMF $ ZMod 2 :=
   open scoped Classical in
-  do
-    let h ← scheme.setup
-    let (c, m, m', o, o') ← A h
-    if scheme.verify h m c o = 1 ∧ scheme.verify h m' c o' = 1 ∧ m ≠ m' then pure 1 else pure 0
+  PMF.bind scheme.setup (fun h =>
+    PMF.bind (A h.1) (fun (c, m , m', o, o') =>
+     if scheme.verify h.1 m c o = 1 ∧ scheme.verify h.1 m' c o' = 1 ∧ m ≠ m' then pure 1 else pure 0 ))
 
 def computational_binding [DecidableEq M] (scheme : CommitmentScheme M C O K) (ε : ENNReal) : Prop :=
   ∀ (A : K → PMF (C × M × M × O × O)), comp_binding_game scheme A 1 ≤ ε
 
-
 -- With Adversary namespace
 def comp_binding_game' (scheme : CommitmentScheme M C O K)
   (A' : K → PMF (Adversary.guess M C O)) : PMF $ ZMod 2 :=
   open scoped Classical in
-  do
-    let h ← scheme.setup
-    let guess ← A' h
-    if scheme.verify h guess.m guess.c guess.o = 1 ∧ scheme.verify h guess.m' guess.c guess.o' = 1 ∧ guess.m ≠ guess.m' then pure 1 else pure 0
+  PMF.bind scheme.setup (fun h =>
+    PMF.bind (A' h.1) (fun guess =>
+      if scheme.verify h.1 guess.m guess.c guess.o = 1 ∧ scheme.verify h.1 guess.m' guess.c guess.o' = 1 ∧ guess.m ≠ guess.m' then pure 1 else pure 0 ))
 
 def computational_binding' [DecidableEq M] (scheme : CommitmentScheme M C O K) (ε : ENNReal) : Prop :=
   ∀ (A' : K → PMF (Adversary.guess M C O )), comp_binding_game' scheme A' 1 ≤ ε
@@ -69,24 +72,23 @@ def computational_binding' [DecidableEq M] (scheme : CommitmentScheme M C O K) (
 
 -- Perfect hiding
 def do_commit (scheme: CommitmentScheme M C O K) (m : M) : PMF C :=
-do
-  let h ← scheme.setup
-  let commit ← scheme.commit h m
-  return commit.c
+PMF.bind scheme.setup (fun h =>
+  PMF.bind (scheme.commit h.1 m) (fun commit => pure commit.1))
 
 def perfect_hiding (scheme: CommitmentScheme M C O K) : Prop :=
   ∀ (m m' : M) (c : C), (do_commit scheme m) c = (do_commit scheme m') c
 
-
 -- Computational hiding game
 def comp_hiding_game (scheme : CommitmentScheme M C O K)
   (A : K → C → PMF (ZMod 2)) (m : M) : PMF (ZMod 2) :=
-  do
-    let h ← scheme.setup -- As above with comp_binding_game
-    let commit ← scheme.commit h m
-    A h commit.c
+  PMF.bind scheme.setup (fun h =>
+    PMF.bind (scheme.commit h.1 m) (fun commit => A h.1 commit.1))
 
 def computational_hiding (scheme : CommitmentScheme M C O K) (ε : ENNReal) : Prop :=
   ∀ (A : K → C → PMF (ZMod 2)) (m₀ m₁ : M),
   comp_hiding_game scheme A m₀ 1 - comp_hiding_game scheme A m₁ 1 ≤ ε ||
   comp_hiding_game scheme A m₁ 1 - comp_hiding_game scheme A m₀ 1 ≤ ε
+
+end
+
+end Commitment
diff --git a/VerifiedCommitments/PedersenBinding.lean b/VerifiedCommitments/PedersenBinding.lean
index 59225cb..aaee00e 100644
--- a/VerifiedCommitments/PedersenBinding.lean
+++ b/VerifiedCommitments/PedersenBinding.lean
@@ -1,101 +1,261 @@
 import VerifiedCommitments.PedersenScheme
+import VerifiedCommitments.dlog
 import Mathlib.Tactic
+import VerifiedCommitments.«scratch-skip-bind»
 
 namespace Pedersen
 
+-- Helper lemma: if binding succeeds, then either o = o' or we can extract the discrete log
+lemma binding_implies_dlog
+  (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G)
+    (q : ℕ) [NeZero q] [CancelMonoidWithZero (ZMod q)] (hq_prime : Nat.Prime q)
+    (G_card_q : Fintype.card G = q)
+    (hg_gen : orderOf g = Fintype.card G)
+    (a : ZMod q) (guess : Adversary.guess (ZMod q) G (ZMod q)) :
+  let h := g ^ a.val
+  let verify := fun (m : ZMod q) (c : G) (o : ZMod q) => if c = g^m.val * h^o.val then (1 : ZMod 2) else 0
+  (verify guess.m guess.c guess.o = 1 ∧ verify guess.m' guess.c guess.o' = 1 ∧ guess.m ≠ guess.m') →
+  (guess.o ≠ guess.o' → g^(((guess.m - guess.m') * (guess.o' - guess.o)⁻¹).val) = h) := by
+  intro h verify ⟨h1, h2, m_ne⟩ o_ne
+  -- From h1: guess.c = g^(guess.m).val * h^(guess.o).val
+  -- From h2: guess.c = g^(guess.m').val * h^(guess.o').val
+  simp only [verify] at h1 h2
+  split at h1 <;> split at h2
+  case' isTrue.isTrue c_eq1 c_eq2 =>
+    simp only [h] at c_eq1 c_eq2
+
+    have collision : g^guess.m.val * (g^a.val)^guess.o.val = g^guess.m'.val * (g^a.val)^guess.o'.val := by
+      rw [← c_eq1, c_eq2]
+
+    conv_lhs at collision => arg 2; rw [← pow_mul]
+    conv_rhs at collision => arg 2; rw [← pow_mul]
+    rw [← pow_add, ← pow_add] at collision
+
+    have h_coprime : (guess.o' - guess.o).val.Coprime q := by
+      cases' Nat.coprime_or_dvd_of_prime hq_prime (guess.o' - guess.o).val with h_cop h_dvd
+      · exact Nat.coprime_comm.mp h_cop
+      · exfalso
+        have h_zero : guess.o' - guess.o = 0 := by
+          rw [← ZMod.val_eq_zero]
+          have h_mod_zero : (guess.o' - guess.o).val % q = 0 := Nat.mod_eq_zero_of_dvd h_dvd
+          have h_val_bound : (guess.o' - guess.o).val < q := ZMod.val_lt (guess.o' - guess.o)
+          exact Nat.eq_zero_of_dvd_of_lt h_dvd h_val_bound
+        exact o_ne.symm (eq_of_sub_eq_zero h_zero)
+
+    have h_ord : orderOf g = q := by
+      rw [← G_card_q]; exact hg_gen
+
+    have h_congr_nat : guess.m.val + a.val * guess.o.val ≡ guess.m'.val + a.val * guess.o'.val [MOD q] := by
+      simpa [h_ord] using (pow_eq_pow_iff_modEq.mp collision)
+
+    have h_zmod : (guess.m + a * guess.o : ZMod q) = (guess.m' + a * guess.o' : ZMod q) := by
+      have eq_cast : ((guess.m.val + a.val * guess.o.val : ℕ) : ZMod q) =
+                    ((guess.m'.val + a.val * guess.o'.val : ℕ) : ZMod q) :=
+        (ZMod.eq_iff_modEq_nat _).mpr h_congr_nat
+      simp at eq_cast
+      exact eq_cast
+
+    have h_lin : a * (guess.o' - guess.o) = guess.m - guess.m' := by grind
+
+    have h_unit : guess.o' - guess.o ≠ 0 := sub_ne_zero.mpr o_ne.symm
+
+    have h_solve_x : a = (guess.m - guess.m') * (guess.o' - guess.o)⁻¹ := by
+      calc a = a * 1                                 := by rw [mul_one]
+        _ = a * ((guess.o' - guess.o) * (guess.o' - guess.o)⁻¹)              := by
+          haveI : Fact (Nat.Prime q) := ⟨hq_prime⟩
+          rw [← one_mul a]
+          congr 1
+          have h_field_inv : (guess.o' - guess.o) * (guess.o' - guess.o)⁻¹ = 1 := by
+            apply Field.mul_inv_cancel
+            exact h_unit
+          exact h_field_inv.symm
+        _ = (a * (guess.o' - guess.o)) * (guess.o' - guess.o)⁻¹              := by rw [mul_assoc]
+        _ = (guess.m - guess.m') * (guess.o' - guess.o)⁻¹                    := by rw [h_lin]
+
+    have h_congr_final : ((guess.m - guess.m') * (guess.o' - guess.o)⁻¹).val ≡ a.val [MOD q] := by
+      have h1 : (((guess.m - guess.m') * (guess.o' - guess.o)⁻¹).val : ZMod q) = (guess.m - guess.m') * (guess.o' - guess.o)⁻¹ :=
+        ZMod.natCast_zmod_val ((guess.m - guess.m') * (guess.o' - guess.o)⁻¹)
+      have h2 : (a.val : ZMod q) = a := ZMod.natCast_zmod_val a
+      rw [← ZMod.eq_iff_modEq_nat]
+      rw [h1, h2]
+      exact h_solve_x.symm
+
+    have h_eq : g ^ ((guess.m - guess.m') * (guess.o' - guess.o)⁻¹).val = g ^ a.val :=
+      (pow_eq_pow_iff_modEq.mpr (by rwa [h_ord]))
+
+    rw [h_eq]
+  all_goals contradiction
+
 lemma binding_as_hard_dlog
   (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G)
-    (q : ℕ) [NeZero q] [CancelMonoidWithZero (ZMod q)] (hq_prime : Nat.Prime q) (ε : ENNReal)
+    (q : ℕ) [NeZero q] [CancelMonoidWithZero (ZMod q)] (hq_prime : Nat.Prime q)
     (G_card_q : Fintype.card G = q)
     (hg_gen : orderOf g = Fintype.card G)
-    (A : G → PMF (Adversary.guess (ZMod q) G (ZMod q))) :
-    comp_binding_game' (Pedersen.scheme G g q hq_prime) A 1 ≤ DLog.experiment G g q hq_prime (DLog.adversary' G q A) 1 := by
-  simp only [DLog.experiment, comp_binding_game', Pedersen.scheme, DLog.adversary']
-  simp only [bind_pure_comp, ite_eq_left_iff, zero_ne_one, imp_false, Decidable.not_not, ne_eq,
-    bind_map_left, ite_not, map_bind]
-  congr! 5 with x ⟨c, m, m', o, o'⟩
-  simp
-  split_ifs
-  · sorry -- this is a case I want to skip
-  rename_i ho
-  rename_i h
-  obtain ⟨h1, h2, h3⟩ := h
-  rw [h1] at h2
-  simp only [map_pure]
-  have h_noo' : o' ≠ o := by exact fun a ↦ ho (id (Eq.symm a))
-  have h_coprime : (o' - o).val.Coprime q := by
-    cases' Nat.coprime_or_dvd_of_prime hq_prime (o' - o).val with h_cop h_dvd
-    · exact Nat.coprime_comm.mp h_cop
-    · exfalso
-      have h_zero : o' - o = 0 := by
-        rw [← ZMod.val_eq_zero]
-        have h_mod_zero : (o' - o).val % q = 0 := Nat.mod_eq_zero_of_dvd h_dvd
-        have h_val_bound : (o' - o).val < q := ZMod.val_lt (o' - o)
-        exact Nat.eq_zero_of_dvd_of_lt h_dvd h_val_bound
-      exact h_noo' (eq_of_sub_eq_zero h_zero)
-
-  have h_ex_inv : ∃ y, ↑(o' - o).val * y ≡ 1 [ZMOD q] := by apply Int.mod_coprime h_coprime
-
-  have h_ord : orderOf g = q := by
-    rw [← G_card_q]; exact hg_gen
-
-  have h_pow : g ^ (m.val + x.val * o.val) = g ^ (m'.val + x.val * o'.val) := by
-    simp [←pow_mul, ←pow_add] at h2
-    exact h2
-
-  have h_congr_nat : m.val + x.val * o.val ≡ m'.val + x.val * o'.val [MOD q] := by
-    simpa [h_ord] using (pow_eq_pow_iff_modEq.mp h_pow)
-
-  have h_zmod : (m + x * o : ZMod q) = (m' + x * o' : ZMod q) := by
-    have eq_cast : ((m.val + x.val * o.val : ℕ) : ZMod q) =
-                  ((m'.val + x.val * o'.val : ℕ) : ZMod q) :=
-      (ZMod.eq_iff_modEq_nat _).mpr h_congr_nat
-    simp at eq_cast
-    exact eq_cast
-
-  have h_lin : x * (o' - o) = m - m' := by grind
-
-  have h_unit : o' - o ≠ 0 := sub_ne_zero.mpr h_noo'
-
-  have h_solve_x : x = (m - m') * (o' - o)⁻¹ := by
-     calc x = x * 1                                 := by rw [mul_one]
-       _ = x * ((o' - o) * (o' - o)⁻¹)              := by
-        haveI : Fact (Nat.Prime q) := ⟨hq_prime⟩
-        rw [← one_mul x]
-        congr 1
-        have h_field_inv : (o' - o) * (o' - o)⁻¹ = 1 := by
-          apply Field.mul_inv_cancel
-          exact h_unit
-        exact h_field_inv.symm
-       _ = (x * (o' - o)) * (o' - o)⁻¹              := by rw [mul_assoc]
-       _ = (m - m') * (o' - o)⁻¹                    := by rw [h_lin]
-
-  have h_congr_final : ((m - m') * (o' - o)⁻¹).val ≡ x.val [MOD q] := by
-    have h1 : (((m - m') * (o' - o)⁻¹).val : ZMod q) = (m - m') * (o' - o)⁻¹ :=
-      ZMod.natCast_zmod_val ((m - m') * (o' - o)⁻¹)
-    have h2 : (x.val : ZMod q) = x := ZMod.natCast_zmod_val x
-    rw [← ZMod.eq_iff_modEq_nat]
-    rw [h1, h2]
-    exact h_solve_x.symm
-
-  have h_eq : g ^ ((m - m') * (o' - o)⁻¹).val = g ^ x.val :=
-    (pow_eq_pow_iff_modEq.mpr (by rwa [h_ord]))
-
-  rw [h_eq]
-  simp only [↓reduceIte]
-  · sorry -- cases I want to skip
-  · sorry
-
-
-theorem Pedersen.computational_binding :
+    (A : G → PMF (Adversary.guess (ZMod q) G (ZMod q))) : -- Pedersen adversary
+    haveI : Fact (Nat.Prime q) := ⟨hq_prime⟩;
+    Commitment.comp_binding_game' (Pedersen.scheme G g q hq_prime) A 1 ≤ DLog.experiment G g q hq_prime (DLog.adversary' G q A) 1 := by
+  haveI : Fact (Nat.Prime q) := ⟨hq_prime⟩
+  -- Unfold definitions
+  unfold Commitment.comp_binding_game' DLog.experiment DLog.adversary'
+  simp only [Pedersen.scheme, Pedersen.setup, Pedersen.verify]
+
+  -- Expand the bind applications
+  rw [PMF.bind_apply, PMF.bind_apply]
+
+  -- Both sum over the same type: G × ZMod q (the pairs from setup)
+  -- We need pointwise inequality
+  apply ENNReal.tsum_le_tsum
+  intro ⟨h, a⟩
+
+  -- Key observation: setup only returns pairs (g^x.val, x)
+  -- So if h ≠ g^a.val, the probability of this pair is 0 and inequality holds trivially
+  by_cases h_case : h = g^a.val
+
+  · -- Case: h = g^a.val (pair is in support of setup)
+    subst h_case  -- Replace h with g^a.val everywhere
+
+    -- Now we have h = g^a.val as needed!
+    apply mul_le_mul_right
+
+    -- Now compare the inner probabilities
+    -- Continue with the proof that was already working
+    -- First, use bind associativity on RHS to flatten the nested binds
+    conv_rhs => rw [PMF.bind_bind]
+
+    -- Now both have structure: (A (g^a.val)).bind (fun guess => ...) 1
+    -- Expand the bind application
+    rw [PMF.bind_apply, PMF.bind_apply]
+
+    -- Now both are sums over Adversary.guess
+    apply ENNReal.tsum_le_tsum
+    intro guess
+
+    apply mul_le_mul_right
+
+    -- For each guess, show:
+    -- (if [binding succeeds] then pure 1 else pure 0) 1 ≤
+    -- ((if o≠o' then pure x' else uniform).bind (λ x'. pure (if g^x'=g^a then 1 else 0))) 1
+
+    simp only [ite_eq_left_iff, zero_ne_one, imp_false, Decidable.not_not, ne_eq, ite_not,
+      PMF.bind_apply, tsum_fintype]
+    rw [@DFunLike.ite_apply]
+    split_ifs with h₁ h₂
+
+    · -- Case 1: h₁ (binding) AND h₂ (o = o')
+      -- This is the contradiction case: o = o' but binding succeeds
+      exfalso
+      obtain ⟨eq1, eq2, m_ne⟩ := h₁
+      -- Since h₂: o = o', we have (g^a.val)^o.val = (g^a.val)^o'.val
+      have ho_eq : (g^a.val)^guess.o.val = (g^a.val)^guess.o'.val := by
+        rw [h₂]
+      -- So: g^m.val * (g^a.val)^o.val = g^m'.val * (g^a.val)^o.val
+      have collision : g^guess.m.val * (g^a.val)^guess.o.val = g^guess.m'.val * (g^a.val)^guess.o.val := by
+        calc g^guess.m.val * (g^a.val)^guess.o.val
+            = guess.c := eq1.symm
+          _ = g^guess.m'.val * (g^a.val)^guess.o'.val := eq2
+          _ = g^guess.m'.val * (g^a.val)^guess.o.val := by rw [← ho_eq]
+      -- Cancel (g^a.val)^o.val from both sides
+      have g_eq : g^guess.m.val = g^guess.m'.val := mul_right_cancel collision
+      -- Since g is a generator, this means m.val ≡ m'.val (mod q)
+      have h_ord : orderOf g = q := by rw [← G_card_q]; exact hg_gen
+      have h_congr : guess.m.val ≡ guess.m'.val [MOD q] := by
+        simpa [h_ord] using (pow_eq_pow_iff_modEq.mp g_eq)
+      -- Therefore m = m' in ZMod q
+      have m_eq : guess.m = guess.m' := by
+        have eq_cast : ((guess.m.val : ℕ) : ZMod q) = ((guess.m'.val : ℕ) : ZMod q) :=
+          ZMod.natCast_eq_natCast_iff guess.m.val guess.m'.val q |>.mpr h_congr
+        simp at eq_cast
+        exact eq_cast
+      exact m_ne m_eq
+
+    · -- Case 2: Binding succeeds (h₁) AND o ≠ o' (¬h₂)
+      -- This is the main case where we use binding_implies_dlog
+      have h_o_ne : guess.o ≠ guess.o' := h₂
+      let x' := (guess.m - guess.m') * (guess.o' - guess.o)⁻¹
+
+      -- Convert h₁ to the form expected by binding_implies_dlog
+      have h₁' : (let h := g^a.val;
+                  let verify := fun m c o => if c = g^m.val * h^o.val then (1 : ZMod 2) else 0;
+                  verify guess.m guess.c guess.o = 1 ∧ verify guess.m' guess.c guess.o' = 1 ∧ guess.m ≠ guess.m') := by
+        obtain ⟨eq1, eq2, m_ne⟩ := h₁
+        simp only []
+        refine ⟨?_, ?_, m_ne⟩
+        · split
+          · rfl
+          · contradiction
+        · split
+          · rfl
+          · contradiction
+
+      -- By binding_implies_dlog, g^x'.val = g^a.val
+      have h_dlog : g^x'.val = g^a.val := by
+        apply binding_implies_dlog G g q hq_prime G_card_q hg_gen a guess h₁' h_o_ne
+
+      -- The RHS is a sum over a single-element distribution (pure x')
+      -- The sum includes the term for x = x', which equals 1
+      have h_term : (PMF.pure x') x' * (PMF.pure (if g^x'.val = g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) = 1 := by
+        rw [PMF.pure_apply, PMF.pure_apply]
+        simp only [h_dlog]
+        norm_num
+      have h_zero : ∀ x ∈ Finset.univ, x ∉ ({x'} : Finset (ZMod q)) →
+                    (PMF.pure x') x * (PMF.pure (if g^x.val = g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) = 0 := by
+        intros x _ hx
+        rw [PMF.pure_apply]
+        simp only [Finset.mem_singleton] at hx
+        simp [hx]
+      have h_sum_ge : (PMF.pure x') x' * (PMF.pure (if g^x'.val = g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) ≤
+                      ∑ x, (PMF.pure x') x * (PMF.pure (if g^x.val = g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) := by
+        rw [← Finset.sum_subset (Finset.subset_univ {x'}) h_zero]
+        simp only [Finset.sum_singleton]
+        rfl
+      calc (PMF.pure (1 : ZMod 2)) (1 : ZMod 2)
+          = 1 := by rw [PMF.pure_apply]; norm_num
+        _ = (PMF.pure x') x' * (PMF.pure (if g^x'.val = g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) := h_term.symm
+        _ ≤ ∑ x, (PMF.pure x') x * (PMF.pure (if g^x.val = g^a.val then (1 : ZMod 2) else 0)) (1 : ZMod 2) := h_sum_ge
+
+    · -- Case 3: Binding fails (¬h₁) AND o = o' (h✝)
+      show (PMF.pure (0 : ZMod 2)) (1 : ZMod 2) ≤ _
+      rw [PMF.pure_apply]
+      norm_num
+
+    · -- Case 4: Binding fails (¬h₁) AND o ≠ o' (¬h✝)
+      show (PMF.pure (0 : ZMod 2)) (1 : ZMod 2) ≤ _
+      rw [PMF.pure_apply]
+      norm_num
+
+  · -- Case neg: h ≠ g^a.val (pair is NOT in support)
+    -- Setup only returns pairs of the form (g^x.val, x)
+    -- So if h ≠ g^a.val, then (h, a) has probability 0 in the setup distribution
+    -- Therefore both sides are 0 * something = 0, and 0 ≤ 0
+    have h_prob_zero : ((PMF.uniformOfFintype (ZModMult q)).bind fun a_mult => PMF.pure (g^(val a_mult).val, val a_mult)) (h, a) = 0 := by
+      rw [PMF.bind_apply, tsum_fintype]
+      apply Finset.sum_eq_zero
+      intros a_mult _
+      rw [PMF.pure_apply, PMF.uniformOfFintype_apply]
+      split_ifs with h_eq
+      · -- If (h, a) = (g^(val a_mult).val, val a_mult)
+        -- Then h = g^(val a_mult).val and a = val a_mult
+        exfalso
+        have eq_h : h = g^(val a_mult).val := (Prod.mk.injEq _ _ _ _).mp h_eq |>.1
+        have eq_a : a = val a_mult := (Prod.mk.injEq _ _ _ _).mp h_eq |>.2
+        rw [← eq_a] at eq_h
+        exact h_case eq_h
+      · simp
+    change ((PMF.uniformOfFintype (ZModMult q)).bind fun a_mult => PMF.pure (g^(val a_mult).val, val a_mult)) (h, a) * _ ≤
+           ((PMF.uniformOfFintype (ZModMult q)).bind fun a_mult => PMF.pure (g^(val a_mult).val, val a_mult)) (h, a) * _
+    rw [h_prob_zero]
+    simp only [zero_mul, le_refl]
+
+
+theorem computational_binding :
   ∀ (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G)
-    (q : ℕ) [NeZero q] [CancelMonoidWithZero (ZMod q)] (hq_prime : Nat.Prime q) (ε : ENNReal)
+    (q : ℕ) [NeZero q] [CancelMonoidWithZero (ZMod q)] [Fact (Nat.Prime q)] (hq_prime : (Nat.Prime q)) (ε : ENNReal)
     (G_card_q : Fintype.card G = q)
     (hg_gen : orderOf g = Fintype.card G),
     (∀ (A : G → PMF (ZMod q)), DLog.experiment G g q hq_prime A 1 ≤ ε) →
     (∀ (A : G → PMF (Adversary.guess (ZMod q) G (ZMod q))),
-    comp_binding_game' (Pedersen.scheme G g q hq_prime) A 1 ≤ ε) := by
-  intro G _ _ _ _ g q _ _ hq_prime ε G_card_q hg_gen hdlog A
-  exact le_trans (binding_as_hard_dlog G g q hq_prime ε G_card_q hg_gen A) (hdlog (DLog.adversary' G q A))
-
+    ∃ hq_prime : Nat.Prime q, Commitment.comp_binding_game' (Pedersen.scheme G g q hq_prime) A 1 ≤ ε) := by
+  intro G _ _ _ _ g q _ _ _ hq_prime ε G_card_q hg_gen hdlog A
+  use hq_prime
+  exact le_trans (binding_as_hard_dlog G g q hq_prime G_card_q hg_gen A) (hdlog (DLog.adversary' G q A))
 end Pedersen
diff --git a/VerifiedCommitments/PedersenHiding.lean b/VerifiedCommitments/PedersenHiding.lean
index 9b325a9..5657287 100644
--- a/VerifiedCommitments/PedersenHiding.lean
+++ b/VerifiedCommitments/PedersenHiding.lean
@@ -1,10 +1,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»
 
+namespace Pedersen
 
 variable {G: Type} [Fintype G] [Group G]
 variable (q : ℕ) [Fact (Nat.Prime q)]
@@ -66,7 +66,7 @@ lemma exp_bij' (a : ZModMult q) (m : ZMod q) : Function.Bijective fun (r : ZMod
 
 
 -- Fintype instance for commit
-instance {C O : Type} [Fintype C] [Fintype O] : Fintype (commit C O) :=
+instance {C O : Type} [Fintype C] [Fintype O] : Fintype (C × O) :=
   Fintype.ofEquiv (C × O) {
     toFun := fun ⟨c, o⟩ => ⟨c, o⟩
     invFun := fun ⟨c, o⟩ => ⟨c, o⟩
@@ -168,13 +168,6 @@ lemma bind_eq_map' : ∀ (fixed_a : ZModMult q) (fixed_m : ZMod q),
   intros
   exact rfl
 
-
--- Temporary?
-variable [IsCyclic G] [DecidableEq G] (hq_prime : Nat.Prime q)
-
-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;
@@ -188,69 +181,68 @@ lemma bij_uniform_for_uniform_a (m : ZMod q) :
   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
+lemma pedersen_commitment_uniform (m : ZMod q) (c : G) :
+  (PMF.map Prod.fst ((PMF.bind (generate_a q)
+    (fun a => Pedersen.commit G g q (g^(val a).val) m ))) c) =
+    ((1 : ENNReal) / (Fintype.card G)) := by
+    unfold Pedersen.commit
+    simp only [PMF.map_bind, pure, PMF.pure_map]
+    have h_eq : (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)))) =
+                (PMF.bind (generate_a q)
+                  (fun a => PMF.map (expEquiv q G_card_q g g_gen_G a m) (PMF.uniformOfFintype (ZMod q)))) := by
+      apply bind_skip'
+      intro a
+      ext x
+      simp only [PMF.bind_apply, PMF.map_apply, PMF.pure_apply, PMF.uniformOfFintype_apply]
+      congr 1; ext r
+      by_cases h : x = g^m.val * (g^(val a).val)^r.val
+      · simp only [h, ↓reduceIte]
+        rw [← expEquiv_unfold q G_card_q g g_gen_G a m r]
+        simp
+      · simp only [h, ↓reduceIte]
+        have : x ≠ expEquiv q G_card_q g g_gen_G a m r := by
+          intro contra
+          rw [expEquiv_unfold q G_card_q g g_gen_G a m r] at contra
+          exact h contra
+        simp [this]
+    rw [h_eq]
+    rw [bij_uniform_for_uniform_a q G_card_q g g_gen_G m]
+    simp [PMF.uniformOfFintype_apply]
+
+
+end Pedersen
 
 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
-    intros G _ _ _ _ g q _ hq_prime
-    simp only [Pedersen.scheme, _root_.perfect_hiding, do_commit]
-    simp only [bind_pure_comp, Functor.map_map, bind_map_left]
-    intro m m' c
-    rw [bind, Functor.map]
-    simp only [PMF]
-    rw [Monad.toBind, PMF.instMonad]
-
-    sorry
+  (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q)
+  (G_card_q : Fintype.card G = q)
+  (g_gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g),
+  haveI : Fact (Nat.Prime q) := ⟨hq_prime⟩; Commitment.perfect_hiding (Pedersen.scheme G g q hq_prime) := by
+    intros G _ _ _ _ g q _ hq_prime G_card_q g_gen_G
+    haveI : Fact (Nat.Prime q) := ⟨hq_prime⟩
+    unfold Commitment.perfect_hiding
+    intros m m' c
+    unfold Commitment.do_commit Pedersen.scheme
+    simp only []
+    unfold Pedersen.setup Pedersen.commit
+    simp only [PMF.bind_bind]
+    have h_lhs : ((PMF.uniformOfFintype (ZModMult q)).bind fun a =>
+                   PMF.bind (pure (g^(val a).val, val a)) fun h =>
+                     (PMF.uniformOfFintype (ZMod q)).bind fun r =>
+                       PMF.bind (pure (g^m.val * h.1^r.val, r)) fun commit =>
+                         pure commit.1) c = 1 / Fintype.card G := by
+      simp only [pure, PMF.pure_bind]
+      convert pedersen_commitment_uniform q G_card_q g g_gen_G m c using 2
+      unfold generate_a Pedersen.commit
+      simp only [PMF.map_bind, pure, PMF.pure_map]
+    have h_rhs : ((PMF.uniformOfFintype (ZModMult q)).bind fun a =>
+                   PMF.bind (pure (g^(val a).val, val a)) fun h =>
+                     (PMF.uniformOfFintype (ZMod q)).bind fun r =>
+                       PMF.bind (pure (g^m'.val * h.1^r.val, r)) fun commit =>
+                         pure commit.1) c = 1 / Fintype.card G := by
+      simp only [pure, PMF.pure_bind]
+      convert pedersen_commitment_uniform q G_card_q g g_gen_G m' c using 2
+      unfold generate_a Pedersen.commit
+      simp only [PMF.map_bind, pure, PMF.pure_map]
+    rw [h_lhs, h_rhs]
diff --git a/VerifiedCommitments/PedersenScheme.lean b/VerifiedCommitments/PedersenScheme.lean
index 7d6d2ea..f78a6e0 100644
--- a/VerifiedCommitments/PedersenScheme.lean
+++ b/VerifiedCommitments/PedersenScheme.lean
@@ -1,31 +1,42 @@
 import VerifiedCommitments.CommitmentScheme
-import VerifiedCommitments.dlog
+import Mathlib.Probability.Distributions.Uniform
+import VerifiedCommitments.ZModUtil
 
 namespace Pedersen
 
-  noncomputable def scheme
+-- TODO: I'm not sure this should be here, or that
+-- Setup should definitely return h, but should there be another def hanging around that computes an a independently?
+-- The two alternatives below for bind in setup may have some bearing on how the binding proof progresses, unless I change the dlog definitions to match...
+
+noncomputable def generate_a (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] : PMF (ZModMult q) :=
+  PMF.uniformOfFintype (ZModMult q)
+
+
+noncomputable section
+
+  def setup (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G)
+    (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] (hq_prime : Nat.Prime q) : PMF (G × (ZMod q)) :=
+    PMF.bind (PMF.uniformOfFintype (ZModMult q)) (fun a => return ⟨g^(val a).val, val a⟩)
+    -- PMF.bind (PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2) (fun a => return g^a.val)
+
+  def commit (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G)
+    (q : ℕ) [NeZero q] (h : G) (m : ZMod q) : PMF (G × (ZMod q)) :=
+    PMF.bind (PMF.uniformOfFintype (ZMod q)) (fun r => return ⟨g^m.val * h^r.val, r⟩)
+
+  def verify (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G)
+    (q : ℕ) [NeZero q] (h : G) (m : ZMod q) (c : G) (o : ZMod q): ZMod 2 :=
+    if c = g^m.val * h^o.val then 1 else 0
+
+  def scheme
     (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 := -- 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,
-    commit := fun h m =>  --commit h m g,
-    do
-      let r ← PMF.uniformOfFintype (ZMod q)
-      return ⟨g^m.val * h^r.val, r⟩,
-    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
+    (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] (hq_prime : Nat.Prime q) :
+    CommitmentScheme (ZMod q) G (ZMod q) G := {
+      setup := setup G g q hq_prime,
+      commit (h : G) (m : ZMod q) := commit G g q h m,
+      verify (h : G) (m : ZMod q) (c : G) (o : ZMod q):= verify G g q h m c o
+    }
 
+end
 end Pedersen
+
+instance {G : Type} {q : ℕ} [NeZero q] : Nonempty (G × (ZMod q)) := sorry
diff --git a/VerifiedCommitments/ZModUtil.lean b/VerifiedCommitments/ZModUtil.lean
index 3d4fa04..def9da1 100644
--- a/VerifiedCommitments/ZModUtil.lean
+++ b/VerifiedCommitments/ZModUtil.lean
@@ -23,4 +23,4 @@ def val {q : ℕ} [NeZero q] (a : ZModMult q) : ZMod q := a.val
 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
+instance {q : ℕ} [NeZero q] [Fact (Nat.Prime q)] : Nonempty (ZModMult q) := ⟨⟨1, one_ne_zero⟩⟩
diff --git a/VerifiedCommitments/dlog.lean b/VerifiedCommitments/dlog.lean
index 04b7b39..60fe676 100644
--- a/VerifiedCommitments/dlog.lean
+++ b/VerifiedCommitments/dlog.lean
@@ -1,9 +1,4 @@
-import Mathlib.Probability.ProbabilityMassFunction.Basic
-import Mathlib.Probability.ProbabilityMassFunction.Monad
-import Mathlib.Probability.Distributions.Uniform
-import Mathlib.Data.ZMod.Basic
-import VerifiedCommitments.ProofUtils
-import VerifiedCommitments.CommitmentScheme
+import VerifiedCommitments.PedersenScheme
 
 namespace DLog
 
@@ -11,47 +6,45 @@ noncomputable section
 
 -- Modification of Attack game and advantage as specified in Boneh 10.4 to account for check between generated x and x'
 def attack_game (G : Type) [Group G] (q : ℕ) [NeZero q] (g : G) (A : G → PMF (ZMod q)) : PMF (ZMod 2) :=
-do
-  let x ← PMF.uniformOfFintype (ZMod q)
-  let x' ← A (g^x.val)
-  pure (if x = x' then 1 else 0)
+PMF.bind (PMF.uniformOfFintype (ZMod q)) (fun x =>
+  PMF.bind (A (g^x.val)) (fun x' => pure (if x = x' then 1 else 0)))
 
 -- The advantage of an attacker A in the DLog problem
 -- attack_game returns a PMF ()
 def advantage (G : Type) [Group G] (q : ℕ) [NeZero q] (g : G) (A : G → PMF (ZMod q)) : ENNReal := attack_game G q g A 1
 
+#check Pedersen.scheme
 noncomputable def experiment
   (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G] (g : G)
-    (q : ℕ) [NeZero q] (hq_prime : Nat.Prime q)
+    (q : ℕ) [NeZero q] [Fact (Nat.Prime q)] (hq_prime : Nat.Prime q)
     (A' : G → PMF (ZMod q)) : PMF (ZMod 2) :=
-  do
-    let x ← PMF.uniformOfFinset (nonzeroElements hq_prime).1 (nonzeroElements hq_prime).2
-    let h := g^x.val
-    let x' ← A' h
-    pure (if g^x'.val = h then 1 else 0)
+  PMF.bind (Pedersen.scheme G g q hq_prime).setup (fun h =>
+    PMF.bind (A' h.1) (fun x' => pure (if g^x'.val = g^(h.2).val then 1 else 0)))
+  -- PMF.bind (PMF.uniformOfFintype (ZModMult q)) (fun x =>
+  --   PMF.bind (A' (g^(val x).val)) (fun x' => pure (if g^x'.val = g^(val x).val then 1 else 0)))
 
   noncomputable def adversary
     (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G]
       (q : ℕ) [NeZero q]
       (A : G → PMF (G × ZMod q × ZMod q × ZMod q × ZMod q))
       (h : G) : PMF (ZMod q) :=
-    do
-      let (_c, m, m', o, o') ← A h
-      if o ≠ o' then
+    PMF.bind (A h) (fun (_c, m, m', o, o') =>
+       if o ≠ o' then
         return ((m - m') * (o' - o)⁻¹)
       else
         PMF.uniformOfFintype (ZMod q)
+    )
 
   noncomputable def adversary'
     (G : Type) [Fintype G] [Group G] [IsCyclic G] [DecidableEq G]
       (q : ℕ) [NeZero q]
       (A' : G → PMF (Adversary.guess (ZMod q) G (ZMod q)))
       (h : G) : PMF (ZMod q) :=
-    do
-      let guess ← A' h
+    PMF.bind (A' h) (fun guess =>
       if guess.o ≠ guess.o' then
         return ((guess.m - guess.m') * (guess.o' - guess.o)⁻¹)
       else
         PMF.uniformOfFintype (ZMod q)
+      )
 end
 end DLog
diff --git a/lake-manifest.json b/lake-manifest.json
index 294bf9b..f4ce7bb 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a778305ec3a679802f7dcfa64e2b903d4679ee21",
+   "rev": "6c8fd6fb284ad384ef49513a1d0515b2441799a5",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9f492660e9837df43fd885a2ad05c520da9ff9f5",
+   "rev": "e2a2ee109182182dd0e347e8149d312d72bfbfb2",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
+   "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "90f3b0f429411beeeb29bbc248d799c18a2d520d",
+   "rev": "cff9dd30f2c161b9efd7c657cafed1f967645890",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "556caed0eadb7901e068131d1be208dd907d07a2",
+   "rev": "ef8377f31b5535430b6753a974d685b0019d0681",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.74",
+   "inputRev": "v0.0.84",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "14d8accc7513f8a85ae142201907f49f518ae0ec",
+   "rev": "fa78cf032194308a950a264ed87b422a2a7c1c6c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2e582a44b0150db152bff1c8484eb557fb5340da",
+   "rev": "8920dcbb96a4e8bf641fc399ac9c0888e4a6be72",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9c1ad6d93126e346c859d4a17d71b010e7951f92",
+   "rev": "78129e1913fe4988ac238156ec5f223ec02d286c",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "b62fd39acc32da6fb8bb160c82d1bbc3cb3c186e",
+   "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.27.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "«verified-commitments»",
diff --git a/lean-toolchain b/lean-toolchain
index 66a6d41..fb18a7f 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.24.0-rc1
\ No newline at end of file
+leanprover/lean4:v4.27.0-rc1
\ No newline at end of file