4. Disjoint Access Structure🔗

From previous sections import AccessStructure and SecretSharing Scheme

import SecretSharingScheme.Section_1_Access_Structure
import SecretSharingScheme.Section_2_Secret_Sharing_Sche

section DisjointAccessStructure

open AccessStructure

open BigOperators
open Classical
variable {n : ℕ} {p : ℕ} [Fact p.Prime]


/--
A share is an optional value in ZMod p.
If the participant is not in any qualified set, it is none.
-/
def Share (p : ℕ) := Option (ZMod p)

/--
The validity of a sharing of a secret S with respect to the disjoint qualified sets Qs.
-/
def IsValidSharing (Qs : Set (Set (Fin n))) (S : ZMod p) (σ : Fin n → Share p) : Prop :=
  -- 1. Participants not in any Q ∈ Qs have no share.
  (∀ i, (∀ Q ∈ Qs, i ∉ Q) → σ i = none) ∧
  -- 2. Participants in some Q ∈ Qs have a share.
  (∀ Q ∈ Qs, ∀ i ∈ Q, (σ i).isSome) ∧
  -- 3. For each Q ∈ Qs, the sum of shares is S.
  (∀ Q ∈ Qs, (∑ i : Fin n, if i ∈ Q then ((σ i).getD 0) else 0) = S)

/--
Generate shares for a secret S using random values ρ.
For each Q ∈ Qs, we use the max element to balance the sum.
-/
noncomputable def GenerateShares (Qs : Set (Set (Fin n))) (S : ZMod p) (ρ : Fin n → ZMod p) : Fin n → Share p := fun i =>
  if h : ∃ Q ∈ Qs, i ∈ Q then
    let Q := Classical.choose h
    have hQ_spec : Q ∈ Qs ∧ i ∈ Q := Classical.choose_spec h
    have h_finite : Q.Finite := Set.toFinite Q
    let Q_finset := h_finite.toFinset
    have h_nonempty : Q_finset.Nonempty := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))S:ZMod pρ:Fin n → ZMod pi:Fin nh:∃ Q ∈ Qs, i ∈ QQ:Set (Fin n) := choose hhQ_spec:Q ∈ Qs ∧ i ∈ Qh_finite:Q.FiniteQ_finset:Finset (Fin n) := h_finite.toFinset⊢ Q_finset.Nonempty
      rw [Set.Finite.toFinset_nonempty]n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))S:ZMod pρ:Fin n → ZMod pi:Fin nh:∃ Q ∈ Qs, i ∈ QQ:Set (Fin n) := choose hhQ_spec:Q ∈ Qs ∧ i ∈ Qh_finite:Q.FiniteQ_finset:Finset (Fin n) := h_finite.toFinset⊢ Q.Nonempty
      exact ⟨i, hQ_spec.2⟩All goals completed! 🐙
    let last := Q_finset.max' h_nonempty
    if i = last then
      -- Sum of random values assigned to other members of Q
      let others := Q_finset.erase last
      let sum_others := ∑ j ∈ others, ρ j
      some (S - sum_others)
    else
      some (ρ i)
  else
    none

/--
Reconstruct the secret from a set of participants G and their shares.
If G contains a qualified set Q, we sum the shares of Q.
-/
noncomputable def ReconstructSecret (Qs : Set (Set (Fin n))) (shares : Fin n → Share p) (G : Set (Fin n)) : Option (ZMod p) :=
  if h : ∃ Q ∈ Qs, Q ⊆ G then
    let Q := Classical.choose h
    -- We sum the shares of members of Q.
    -- We assume shares are present (if not, getD 0 will return 0, which might be wrong, but for valid shares it's fine).
    let sum_shares := ∑ i ∈ (Set.toFinite Q).toFinset, (shares i).getD 0
    some sum_shares
  else
    none

/-
Definition of pivot: selects an element in Q \ A to adjust if the last element is in A.
-/
noncomputable def pivot (Q : Set (Fin n)) (A : Set (Fin n)) : Option (Fin n) :=
  if hQ : Q.Nonempty then
    let last := (Set.toFinite Q).toFinset.max' ((Set.toFinite Q).toFinset_nonempty.mpr hQ)
    if last ∈ A then
      if h_diff : ∃ x, x ∈ Q ∧ x ∉ A then
        some (Classical.choose h_diff)
      else
        none
    else
      none
  else
    none

/-
Definition of shift: the adjustment vector for the random tape.
-/
noncomputable def shift (Qs : Set (Set (Fin n))) (A : Set (Fin n)) (S1 S2 : ZMod p) (i : Fin n) : ZMod p :=
--  S2 - S1
  if _h : ∃ Q ∈ Qs, pivot Q A = some i then
    S2 - S1
  else
    0

/-
Lemma: pivot returns some value iff the last element of Q is in A.
-/
theorem pivot_spec {Q : Set (Fin n)} {A : Set (Fin n)} (hQ : Q.Nonempty) (h_unauth : ¬(Q ⊆ A)) :
  (pivot Q A).isSome ↔ ((Set.toFinite Q).toFinset.max' ((Set.toFinite Q).toFinset_nonempty.mpr hQ)) ∈ A := byn:ℕQ:Set (Fin n)A:Set (Fin n)hQ:Q.Nonemptyh_unauth:¬Q ⊆ A⊢ (pivot Q A).isSome = true ↔ ⋯.toFinset.max' ⋯ ∈ A
    unfold pivotn:ℕQ:Set (Fin n)A:Set (Fin n)hQ:Q.Nonemptyh_unauth:¬Q ⊆ A⊢ (if hQ : Q.Nonempty then
        have last := ⋯.toFinset.max' ⋯;
        if last ∈ A then if h_diff : ∃ x ∈ Q, x ∉ A then some (choose h_diff) else none else none
      else none).isSome =
    true ↔
  ⋯.toFinset.max' ⋯ ∈ A;
    split_ifsposn:ℕQ:Set (Fin n)A:Set (Fin n)hQ:Q.Nonemptyh_unauth:¬Q ⊆ Ah✝:∃ x ∈ Q, x ∉ A⊢ (have last := ⋯.toFinset.max' ⋯;
      if last ∈ A then some (choose h✝) else none).isSome =
    true ↔
  ⋯.toFinset.max' ⋯ ∈ Anegn:ℕQ:Set (Fin n)A:Set (Fin n)hQ:Q.Nonemptyh_unauth:¬Q ⊆ Ah✝:¬∃ x ∈ Q, x ∉ A⊢ (have last := ⋯.toFinset.max' ⋯;
      if last ∈ A then none else none).isSome =
    true ↔
  ⋯.toFinset.max' ⋯ ∈ A <;>posn:ℕQ:Set (Fin n)A:Set (Fin n)hQ:Q.Nonemptyh_unauth:¬Q ⊆ Ah✝:∃ x ∈ Q, x ∉ A⊢ (have last := ⋯.toFinset.max' ⋯;
      if last ∈ A then some (choose h✝) else none).isSome =
    true ↔
  ⋯.toFinset.max' ⋯ ∈ Anegn:ℕQ:Set (Fin n)A:Set (Fin n)hQ:Q.Nonemptyh_unauth:¬Q ⊆ Ah✝:¬∃ x ∈ Q, x ∉ A⊢ (have last := ⋯.toFinset.max' ⋯;
      if last ∈ A then none else none).isSome =
    true ↔
  ⋯.toFinset.max' ⋯ ∈ A simp_all +decide [ Set.subset_def ]All goals completed! 🐙

/-
Lemma: if pivot returns x, then x is in Q, not in A, and not the last element.
-/
theorem pivot_mem {Q : Set (Fin n)} {A : Set (Fin n)} (hQ : Q.Nonempty) (x : Fin n) :
  pivot Q A = some x → x ∈ Q ∧ x ∉ A ∧ x ≠ (Set.toFinite Q).toFinset.max' ((Set.toFinite Q).toFinset_nonempty.mpr hQ) := byn:ℕQ:Set (Fin n)A:Set (Fin n)hQ:Q.Nonemptyx:Fin n⊢ pivot Q A = some x → x ∈ Q ∧ x ∉ A ∧ x ≠ ⋯.toFinset.max' ⋯
    intros hxn:ℕQ:Set (Fin n)A:Set (Fin n)hQ:Q.Nonemptyx:Fin nhx:pivot Q A = some x⊢ x ∈ Q ∧ x ∉ A ∧ x ≠ ⋯.toFinset.max' ⋯;
    unfold pivot at hxn:ℕQ:Set (Fin n)A:Set (Fin n)hQ:Q.Nonemptyx:Fin nhx:(if hQ : Q.Nonempty then
    have last := ⋯.toFinset.max' ⋯;
    if last ∈ A then if h_diff : ∃ x ∈ Q, x ∉ A then some (choose h_diff) else none else none
  else none) =
  some x⊢ x ∈ Q ∧ x ∉ A ∧ x ≠ ⋯.toFinset.max' ⋯;
    split_ifs at hxposn:ℕQ:Set (Fin n)A:Set (Fin n)hQ:Q.Nonemptyx:Fin nh✝:∃ x ∈ Q, x ∉ Ahx:(have last := ⋯.toFinset.max' ⋯;
  if last ∈ A then some (choose h✝) else none) =
  some x⊢ x ∈ Q ∧ x ∉ A ∧ x ≠ ⋯.toFinset.max' ⋯negn:ℕQ:Set (Fin n)A:Set (Fin n)hQ:Q.Nonemptyx:Fin nh✝:¬∃ x ∈ Q, x ∉ Ahx:(have last := ⋯.toFinset.max' ⋯;
  if last ∈ A then none else none) =
  some x⊢ x ∈ Q ∧ x ∉ A ∧ x ≠ ⋯.toFinset.max' ⋯ ;
    ·posn:ℕQ:Set (Fin n)A:Set (Fin n)hQ:Q.Nonemptyx:Fin nh✝:∃ x ∈ Q, x ∉ Ahx:(have last := ⋯.toFinset.max' ⋯;
  if last ∈ A then some (choose h✝) else none) =
  some x⊢ x ∈ Q ∧ x ∉ A ∧ x ≠ ⋯.toFinset.max' ⋯ simp_all [ Finset.max'_eq_sup' ]posn:ℕQ:Set (Fin n)A:Set (Fin n)hQ:Q.Nonemptyx:Fin nh✝:∃ x ∈ Q, x ∉ Ahx:(Q.toFinset.sup' ⋯ fun x => x) ∈ A ∧ choose h✝ = x⊢ x ∈ Q ∧ x ∉ A ∧ ¬x = Q.toFinset.sup' ⋯ fun x => x;
      ·posn:ℕQ:Set (Fin n)A:Set (Fin n)hQ:Q.Nonemptyx:Fin nh✝:∃ x ∈ Q, x ∉ Ahx:(Q.toFinset.sup' ⋯ fun x => x) ∈ A ∧ choose h✝ = x⊢ x ∈ Q ∧ x ∉ A ∧ ¬x = Q.toFinset.sup' ⋯ fun x => x have := Classical.choose_spec ‹∃ x ∈ Q, x∉A›posn:ℕQ:Set (Fin n)A:Set (Fin n)hQ:Q.Nonemptyx:Fin nh✝:∃ x ∈ Q, x ∉ Ahx:(Q.toFinset.sup' ⋯ fun x => x) ∈ A ∧ choose h✝ = xthis:choose h✝ ∈ Q ∧ choose h✝ ∉ A⊢ x ∈ Q ∧ x ∉ A ∧ ¬x = Q.toFinset.sup' ⋯ fun x => x;
        aesopAll goals completed! 🐙;
    ·negn:ℕQ:Set (Fin n)A:Set (Fin n)hQ:Q.Nonemptyx:Fin nh✝:¬∃ x ∈ Q, x ∉ Ahx:(have last := ⋯.toFinset.max' ⋯;
  if last ∈ A then none else none) =
  some x⊢ x ∈ Q ∧ x ∉ A ∧ x ≠ ⋯.toFinset.max' ⋯ grindAll goals completed! 🐙

/-
Lemma: The shift vector is zero for any participant in the unauthorized set A.
-/
theorem shift_eq_zero_on_A {Qs : Set (Set (Fin n))} {A : Set (Fin n)} {S1 S2 : ZMod p}
    (_h_disjoint : Qs.PairwiseDisjoint id)
    (h_nonempty : ∀ Q ∈ Qs, Q.Nonempty)
    (i : Fin n) (hi : i ∈ A) :
    shift Qs A S1 S2 i = 0 := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod p_h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyi:Fin nhi:i ∈ A⊢ shift Qs A S1 S2 i = 0
  unfold shiftn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod p_h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyi:Fin nhi:i ∈ A⊢ (if _h : ∃ Q ∈ Qs, pivot Q A = some i then S2 - S1 else 0) = 0

  split_ifs with hposn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod p_h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyi:Fin nhi:i ∈ Ah:∃ Q ∈ Qs, pivot Q A = some i⊢ S2 - S1 = 0negn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod p_h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyi:Fin nhi:i ∈ Ah:¬∃ Q ∈ Qs, pivot Q A = some i⊢ 0 = 0
  ·posn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod p_h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyi:Fin nhi:i ∈ Ah:∃ Q ∈ Qs, pivot Q A = some i⊢ S2 - S1 = 0 obtain ⟨Q, hQ, h_pivot⟩ := hposn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod p_h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyi:Fin nhi:i ∈ AQ:Set (Fin n)hQ:Q ∈ Qsh_pivot:pivot Q A = some i⊢ S2 - S1 = 0
    -- pivot Q A = some i implies i ∉ A
    have := pivot_mem (h_nonempty Q hQ) i h_pivotposn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod p_h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyi:Fin nhi:i ∈ AQ:Set (Fin n)hQ:Q ∈ Qsh_pivot:pivot Q A = some ithis:i ∈ Q ∧ i ∉ A ∧ i ≠ ⋯.toFinset.max' ⋯⊢ S2 - S1 = 0
    have hi_not_A := this.2.1posn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod p_h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyi:Fin nhi:i ∈ AQ:Set (Fin n)hQ:Q ∈ Qsh_pivot:pivot Q A = some ithis:i ∈ Q ∧ i ∉ A ∧ i ≠ ⋯.toFinset.max' ⋯hi_not_A:i ∉ A⊢ S2 - S1 = 0
    contradictionAll goals completed! 🐙
  ·negn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod p_h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyi:Fin nhi:i ∈ Ah:¬∃ Q ∈ Qs, pivot Q A = some i⊢ 0 = 0 rflAll goals completed! 🐙

/-
Lemma: For a qualified set Q where the last element is in A, the sum of shifts on the other elements is S2 - S1.
-/
theorem sum_shift_eq_diff {Qs : Set (Set (Fin n))} {A : Set (Fin n)} {S1 S2 : ZMod p}
    (h_disjoint : Qs.PairwiseDisjoint id)
    (h_nonempty : ∀ Q ∈ Qs, Q.Nonempty)
    (h_unauth : ∀ Q ∈ Qs, ¬(Q ⊆ A))
    (Q : Set (Fin n)) (hQ : Q ∈ Qs)
    (last : Fin n) (h_last : last = (Set.toFinite Q).toFinset.max' ((Set.toFinite Q).toFinset_nonempty.mpr (h_nonempty Q hQ)))
    (h_last_in_A : last ∈ A) :
    ∑ j ∈ (Set.toFinite Q).toFinset.erase last, shift Qs A S1 S2 j = S2 - S1 := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ AQ:Set (Fin n)hQ:Q ∈ Qslast:Fin nh_last:last = ⋯.toFinset.max' ⋯h_last_in_A:last ∈ A⊢ ∑ j ∈ ⋯.toFinset.erase last, shift Qs A S1 S2 j = S2 - S1
  -- The sum has only one non-zero term, corresponding to the pivot.
  -- pivot Q A is some x, with x ∈ Q \ A.
  -- Since last ∈ A, x ≠ last.
  -- So x ∈ (Q \ {last}).
  -- Also shift is zero everywhere else in Q (because Qs are disjoint).
  have h_shift_def : ∀ j ∈ (Set.toFinite Q).toFinset.erase last, shift Qs A S1 S2 j = if pivot Q A = some j then S2 - S1 else 0 := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ AQ:Set (Fin n)hQ:Q ∈ Qslast:Fin nh_last:last = ⋯.toFinset.max' ⋯h_last_in_A:last ∈ A⊢ ∑ j ∈ ⋯.toFinset.erase last, shift Qs A S1 S2 j = S2 - S1
    intro j hjn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ AQ:Set (Fin n)hQ:Q ∈ Qslast:Fin nh_last:last = ⋯.toFinset.max' ⋯h_last_in_A:last ∈ Aj:Fin nhj:j ∈ ⋯.toFinset.erase last⊢ shift Qs A S1 S2 j = if pivot Q A = some j then S2 - S1 else 0;
    convert if_congr ?_ rfl rflconvert_5n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ AQ:Set (Fin n)hQ:Q ∈ Qslast:Fin nh_last:last = ⋯.toFinset.max' ⋯h_last_in_A:last ∈ Aj:Fin nhj:j ∈ ⋯.toFinset.erase last⊢ (∃ Q ∈ Qs, pivot Q A = some j) ↔ pivot Q A = some j;
    constructorconvert_5.mpn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ AQ:Set (Fin n)hQ:Q ∈ Qslast:Fin nh_last:last = ⋯.toFinset.max' ⋯h_last_in_A:last ∈ Aj:Fin nhj:j ∈ ⋯.toFinset.erase last⊢ (∃ Q ∈ Qs, pivot Q A = some j) → pivot Q A = some jconvert_5.mprn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ AQ:Set (Fin n)hQ:Q ∈ Qslast:Fin nh_last:last = ⋯.toFinset.max' ⋯h_last_in_A:last ∈ Aj:Fin nhj:j ∈ ⋯.toFinset.erase last⊢ pivot Q A = some j → ∃ Q ∈ Qs, pivot Q A = some j;
    ·convert_5.mpn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ AQ:Set (Fin n)hQ:Q ∈ Qslast:Fin nh_last:last = ⋯.toFinset.max' ⋯h_last_in_A:last ∈ Aj:Fin nhj:j ∈ ⋯.toFinset.erase last⊢ (∃ Q ∈ Qs, pivot Q A = some j) → pivot Q A = some j rintro ⟨ Q', hQ', h ⟩convert_5.mpn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ AQ:Set (Fin n)hQ:Q ∈ Qslast:Fin nh_last:last = ⋯.toFinset.max' ⋯h_last_in_A:last ∈ Aj:Fin nhj:j ∈ ⋯.toFinset.erase lastQ':Set (Fin n)hQ':Q' ∈ Qsh:pivot Q' A = some j⊢ pivot Q A = some j;
      have h_eq : Q' = Q := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ AQ:Set (Fin n)hQ:Q ∈ Qslast:Fin nh_last:last = ⋯.toFinset.max' ⋯h_last_in_A:last ∈ A⊢ ∑ j ∈ ⋯.toFinset.erase last, shift Qs A S1 S2 j = S2 - S1
        have h_eq : j ∈ Q' ∧ j ∈ Q := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ AQ:Set (Fin n)hQ:Q ∈ Qslast:Fin nh_last:last = ⋯.toFinset.max' ⋯h_last_in_A:last ∈ A⊢ ∑ j ∈ ⋯.toFinset.erase last, shift Qs A S1 S2 j = S2 - S1
          have := pivot_mem ( h_nonempty Q' hQ' ) j hn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ AQ:Set (Fin n)hQ:Q ∈ Qslast:Fin nh_last:last = ⋯.toFinset.max' ⋯h_last_in_A:last ∈ Aj:Fin nhj:j ∈ ⋯.toFinset.erase lastQ':Set (Fin n)hQ':Q' ∈ Qsh:pivot Q' A = some jthis:j ∈ Q' ∧ j ∉ A ∧ j ≠ ⋯.toFinset.max' ⋯⊢ j ∈ Q' ∧ j ∈ Q; aesopAll goals completed! 🐙;
        have := h_disjoint hQ' hQn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ AQ:Set (Fin n)hQ:Q ∈ Qslast:Fin nh_last:last = ⋯.toFinset.max' ⋯h_last_in_A:last ∈ Aj:Fin nhj:j ∈ ⋯.toFinset.erase lastQ':Set (Fin n)hQ':Q' ∈ Qsh:pivot Q' A = some jh_eq:j ∈ Q' ∧ j ∈ Qthis:Q' ≠ Q → Function.onFun Disjoint id Q' Q⊢ Q' = Q;
        exact Classical.not_not.1 fun h => Set.disjoint_left.mp ( this h ) h_eq.1 h_eq.2All goals completed! 🐙;
      aesopAll goals completed! 🐙;
    ·convert_5.mprn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ AQ:Set (Fin n)hQ:Q ∈ Qslast:Fin nh_last:last = ⋯.toFinset.max' ⋯h_last_in_A:last ∈ Aj:Fin nhj:j ∈ ⋯.toFinset.erase last⊢ pivot Q A = some j → ∃ Q ∈ Qs, pivot Q A = some j exact fun h => ⟨ Q, hQ, h ⟩All goals completed! 🐙;
  have h_pivot_def : ∃ x, pivot Q A = some x ∧ x ∈ (Set.toFinite Q).toFinset.erase last := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ AQ:Set (Fin n)hQ:Q ∈ Qslast:Fin nh_last:last = ⋯.toFinset.max' ⋯h_last_in_A:last ∈ A⊢ ∑ j ∈ ⋯.toFinset.erase last, shift Qs A S1 S2 j = S2 - S1
    unfold pivotn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ AQ:Set (Fin n)hQ:Q ∈ Qslast:Fin nh_last:last = ⋯.toFinset.max' ⋯h_last_in_A:last ∈ Ah_shift_def:∀ j ∈ ⋯.toFinset.erase last, shift Qs A S1 S2 j = if pivot Q A = some j then S2 - S1 else 0⊢ ∃ x,
  (if hQ : Q.Nonempty then
        have last := ⋯.toFinset.max' ⋯;
        if last ∈ A then if h_diff : ∃ x ∈ Q, x ∉ A then some (choose h_diff) else none else none
      else none) =
      some x ∧
    x ∈ ⋯.toFinset.erase last;
    simp_all +decide [ Set.not_subset ]n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth✝:∀ Q ∈ Qs, ¬Q ⊆ AQ:Set (Fin n)hQ:Q ∈ Qslast:Fin nh_unauth:∀ Q ∈ Qs, ∃ a ∈ Q, a ∉ Ah_last:last = Q.toFinset.max' ⋯h_last_in_A:Q.toFinset.max' ⋯ ∈ Ah_shift_def:∀ (j : Fin n), ¬j = Q.toFinset.max' ⋯ → j ∈ Q → shift Qs A S1 S2 j = if pivot Q A = some j then S2 - S1 else 0⊢ ¬choose ⋯ = Q.toFinset.max' ⋯ ∧ choose ⋯ ∈ Q;
    exact ⟨ fun h => Classical.choose_spec ( h_unauth Q hQ ) |>.2 <| h ▸ h_last_in_A, Classical.choose_spec ( h_unauth Q hQ ) |>.1 ⟩All goals completed! 🐙;
  obtain ⟨ x, hx₁, hx₂ ⟩ := h_pivot_defn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ AQ:Set (Fin n)hQ:Q ∈ Qslast:Fin nh_last:last = ⋯.toFinset.max' ⋯h_last_in_A:last ∈ Ah_shift_def:∀ j ∈ ⋯.toFinset.erase last, shift Qs A S1 S2 j = if pivot Q A = some j then S2 - S1 else 0x:Fin nhx₁:pivot Q A = some xhx₂:x ∈ ⋯.toFinset.erase last⊢ ∑ j ∈ ⋯.toFinset.erase last, shift Qs A S1 S2 j = S2 - S1;
  rw [ Finset.sum_eq_single x ]n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ AQ:Set (Fin n)hQ:Q ∈ Qslast:Fin nh_last:last = ⋯.toFinset.max' ⋯h_last_in_A:last ∈ Ah_shift_def:∀ j ∈ ⋯.toFinset.erase last, shift Qs A S1 S2 j = if pivot Q A = some j then S2 - S1 else 0x:Fin nhx₁:pivot Q A = some xhx₂:x ∈ ⋯.toFinset.erase last⊢ shift Qs A S1 S2 x = S2 - S1h₀n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ AQ:Set (Fin n)hQ:Q ∈ Qslast:Fin nh_last:last = ⋯.toFinset.max' ⋯h_last_in_A:last ∈ Ah_shift_def:∀ j ∈ ⋯.toFinset.erase last, shift Qs A S1 S2 j = if pivot Q A = some j then S2 - S1 else 0x:Fin nhx₁:pivot Q A = some xhx₂:x ∈ ⋯.toFinset.erase last⊢ ∀ b ∈ ⋯.toFinset.erase last, b ≠ x → shift Qs A S1 S2 b = 0h₁n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ AQ:Set (Fin n)hQ:Q ∈ Qslast:Fin nh_last:last = ⋯.toFinset.max' ⋯h_last_in_A:last ∈ Ah_shift_def:∀ j ∈ ⋯.toFinset.erase last, shift Qs A S1 S2 j = if pivot Q A = some j then S2 - S1 else 0x:Fin nhx₁:pivot Q A = some xhx₂:x ∈ ⋯.toFinset.erase last⊢ x ∉ ⋯.toFinset.erase last → shift Qs A S1 S2 x = 0 <;>n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ AQ:Set (Fin n)hQ:Q ∈ Qslast:Fin nh_last:last = ⋯.toFinset.max' ⋯h_last_in_A:last ∈ Ah_shift_def:∀ j ∈ ⋯.toFinset.erase last, shift Qs A S1 S2 j = if pivot Q A = some j then S2 - S1 else 0x:Fin nhx₁:pivot Q A = some xhx₂:x ∈ ⋯.toFinset.erase last⊢ shift Qs A S1 S2 x = S2 - S1h₀n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ AQ:Set (Fin n)hQ:Q ∈ Qslast:Fin nh_last:last = ⋯.toFinset.max' ⋯h_last_in_A:last ∈ Ah_shift_def:∀ j ∈ ⋯.toFinset.erase last, shift Qs A S1 S2 j = if pivot Q A = some j then S2 - S1 else 0x:Fin nhx₁:pivot Q A = some xhx₂:x ∈ ⋯.toFinset.erase last⊢ ∀ b ∈ ⋯.toFinset.erase last, b ≠ x → shift Qs A S1 S2 b = 0h₁n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ AQ:Set (Fin n)hQ:Q ∈ Qslast:Fin nh_last:last = ⋯.toFinset.max' ⋯h_last_in_A:last ∈ Ah_shift_def:∀ j ∈ ⋯.toFinset.erase last, shift Qs A S1 S2 j = if pivot Q A = some j then S2 - S1 else 0x:Fin nhx₁:pivot Q A = some xhx₂:x ∈ ⋯.toFinset.erase last⊢ x ∉ ⋯.toFinset.erase last → shift Qs A S1 S2 x = 0 aesopAll goals completed! 🐙

/-
Lemma: shift(S2, S1) is the negation of shift(S1, S2).
-/
theorem shift_symm {Qs : Set (Set (Fin n))} {A : Set (Fin n)} {S1 S2 : ZMod p} :
    shift Qs A S2 S1 = - shift Qs A S1 S2 := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod p⊢ shift Qs A S2 S1 = -shift Qs A S1 S2
      -- By definition of shift, we have that shift Qs A S2 S1 i = S2 - S1 if there exists a Q in Qs such that pivot Q A is some i, otherwise 0.
      funext ihn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod pi:Fin n⊢ shift Qs A S2 S1 i = (-shift Qs A S1 S2) i; simp [shift]hn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod pi:Fin n⊢ (if ∃ Q ∈ Qs, pivot Q A = some i then S1 - S2 else 0) = -if ∃ Q ∈ Qs, pivot Q A = some i then S2 - S1 else 0;
      split_ifsposn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod pi:Fin nh✝:∃ Q ∈ Qs, pivot Q A = some i⊢ S1 - S2 = -(S2 - S1)negn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod pi:Fin nh✝:¬∃ Q ∈ Qs, pivot Q A = some i⊢ 0 = -0 <;>posn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod pi:Fin nh✝:∃ Q ∈ Qs, pivot Q A = some i⊢ S1 - S2 = -(S2 - S1)negn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod pi:Fin nh✝:¬∃ Q ∈ Qs, pivot Q A = some i⊢ 0 = -0 ringAll goals completed! 🐙

/-
Lemma: The generated shares for S2 using the shifted random tape are the same as for S1 using the original tape, for participants in A.
-/
theorem generateShares_shift_eq {Qs : Set (Set (Fin n))} {A : Set (Fin n)} {S1 S2 : ZMod p}
    (h_disjoint : Qs.PairwiseDisjoint id)
    (h_nonempty : ∀ Q ∈ Qs, Q.Nonempty)
    (h_unauth : ∀ Q ∈ Qs, ¬(Q ⊆ A))
    (ρ : Fin n → ZMod p)
    (i : Fin n) (hi : i ∈ A) :
    GenerateShares Qs S2 (ρ + shift Qs A S1 S2) i =
    GenerateShares Qs S1 ρ i := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ A⊢ GenerateShares Qs S2 (ρ + shift Qs A S1 S2) i = GenerateShares Qs S1 ρ i
  -- By definition of GenerateShares, we need to consider three cases: when Q contains i, when Q does not contain i, and when Q is not in Qs.
  by_cases hQ : ∃ Q ∈ Qs, i ∈ Qposn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Q⊢ GenerateShares Qs S2 (ρ + shift Qs A S1 S2) i = GenerateShares Qs S1 ρ inegn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:¬∃ Q ∈ Qs, i ∈ Q⊢ GenerateShares Qs S2 (ρ + shift Qs A S1 S2) i = GenerateShares Qs S1 ρ i;
  ·posn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Q⊢ GenerateShares Qs S2 (ρ + shift Qs A S1 S2) i = GenerateShares Qs S1 ρ i -- Since $i \in A$, we have $shift Qs A S1 S2 i = 0$ by definition of shift.
    have h_shift_zero : shift Qs A S1 S2 i = 0 := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ A⊢ GenerateShares Qs S2 (ρ + shift Qs A S1 S2) i = GenerateShares Qs S1 ρ i
      exact shift_eq_zero_on_A h_disjoint h_nonempty i hiAll goals completed! 🐙;
    -- Since $shift Qs A S1 S2 i = 0$, adding it to $\rho$ does not change the value.
    simp [h_shift_zero, GenerateShares]posn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0⊢ (if h : ∃ Q ∈ Qs, i ∈ Q then
    if i = (choose ⋯).toFinset.max' ⋯ then
      some (S2 - ∑ x ∈ (choose ⋯).toFinset.erase ((choose ⋯).toFinset.max' ⋯), (ρ x + shift Qs A S1 S2 x))
    else some (ρ i)
  else none) =
  if h : ∃ Q ∈ Qs, i ∈ Q then
    if i = (choose ⋯).toFinset.max' ⋯ then some (S1 - ∑ x ∈ (choose ⋯).toFinset.erase ((choose ⋯).toFinset.max' ⋯), ρ x)
    else some (ρ i)
  else none;
    split_ifsposn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:i = (choose ⋯).toFinset.max' ⋯⊢ some (S2 - ∑ x ∈ (choose ⋯).toFinset.erase ((choose ⋯).toFinset.max' ⋯), (ρ x + shift Qs A S1 S2 x)) =
  some (S1 - ∑ x ∈ (choose ⋯).toFinset.erase ((choose ⋯).toFinset.max' ⋯), ρ x)negn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:¬i = (choose ⋯).toFinset.max' ⋯⊢ some (ρ i) = some (ρ i) <;>posn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:i = (choose ⋯).toFinset.max' ⋯⊢ some (S2 - ∑ x ∈ (choose ⋯).toFinset.erase ((choose ⋯).toFinset.max' ⋯), (ρ x + shift Qs A S1 S2 x)) =
  some (S1 - ∑ x ∈ (choose ⋯).toFinset.erase ((choose ⋯).toFinset.max' ⋯), ρ x)negn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:¬i = (choose ⋯).toFinset.max' ⋯⊢ some (ρ i) = some (ρ i) simp [ Finset.sum_add_distrib ]All goals completed! 🐙;
    convert sum_shift_eq_diff h_disjoint h_nonempty h_unauth _ _ _ rfl using 1an:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:i = (choose ⋯).toFinset.max' ⋯⊢ some
      (S2 -
        (∑ x ∈ (choose ⋯).toFinset.erase ((choose ⋯).toFinset.max' ⋯), ρ x +
          ∑ x ∈ (choose ⋯).toFinset.erase ((choose ⋯).toFinset.max' ⋯), shift Qs A S1 S2 x)) =
    some (S1 - ∑ x ∈ (choose ⋯).toFinset.erase ((choose ⋯).toFinset.max' ⋯), ρ x) ↔
  ⋯.toFinset.max' ⋯ ∈ A →
    ∑ j ∈ ⋯.toFinset.erase (⋯.toFinset.max' ⋯), shift Qs A ?pos.convert_3✝ ?pos.convert_4✝ j =
      ?pos.convert_4✝ - ?pos.convert_3✝pos.convert_1n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:i = (choose ⋯).toFinset.max' ⋯⊢ ℕpos.convert_2n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:i = (choose ⋯).toFinset.max' ⋯⊢ Fact (Nat.Prime ?pos.convert_1✝)pos.convert_3n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:i = (choose ⋯).toFinset.max' ⋯⊢ ZMod ?pos.convert_1✝pos.convert_4n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:i = (choose ⋯).toFinset.max' ⋯⊢ ZMod ?pos.convert_1✝pos.convert_5n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:i = (choose ⋯).toFinset.max' ⋯⊢ Set (Fin n)pos.convert_6n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:i = (choose ⋯).toFinset.max' ⋯⊢ ?pos.convert_5✝ ∈ Qs;
    rotate_leftpos.convert_1n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:i = (choose ⋯).toFinset.max' ⋯⊢ ℕpos.convert_2n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:i = (choose ⋯).toFinset.max' ⋯⊢ Fact (Nat.Prime ?pos.convert_1✝)pos.convert_3n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:i = (choose ⋯).toFinset.max' ⋯⊢ ZMod ?pos.convert_1✝pos.convert_4n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:i = (choose ⋯).toFinset.max' ⋯⊢ ZMod ?pos.convert_1✝pos.convert_5n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:i = (choose ⋯).toFinset.max' ⋯⊢ Set (Fin n)pos.convert_6n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:i = (choose ⋯).toFinset.max' ⋯⊢ ?pos.convert_5✝ ∈ Qsan:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:i = (choose ⋯).toFinset.max' ⋯⊢ some
      (S2 -
        (∑ x ∈ (choose ⋯).toFinset.erase ((choose ⋯).toFinset.max' ⋯), ρ x +
          ∑ x ∈ (choose ⋯).toFinset.erase ((choose ⋯).toFinset.max' ⋯), shift Qs A S1 S2 x)) =
    some (S1 - ∑ x ∈ (choose ⋯).toFinset.erase ((choose ⋯).toFinset.max' ⋯), ρ x) ↔
  ⋯.toFinset.max' ⋯ ∈ A →
    ∑ j ∈ ⋯.toFinset.erase (⋯.toFinset.max' ⋯), shift Qs A ?pos.convert_3✝ ?pos.convert_4✝ j =
      ?pos.convert_4✝ - ?pos.convert_3✝;
    ·pos.convert_1n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:i = (choose ⋯).toFinset.max' ⋯⊢ ℕ exact pAll goals completed! 🐙;
    ·pos.convert_2n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:i = (choose ⋯).toFinset.max' ⋯⊢ Fact (Nat.Prime ?pos.convert_1✝) exact ⟨ Fact.out ⟩All goals completed! 🐙;
    ·pos.convert_3n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:i = (choose ⋯).toFinset.max' ⋯⊢ ZMod ?pos.convert_1✝ exact S1All goals completed! 🐙;
    ·pos.convert_4n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:i = (choose ⋯).toFinset.max' ⋯⊢ ZMod ?pos.convert_1✝ exact S2All goals completed! 🐙;
    ·pos.convert_5n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:i = (choose ⋯).toFinset.max' ⋯⊢ Set (Fin n) exact Classical.choose hQAll goals completed! 🐙;
    ·pos.convert_6n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:i = (choose ⋯).toFinset.max' ⋯⊢ ?pos.convert_5✝ ∈ Qs exact Classical.choose_spec hQ |>.1All goals completed! 🐙;
    simp +decide [ ← ‹i = _›]an:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:∃ Q ∈ Qs, i ∈ Qh_shift_zero:shift Qs A S1 S2 i = 0h✝:i = (choose ⋯).toFinset.max' ⋯⊢ some (S2 - (∑ x ∈ (choose ⋯).toFinset.erase i, ρ x + ∑ x ∈ (choose ⋯).toFinset.erase i, shift Qs A S1 S2 x)) =
    some (S1 - ∑ x ∈ (choose ⋯).toFinset.erase i, ρ x) ↔
  i ∈ A → ∑ x ∈ (choose hQ).toFinset.erase i, shift Qs A S1 S2 x = S2 - S1;
    grindAll goals completed! 🐙;
  ·negn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Aρ:Fin n → ZMod pi:Fin nhi:i ∈ AhQ:¬∃ Q ∈ Qs, i ∈ Q⊢ GenerateShares Qs S2 (ρ + shift Qs A S1 S2) i = GenerateShares Qs S1 ρ i -- Since there's no Q in Qs containing i, by definition of GenerateShares, both shares should be none. So, the equality holds trivially because both sides are none.
    simp [GenerateShares, hQ]All goals completed! 🐙



/-
Lemma: The shift map is a bijection.
-/
theorem shift_is_bijection {Qs : Set (Set (Fin n))} {A : Set (Fin n)} {S1 S2 : ZMod p}
    (h_disjoint : Qs.PairwiseDisjoint id)
    (h_nonempty : ∀ Q ∈ Qs, Q.Nonempty)
    (h_unauth : ∀ Q ∈ Qs, ¬(Q ⊆ A))
    (shares_A : ∀ i : Fin n, i ∈ A → Share p) :
    Set.BijOn (fun ρ => ρ + shift Qs A S1 S2)
      {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}
      {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi} := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share p⊢ Set.BijOn (fun ρ => ρ + shift Qs A S1 S2) {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}
  {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi}
        refine' ⟨ fun ρ hρ i hi => _, _, _ ⟩refine'_1n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share pρ:Fin n → ZMod phρ:ρ ∈ {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}i:Fin nhi:i ∈ A⊢ GenerateShares Qs S2 ((fun ρ => ρ + shift Qs A S1 S2) ρ) i = shares_A i hirefine'_2n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share p⊢ Set.InjOn (fun ρ => ρ + shift Qs A S1 S2) {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}refine'_3n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share p⊢ Set.SurjOn (fun ρ => ρ + shift Qs A S1 S2) {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}
  {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi};
        ·refine'_1n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share pρ:Fin n → ZMod phρ:ρ ∈ {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}i:Fin nhi:i ∈ A⊢ GenerateShares Qs S2 ((fun ρ => ρ + shift Qs A S1 S2) ρ) i = shares_A i hi convert generateShares_shift_eq h_disjoint h_nonempty h_unauth ρ i hi using 1h.e'_3n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share pρ:Fin n → ZMod phρ:ρ ∈ {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}i:Fin nhi:i ∈ A⊢ shares_A i hi = GenerateShares Qs S1 ρ i;
          exact hρ i hi ▸ rflAll goals completed! 🐙;
        ·refine'_2n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share p⊢ Set.InjOn (fun ρ => ρ + shift Qs A S1 S2) {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi} exact fun x hx y hy hxy => byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share px:Fin n → ZMod phx:x ∈ {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}y:Fin n → ZMod phy:y ∈ {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}hxy:(fun ρ => ρ + shift Qs A S1 S2) x = (fun ρ => ρ + shift Qs A S1 S2) y⊢ x = y simpa using hxyAll goals completed! 🐙;
        ·refine'_3n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share p⊢ Set.SurjOn (fun ρ => ρ + shift Qs A S1 S2) {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}
  {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi} intro ρ hρrefine'_3n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share pρ:Fin n → ZMod phρ:ρ ∈ {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi}⊢ ρ ∈ (fun ρ => ρ + shift Qs A S1 S2) '' {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi};
          refine' ⟨ ρ - shift Qs A S1 S2, _, _ ⟩refine'_3.refine'_1n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share pρ:Fin n → ZMod phρ:ρ ∈ {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi}⊢ ρ - shift Qs A S1 S2 ∈ {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}refine'_3.refine'_2n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share pρ:Fin n → ZMod phρ:ρ ∈ {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi}⊢ (fun ρ => ρ + shift Qs A S1 S2) (ρ - shift Qs A S1 S2) = ρ <;>refine'_3.refine'_1n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share pρ:Fin n → ZMod phρ:ρ ∈ {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi}⊢ ρ - shift Qs A S1 S2 ∈ {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}refine'_3.refine'_2n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share pρ:Fin n → ZMod phρ:ρ ∈ {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi}⊢ (fun ρ => ρ + shift Qs A S1 S2) (ρ - shift Qs A S1 S2) = ρ simp_all +decide [ sub_eq_add_neg ]All goals completed! 🐙;
          convert generateShares_shift_eq h_disjoint h_nonempty h_unauth ( ρ + -shift Qs A S1 S2 ) using 1h.an:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share pρ:Fin n → ZMod phρ:∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hia✝:Fin n⊢ (∀ (hi : a✝ ∈ A), GenerateShares Qs S1 (ρ + -shift Qs A S1 S2) a✝ = shares_A a✝ hi) ↔
  a✝ ∈ A →
    GenerateShares Qs ?refine'_3.refine'_1.convert_2
        (ρ + -shift Qs A S1 S2 + shift Qs A ?refine'_3.refine'_1.convert_1 ?refine'_3.refine'_1.convert_2) a✝ =
      GenerateShares Qs ?refine'_3.refine'_1.convert_1 (ρ + -shift Qs A S1 S2) a✝refine'_3.refine'_1.convert_1n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share pρ:Fin n → ZMod phρ:∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi⊢ ZMod prefine'_3.refine'_1.convert_2n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share pρ:Fin n → ZMod phρ:∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi⊢ ZMod p;
          rotate_leftrefine'_3.refine'_1.convert_1n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share pρ:Fin n → ZMod phρ:∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi⊢ ZMod prefine'_3.refine'_1.convert_2n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share pρ:Fin n → ZMod phρ:∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi⊢ ZMod ph.an:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share pρ:Fin n → ZMod phρ:∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hia✝:Fin n⊢ (∀ (hi : a✝ ∈ A), GenerateShares Qs S1 (ρ + -shift Qs A S1 S2) a✝ = shares_A a✝ hi) ↔
  a✝ ∈ A →
    GenerateShares Qs ?refine'_3.refine'_1.convert_2
        (ρ + -shift Qs A S1 S2 + shift Qs A ?refine'_3.refine'_1.convert_1 ?refine'_3.refine'_1.convert_2) a✝ =
      GenerateShares Qs ?refine'_3.refine'_1.convert_1 (ρ + -shift Qs A S1 S2) a✝;
          ·refine'_3.refine'_1.convert_1n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share pρ:Fin n → ZMod phρ:∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi⊢ ZMod p exact S1All goals completed! 🐙;
          ·refine'_3.refine'_1.convert_2n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share pρ:Fin n → ZMod phρ:∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi⊢ ZMod p exact S2All goals completed! 🐙;
          ·h.an:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share pρ:Fin n → ZMod phρ:∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hia✝:Fin n⊢ (∀ (hi : a✝ ∈ A), GenerateShares Qs S1 (ρ + -shift Qs A S1 S2) a✝ = shares_A a✝ hi) ↔
  a✝ ∈ A →
    GenerateShares Qs ?refine'_3.refine'_1.convert_2
        (ρ + -shift Qs A S1 S2 + shift Qs A ?refine'_3.refine'_1.convert_1 ?refine'_3.refine'_1.convert_2) a✝ =
      GenerateShares Qs ?refine'_3.refine'_1.convert_1 (ρ + -shift Qs A S1 S2) a✝ simp +decide [ ← hρ ]h.an:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)S1:ZMod pS2:ZMod ph_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptyh_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share pρ:Fin n → ZMod phρ:∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hia✝:Fin n⊢ a✝ ∈ A → GenerateShares Qs S1 (ρ + -shift Qs A S1 S2) a✝ = GenerateShares Qs S2 ρ a✝ ↔
  a✝ ∈ A → GenerateShares Qs S2 ρ a✝ = GenerateShares Qs S1 (ρ + -shift Qs A S1 S2) a✝;
            rw [ eq_comm ]All goals completed! 🐙


/-
Perfect security theorem: The number of random tapes consistent with a given set of shares on an unauthorized set is independent of the secret.
-/
theorem PerfectSecurity {n : ℕ} {p : ℕ} [Fact p.Prime]
    (Qs : Set (Set (Fin n)))
    (h_disjoint : Qs.PairwiseDisjoint id)
    (h_nonempty : ∀ Q ∈ Qs, Q.Nonempty)
    (A : Set (Fin n))
    (h_unauth : ∀ Q ∈ Qs, ¬(Q ⊆ A)) -- A is unauthorized
    (shares_A : ∀ i : Fin n, i ∈ A → Share p) -- Fixed shares for A
    (S1 S2 : ZMod p) :
    Set.ncard {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi} =
    Set.ncard {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi} := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyA:Set (Fin n)h_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share pS1:ZMod pS2:ZMod p⊢ {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}.ncard =
  {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi}.ncard
      -- the shift map is a bijection.
      have h_bijection : Set.BijOn (fun ρ => ρ + shift Qs A S1 S2)
        {ρ : Fin n → ZMod p | ∀ i hi, GenerateShares Qs S1 ρ i = shares_A i hi}
        {ρ : Fin n → ZMod p | ∀ i hi, GenerateShares Qs S2 ρ i = shares_A i hi} := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyA:Set (Fin n)h_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share pS1:ZMod pS2:ZMod p⊢ {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}.ncard =
  {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi}.ncard
          exact shift_is_bijection h_disjoint h_nonempty h_unauth shares_AAll goals completed! 🐙
      rw [ Set.ncard_def, Set.ncard_def, Set.encard_congr ( h_bijection.equiv ) ]All goals completed! 🐙

/-
Perfect security theorem
-/
theorem PerfectSecurity_thm {n : ℕ} {p : ℕ} [Fact p.Prime]
    (Qs : Set (Set (Fin n)))
    (h_disjoint : Qs.PairwiseDisjoint id)
    (h_nonempty : ∀ Q ∈ Qs, Q.Nonempty)
    (A : Set (Fin n))
    (h_unauth : ∀ Q ∈ Qs, ¬(Q ⊆ A)) -- A is unauthorized
    (shares_A : ∀ i : Fin n, i ∈ A → Share p) -- Fixed shares for A
    (S1 S2 : ZMod p) :
    Set.ncard {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi} =
    Set.ncard {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi} := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyA:Set (Fin n)h_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share pS1:ZMod pS2:ZMod p⊢ {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}.ncard =
  {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi}.ncard
  have h_bij := shift_is_bijection h_disjoint h_nonempty h_unauth shares_A (S1 := S1) (S2 := S2)n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyA:Set (Fin n)h_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share pS1:ZMod pS2:ZMod ph_bij:Set.BijOn (fun ρ => ρ + shift Qs A S1 S2) {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}
  {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi}⊢ {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}.ncard =
  {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi}.ncard
  rw [← h_bij.image_eq]n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyA:Set (Fin n)h_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → Share pS1:ZMod pS2:ZMod ph_bij:Set.BijOn (fun ρ => ρ + shift Qs A S1 S2) {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}
  {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi}⊢ {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}.ncard =
  ((fun ρ => ρ + shift Qs A S1 S2) '' {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}).ncard
  rw [Set.InjOn.ncard_image h_bij.injOn]All goals completed! 🐙


/-
Helper lemma: The qualified set chosen by GenerateShares is the correct one due to disjointness.
-/
theorem GenerateShares_Q_eq {n : ℕ} {Qs : Set (Set (Fin n))}
    (h_disjoint : Qs.PairwiseDisjoint id)
    {Q : Set (Fin n)} (hQ : Q ∈ Qs)
    {i : Fin n} (hi : i ∈ Q) :
    Classical.choose (show ∃ Q' ∈ Qs, i ∈ Q' from ⟨Q, hQ, hi⟩) = Q := byn:ℕQs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idQ:Set (Fin n)hQ:Q ∈ Qsi:Fin nhi:i ∈ Q⊢ choose ⋯ = Q
  let P := fun Q' => Q' ∈ Qs ∧ i ∈ Q'n:ℕQs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idQ:Set (Fin n)hQ:Q ∈ Qsi:Fin nhi:i ∈ QP:Set (Fin n) → Prop := fun Q' => Q' ∈ Qs ∧ i ∈ Q'⊢ choose ⋯ = Q
  let Q' := Classical.choose (show ∃ Q' ∈ Qs, i ∈ Q' from ⟨Q, hQ, hi⟩)n:ℕQs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idQ:Set (Fin n)hQ:Q ∈ Qsi:Fin nhi:i ∈ QP:Set (Fin n) → Prop := fun Q' => Q' ∈ Qs ∧ i ∈ Q'Q':Set (Fin n) := choose ⋯⊢ choose ⋯ = Q
  have hQ' : Q' ∈ Qs ∧ i ∈ Q' := Classical.choose_spec (show ∃ Q' ∈ Qs, i ∈ Q' from ⟨Q, hQ, hi⟩)n:ℕQs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idQ:Set (Fin n)hQ:Q ∈ Qsi:Fin nhi:i ∈ QP:Set (Fin n) → Prop := fun Q' => Q' ∈ Qs ∧ i ∈ Q'Q':Set (Fin n) := choose ⋯hQ':Q' ∈ Qs ∧ i ∈ Q'⊢ choose ⋯ = Q
  have h_inter : i ∈ Q' ∩ Q := ⟨hQ'.2, hi⟩n:ℕQs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idQ:Set (Fin n)hQ:Q ∈ Qsi:Fin nhi:i ∈ QP:Set (Fin n) → Prop := fun Q' => Q' ∈ Qs ∧ i ∈ Q'Q':Set (Fin n) := choose ⋯hQ':Q' ∈ Qs ∧ i ∈ Q'h_inter:i ∈ Q' ∩ Q⊢ choose ⋯ = Q
  have h_not_disjoint : ¬Disjoint Q' Q := Set.not_disjoint_iff.mpr ⟨i, h_inter⟩n:ℕQs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idQ:Set (Fin n)hQ:Q ∈ Qsi:Fin nhi:i ∈ QP:Set (Fin n) → Prop := fun Q' => Q' ∈ Qs ∧ i ∈ Q'Q':Set (Fin n) := choose ⋯hQ':Q' ∈ Qs ∧ i ∈ Q'h_inter:i ∈ Q' ∩ Qh_not_disjoint:¬Disjoint Q' Q⊢ choose ⋯ = Q
  by_contra h_nen:ℕQs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idQ:Set (Fin n)hQ:Q ∈ Qsi:Fin nhi:i ∈ QP:Set (Fin n) → Prop := fun Q' => Q' ∈ Qs ∧ i ∈ Q'Q':Set (Fin n) := choose ⋯hQ':Q' ∈ Qs ∧ i ∈ Q'h_inter:i ∈ Q' ∩ Qh_not_disjoint:¬Disjoint Q' Qh_ne:¬choose ⋯ = Q⊢ False
  have h_disj := h_disjoint hQ'.1 hQ h_nen:ℕQs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idQ:Set (Fin n)hQ:Q ∈ Qsi:Fin nhi:i ∈ QP:Set (Fin n) → Prop := fun Q' => Q' ∈ Qs ∧ i ∈ Q'Q':Set (Fin n) := choose ⋯hQ':Q' ∈ Qs ∧ i ∈ Q'h_inter:i ∈ Q' ∩ Qh_not_disjoint:¬Disjoint Q' Qh_ne:¬choose ⋯ = Qh_disj:Function.onFun Disjoint id Q' Q⊢ False
  contradictionAll goals completed! 🐙

theorem GenerateShares_isValid {n : ℕ} {p : ℕ} [Fact p.Prime]
    (Qs : Set (Set (Fin n)))
    (h_disjoint : Qs.PairwiseDisjoint id)
    (h_nonempty : ∀ Q ∈ Qs, Q.Nonempty)
    (S : ZMod p) (ρ : Fin n → ZMod p) :
    IsValidSharing Qs S (GenerateShares Qs S ρ) := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod p⊢ IsValidSharing Qs S (GenerateShares Qs S ρ)

  refine ⟨?h1, ?h2, ?h3⟩h1n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod p⊢ ∀ (i : Fin n), (∀ Q ∈ Qs, i ∉ Q) → GenerateShares Qs S ρ i = noneh2n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod p⊢ ∀ Q ∈ Qs, ∀ i ∈ Q, Option.isSome (GenerateShares Qs S ρ i) = trueh3n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod p⊢ ∀ Q ∈ Qs, (∑ i, if i ∈ Q then Option.getD (GenerateShares Qs S ρ i) 0 else 0) = S
  /- 1) Participants not in any Q ∈ Qs get `none`. -/
  ·h1n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod p⊢ ∀ (i : Fin n), (∀ Q ∈ Qs, i ∉ Q) → GenerateShares Qs S ρ i = none intro i hih1n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pi:Fin nhi:∀ Q ∈ Qs, i ∉ Q⊢ GenerateShares Qs S ρ i = none
    -- hi : (∀ Q ∈ Qs, i ∉ Q)
    have hneg : ¬ (∃ Q ∈ Qs, i ∈ Q) := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod p⊢ IsValidSharing Qs S (GenerateShares Qs S ρ)
      intro hexn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pi:Fin nhi:∀ Q ∈ Qs, i ∉ Qhex:∃ Q ∈ Qs, i ∈ Q⊢ False
      rcases hex with ⟨Q, hQ, hiQ⟩n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pi:Fin nhi:∀ Q ∈ Qs, i ∉ QQ:Set (Fin n)hQ:Q ∈ QshiQ:i ∈ Q⊢ False
      exact (hi Q hQ) hiQAll goals completed! 🐙
    -- Now unfold and take the `else` branch
    simp [GenerateShares, hneg]All goals completed! 🐙
  /- 2) Participants in a qualified set get `some _` (i.e. `.isSome`). -/
  ·h2n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod p⊢ ∀ Q ∈ Qs, ∀ i ∈ Q, Option.isSome (GenerateShares Qs S ρ i) = true intro Q hQh2n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ Qs⊢ ∀ i ∈ Q, Option.isSome (GenerateShares Qs S ρ i) = true ih2n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ Qsi:Fin n⊢ i ∈ Q → Option.isSome (GenerateShares Qs S ρ i) = true hiQh2n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ Qsi:Fin nhiQ:i ∈ Q⊢ Option.isSome (GenerateShares Qs S ρ i) = true
    have hex : ∃ Q' ∈ Qs, i ∈ Q' := ⟨Q, hQ, hiQ⟩h2n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ Qsi:Fin nhiQ:i ∈ Qhex:∃ Q' ∈ Qs, i ∈ Q'⊢ Option.isSome (GenerateShares Qs S ρ i) = true
    simp [GenerateShares, hex]h2n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ Qsi:Fin nhiQ:i ∈ Qhex:∃ Q' ∈ Qs, i ∈ Q'⊢ Option.isSome
    (if i = (choose ⋯).toFinset.max' ⋯ then some (S - ∑ x ∈ (choose ⋯).toFinset.erase ((choose ⋯).toFinset.max' ⋯), ρ x)
    else some (ρ i)) =
  true
    split_ifsposn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ Qsi:Fin nhiQ:i ∈ Qhex:∃ Q' ∈ Qs, i ∈ Q'h✝:i = (choose ⋯).toFinset.max' ⋯⊢ (some (S - ∑ x ∈ (choose ⋯).toFinset.erase ((choose ⋯).toFinset.max' ⋯), ρ x)).isSome = truenegn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ Qsi:Fin nhiQ:i ∈ Qhex:∃ Q' ∈ Qs, i ∈ Q'h✝:¬i = (choose ⋯).toFinset.max' ⋯⊢ (some (ρ i)).isSome = true <;>posn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ Qsi:Fin nhiQ:i ∈ Qhex:∃ Q' ∈ Qs, i ∈ Q'h✝:i = (choose ⋯).toFinset.max' ⋯⊢ (some (S - ∑ x ∈ (choose ⋯).toFinset.erase ((choose ⋯).toFinset.max' ⋯), ρ x)).isSome = truenegn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ Qsi:Fin nhiQ:i ∈ Qhex:∃ Q' ∈ Qs, i ∈ Q'h✝:¬i = (choose ⋯).toFinset.max' ⋯⊢ (some (ρ i)).isSome = true simpAll goals completed! 🐙
  /- 3) For each Q ∈ Qs, the sum over Q of shares equals S. -/
  ·h3n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod p⊢ ∀ Q ∈ Qs, (∑ i, if i ∈ Q then Option.getD (GenerateShares Qs S ρ i) 0 else 0) = S intro Q hQh3n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ Qs⊢ (∑ i, if i ∈ Q then Option.getD (GenerateShares Qs S ρ i) 0 else 0) = S
    -- Define the finite set Qfin.
    let Qfin : Finset (Fin n) := (Set.toFinite Q).toFinseth3n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinset⊢ (∑ i, if i ∈ Q then Option.getD (GenerateShares Qs S ρ i) 0 else 0) = S

    -- Establish non-emptiness to pick a 'last' element.
    have hQ_nonempty : Q.Nonempty := h_nonempty Q hQh3n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.Nonempty⊢ (∑ i, if i ∈ Q then Option.getD (GenerateShares Qs S ρ i) 0 else 0) = S
    have hQfin_nonempty : Qfin.Nonempty := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod p⊢ IsValidSharing Qs S (GenerateShares Qs S ρ)
      rw [Set.Finite.toFinset_nonempty]n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.Nonempty⊢ Q.Nonempty
      exact hQ_nonemptyAll goals completed! 🐙

    let last := Qfin.max' hQfin_nonemptyh3n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonempty⊢ (∑ i, if i ∈ Q then Option.getD (GenerateShares Qs S ρ i) 0 else 0) = S
    have hlast_mem : last ∈ Qfin := Qfin.max'_mem hQfin_nonemptyh3n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfin⊢ (∑ i, if i ∈ Q then Option.getD (GenerateShares Qs S ρ i) 0 else 0) = S

    -- We define 'g' as the numeric value of the share.
    let g : Fin n → ZMod p := fun i => (GenerateShares Qs S ρ i).getD 0h3n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0⊢ (∑ i, if i ∈ Q then Option.getD (GenerateShares Qs S ρ i) 0 else 0) = S

    -- Goal: (∑ i : Fin n, if i ∈ Q then g i else 0) = S

    -- Step 1: Restrict the sum from 'Fin n' to 'Qfin'.
    -- The LHS is sum_{i \in Fin n} (if i \in Q then g i else 0).
    -- This is exactly sum_{i \in Qfin} g i, because Qfin contains exactly the i's where i \in Q.
    have h_sum_restrict : (∑ i : Fin n, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g i := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod p⊢ IsValidSharing Qs S (GenerateShares Qs S ρ)
       rw [← Finset.sum_filter]n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0⊢ ∑ a with a ∈ Q, g a = ∑ i ∈ Qfin, g i

       -- We now need to show: ∑ i in univ.filter (· ∈ Q), g i = ∑ i in Qfin, g i
       apply Finset.sum_congrhn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0⊢ {a | a ∈ Q} = Qfinan:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0⊢ ∀ x ∈ Qfin, g x = g x
       ·hn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0⊢ {a | a ∈ Q} = Qfin -- Goal: univ.filter (· ∈ Q) = Qfin
         ext xh.hn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0x:Fin n⊢ x ∈ {a | a ∈ Q} ↔ x ∈ Qfin
         simp only [Finset.mem_filter, Finset.mem_univ, true_and]h.hn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0x:Fin n⊢ x ∈ Q ↔ x ∈ Qfin
         -- Qfin is defined as (toFinite Q).toFinset
         -- So x ∈ Qfin ↔ x ∈ Q
         simp only [Qfin]h.hn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0x:Fin n⊢ x ∈ Q ↔ x ∈ ⋯.toFinset
         simp only [Set.toFinite_toFinset, Set.mem_toFinset]All goals completed! 🐙
       ·an:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0⊢ ∀ x ∈ Qfin, g x = g x -- Goal: ∀ x ∈ univ.filter ..., g x = g x
         intros _ _an:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0x✝:Fin na✝:x✝ ∈ Qfin⊢ g x✝ = g x✝
         rflAll goals completed! 🐙

    rw [h_sum_restrict]h3n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0h_sum_restrict:(∑ i, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g i⊢ ∑ i ∈ Qfin, g i = S

    -- Step 2: Characterize 'g' inside Qfin.
    have hg_in_Q : ∀ i ∈ Qfin, g i = if i = last then S - ∑ j ∈ Qfin.erase last, ρ j else ρ i := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod p⊢ IsValidSharing Qs S (GenerateShares Qs S ρ)
      intro i hin:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0h_sum_restrict:(∑ i, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g ii:Fin nhi:i ∈ Qfin⊢ g i = if i = last then S - ∑ j ∈ Qfin.erase last, ρ j else ρ i
      dsimp [g]n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0h_sum_restrict:(∑ i, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g ii:Fin nhi:i ∈ Qfin⊢ Option.getD (GenerateShares Qs S ρ i) 0 = if i = last then S - ∑ j ∈ Qfin.erase last, ρ j else ρ i
      -- We are in Q.
      have hiQ : i ∈ Q := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod p⊢ IsValidSharing Qs S (GenerateShares Qs S ρ)
        have : i∈Q ↔ i ∈ Qfin := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod p⊢ IsValidSharing Qs S (GenerateShares Qs S ρ)
          have h1 : i ∈ Q ↔ Q i := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod p⊢ IsValidSharing Qs S (GenerateShares Qs S ρ) rflAll goals completed! 🐙
          simp only [Qfin]n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0h_sum_restrict:(∑ i, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g ii:Fin nhi:i ∈ Qfinh1:i ∈ Q ↔ Q i⊢ i ∈ Q ↔ i ∈ ⋯.toFinset
          simp only [Set.toFinite_toFinset, Set.mem_toFinset]All goals completed! 🐙
        exact this.mpr hiAll goals completed! 🐙

      -- Existence witness for GenerateShares
      have hex : ∃ Q' ∈ Qs, i ∈ Q' := ⟨Q, hQ, hiQ⟩n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0h_sum_restrict:(∑ i, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g ii:Fin nhi:i ∈ QfinhiQ:i ∈ Qhex:∃ Q' ∈ Qs, i ∈ Q'⊢ Option.getD (GenerateShares Qs S ρ i) 0 = if i = last then S - ∑ j ∈ Qfin.erase last, ρ j else ρ i

      -- Expand GenerateShares
      unfold GenerateSharesn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0h_sum_restrict:(∑ i, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g ii:Fin nhi:i ∈ QfinhiQ:i ∈ Qhex:∃ Q' ∈ Qs, i ∈ Q'⊢ Option.getD
    (if h : ∃ Q ∈ Qs, i ∈ Q then
      let Q := choose h;
      have hQ_spec := ⋯;
      have h_finite := ⋯;
      let Q_finset := h_finite.toFinset;
      have h_nonempty := ⋯;
      have last := Q_finset.max' h_nonempty;
      if i = last then
        have others := Q_finset.erase last;
        have sum_others := ∑ j ∈ others, ρ j;
        some (S - sum_others)
      else some (ρ i)
    else none)
    0 =
  if i = last then S - ∑ j ∈ Qfin.erase last, ρ j else ρ i
      rw [dif_pos hex]n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0h_sum_restrict:(∑ i, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g ii:Fin nhi:i ∈ QfinhiQ:i ∈ Qhex:∃ Q' ∈ Qs, i ∈ Q'⊢ Option.getD
    (let Q := choose hex;
    have hQ_spec := ⋯;
    have h_finite := ⋯;
    let Q_finset := h_finite.toFinset;
    have h_nonempty := ⋯;
    have last := Q_finset.max' h_nonempty;
    if i = last then
      have others := Q_finset.erase last;
      have sum_others := ∑ j ∈ others, ρ j;
      some (S - sum_others)
    else some (ρ i))
    0 =
  if i = last then S - ∑ j ∈ Qfin.erase last, ρ j else ρ i

      -- Crucial: The chosen Q' must be Q by disjointness
      have h_Q_eq : Classical.choose hex = Q :=
        GenerateShares_Q_eq h_disjoint hQ hiQn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0h_sum_restrict:(∑ i, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g ii:Fin nhi:i ∈ QfinhiQ:i ∈ Qhex:∃ Q' ∈ Qs, i ∈ Q'h_Q_eq:choose hex = Q⊢ Option.getD
    (let Q := choose hex;
    have hQ_spec := ⋯;
    have h_finite := ⋯;
    let Q_finset := h_finite.toFinset;
    have h_nonempty := ⋯;
    have last := Q_finset.max' h_nonempty;
    if i = last then
      have others := Q_finset.erase last;
      have sum_others := ∑ j ∈ others, ρ j;
      some (S - sum_others)
    else some (ρ i))
    0 =
  if i = last then S - ∑ j ∈ Qfin.erase last, ρ j else ρ i

      -- Substitute Q for the chosen set.
      -- This makes the internal 'Q_finset' and 'last' definitionally equal to our 'Qfin' and 'last'
      -- because they are defined by the same terms on the same set Q.
      simp only [h_Q_eq]n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0h_sum_restrict:(∑ i, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g ii:Fin nhi:i ∈ QfinhiQ:i ∈ Qhex:∃ Q' ∈ Qs, i ∈ Q'h_Q_eq:choose hex = Q⊢ Option.getD (if i = ⋯.toFinset.max' ⋯ then some (S - ∑ x ∈ ⋯.toFinset.erase (⋯.toFinset.max' ⋯), ρ x) else some (ρ i))
    0 =
  if i = last then S - ∑ j ∈ Qfin.erase last, ρ j else ρ i
      split_ifsposn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0h_sum_restrict:(∑ i, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g ii:Fin nhi:i ∈ QfinhiQ:i ∈ Qhex:∃ Q' ∈ Qs, i ∈ Q'h_Q_eq:choose hex = Qh✝:i = ⋯.toFinset.max' ⋯⊢ (some (S - ∑ x ∈ ⋯.toFinset.erase (⋯.toFinset.max' ⋯), ρ x)).getD 0 = S - ∑ x ∈ Qfin.erase last, ρ xnegn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0h_sum_restrict:(∑ i, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g ii:Fin nhi:i ∈ QfinhiQ:i ∈ Qhex:∃ Q' ∈ Qs, i ∈ Q'h_Q_eq:choose hex = Qh✝:¬i = ⋯.toFinset.max' ⋯⊢ (some (ρ i)).getD 0 = ρ i <;>posn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0h_sum_restrict:(∑ i, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g ii:Fin nhi:i ∈ QfinhiQ:i ∈ Qhex:∃ Q' ∈ Qs, i ∈ Q'h_Q_eq:choose hex = Qh✝:i = ⋯.toFinset.max' ⋯⊢ (some (S - ∑ x ∈ ⋯.toFinset.erase (⋯.toFinset.max' ⋯), ρ x)).getD 0 = S - ∑ x ∈ Qfin.erase last, ρ xnegn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0h_sum_restrict:(∑ i, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g ii:Fin nhi:i ∈ QfinhiQ:i ∈ Qhex:∃ Q' ∈ Qs, i ∈ Q'h_Q_eq:choose hex = Qh✝:¬i = ⋯.toFinset.max' ⋯⊢ (some (ρ i)).getD 0 = ρ i rflAll goals completed! 🐙

    -- Step 3: Split the sum into `last` and the remaining elements.
    rw [← Finset.insert_erase hlast_mem]h3n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0h_sum_restrict:(∑ i, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g ihg_in_Q:∀ i ∈ Qfin, g i = if i = last then S - ∑ j ∈ Qfin.erase last, ρ j else ρ i⊢ ∑ i ∈ insert last (Qfin.erase last), g i = S
    rw [Finset.sum_insert (by simp)]h3n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0h_sum_restrict:(∑ i, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g ihg_in_Q:∀ i ∈ Qfin, g i = if i = last then S - ∑ j ∈ Qfin.erase last, ρ j else ρ i⊢ g last + ∑ x ∈ Qfin.erase last, g x = S

    -- Evaluate the `last` term.
    rw [hg_in_Q last hlast_mem]h3n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0h_sum_restrict:(∑ i, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g ihg_in_Q:∀ i ∈ Qfin, g i = if i = last then S - ∑ j ∈ Qfin.erase last, ρ j else ρ i⊢ (if last = last then S - ∑ j ∈ Qfin.erase last, ρ j else ρ last) + ∑ x ∈ Qfin.erase last, g x = S
    rw [if_pos rfl]h3n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0h_sum_restrict:(∑ i, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g ihg_in_Q:∀ i ∈ Qfin, g i = if i = last then S - ∑ j ∈ Qfin.erase last, ρ j else ρ i⊢ S - ∑ j ∈ Qfin.erase last, ρ j + ∑ x ∈ Qfin.erase last, g x = S

    -- Evaluate the remaining terms.
    have h_sum_others :
        (∑ x ∈ Qfin.erase last, g x) = ∑ x ∈ Qfin.erase last, ρ x := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod p⊢ IsValidSharing Qs S (GenerateShares Qs S ρ)
      apply Finset.sum_congr rfln:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0h_sum_restrict:(∑ i, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g ihg_in_Q:∀ i ∈ Qfin, g i = if i = last then S - ∑ j ∈ Qfin.erase last, ρ j else ρ i⊢ ∀ x ∈ Qfin.erase last, g x = ρ x
      intro x hxn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0h_sum_restrict:(∑ i, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g ihg_in_Q:∀ i ∈ Qfin, g i = if i = last then S - ∑ j ∈ Qfin.erase last, ρ j else ρ ix:Fin nhx:x ∈ Qfin.erase last⊢ g x = ρ x

      have hx_in : x ∈ Qfin := Finset.mem_of_mem_erase hxn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0h_sum_restrict:(∑ i, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g ihg_in_Q:∀ i ∈ Qfin, g i = if i = last then S - ∑ j ∈ Qfin.erase last, ρ j else ρ ix:Fin nhx:x ∈ Qfin.erase lasthx_in:x ∈ Qfin⊢ g x = ρ x
      have hx_ne : x ≠ last := Finset.ne_of_mem_erase hxn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0h_sum_restrict:(∑ i, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g ihg_in_Q:∀ i ∈ Qfin, g i = if i = last then S - ∑ j ∈ Qfin.erase last, ρ j else ρ ix:Fin nhx:x ∈ Qfin.erase lasthx_in:x ∈ Qfinhx_ne:x ≠ last⊢ g x = ρ x

      rw [hg_in_Q x hx_in]n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0h_sum_restrict:(∑ i, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g ihg_in_Q:∀ i ∈ Qfin, g i = if i = last then S - ∑ j ∈ Qfin.erase last, ρ j else ρ ix:Fin nhx:x ∈ Qfin.erase lasthx_in:x ∈ Qfinhx_ne:x ≠ last⊢ (if x = last then S - ∑ j ∈ Qfin.erase last, ρ j else ρ x) = ρ x
      rw [if_neg hx_ne]All goals completed! 🐙

    rw [h_sum_others]h3n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pQ:Set (Fin n)hQ:Q ∈ QsQfin:Finset (Fin n) := ⋯.toFinsethQ_nonempty:Q.NonemptyhQfin_nonempty:Qfin.Nonemptylast:Fin n := Qfin.max' hQfin_nonemptyhlast_mem:last ∈ Qfing:Fin n → ZMod p := fun i => Option.getD (GenerateShares Qs S ρ i) 0h_sum_restrict:(∑ i, if i ∈ Q then g i else 0) = ∑ i ∈ Qfin, g ihg_in_Q:∀ i ∈ Qfin, g i = if i = last then S - ∑ j ∈ Qfin.erase last, ρ j else ρ ih_sum_others:∑ x ∈ Qfin.erase last, g x = ∑ x ∈ Qfin.erase last, ρ x⊢ S - ∑ j ∈ Qfin.erase last, ρ j + ∑ x ∈ Qfin.erase last, ρ x = S

    -- Step 4: Final algebra.
    ringAll goals completed! 🐙



/-
Correctness of reconstruction: if G contains a qualified set, it recovers S.
-/
theorem ReconstructSecret_correct {n : ℕ} {p : ℕ} [Fact p.Prime]
    (Qs : Set (Set (Fin n)))
    (h_disjoint : Qs.PairwiseDisjoint id)
    (h_nonempty : ∀ Q ∈ Qs, Q.Nonempty)
    (S : ZMod p) (ρ : Fin n → ZMod p)
    (G : Set (Fin n))
    (hG : ∃ Q ∈ Qs, Q ⊆ G) :
    ReconstructSecret Qs (GenerateShares Qs S ρ) G = some S := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pG:Set (Fin n)hG:∃ Q ∈ Qs, Q ⊆ G⊢ ReconstructSecret Qs (GenerateShares Qs S ρ) G = some S
  unfold ReconstructSecretn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pG:Set (Fin n)hG:∃ Q ∈ Qs, Q ⊆ G⊢ (if h : ∃ Q ∈ Qs, Q ⊆ G then
    let Q := choose h;
    have sum_shares := ∑ i ∈ ⋯.toFinset, Option.getD (GenerateShares Qs S ρ i) 0;
    some sum_shares
  else none) =
  some S;
  have := Classical.choose_spec hGn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pG:Set (Fin n)hG:∃ Q ∈ Qs, Q ⊆ Gthis:choose hG ∈ Qs ∧ choose hG ⊆ G⊢ (if h : ∃ Q ∈ Qs, Q ⊆ G then
    let Q := choose h;
    have sum_shares := ∑ i ∈ ⋯.toFinset, Option.getD (GenerateShares Qs S ρ i) 0;
    some sum_shares
  else none) =
  some S;
  have h_sum_shares : ∑ i ∈ (Set.toFinite (Classical.choose hG)).toFinset, (GenerateShares Qs S ρ i).getD 0 = S := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pG:Set (Fin n)hG:∃ Q ∈ Qs, Q ⊆ G⊢ ReconstructSecret Qs (GenerateShares Qs S ρ) G = some S
    have h_valid : IsValidSharing Qs S (GenerateShares Qs S ρ) := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pG:Set (Fin n)hG:∃ Q ∈ Qs, Q ⊆ G⊢ ReconstructSecret Qs (GenerateShares Qs S ρ) G = some S
      exact GenerateShares_isValid Qs h_disjoint h_nonempty S ρAll goals completed! 🐙
    convert h_valid.2.2 _ this.1 using 1h.e'_2n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pG:Set (Fin n)hG:∃ Q ∈ Qs, Q ⊆ Gthis:choose hG ∈ Qs ∧ choose hG ⊆ Gh_valid:IsValidSharing Qs S (GenerateShares Qs S ρ)⊢ ∑ i ∈ ⋯.toFinset, Option.getD (GenerateShares Qs S ρ i) 0 =
  ∑ i, if i ∈ choose hG then Option.getD (GenerateShares Qs S ρ i) 0 else 0;
    rw [ ← Finset.sum_filter ]h.e'_2n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pG:Set (Fin n)hG:∃ Q ∈ Qs, Q ⊆ Gthis:choose hG ∈ Qs ∧ choose hG ⊆ Gh_valid:IsValidSharing Qs S (GenerateShares Qs S ρ)⊢ ∑ i ∈ ⋯.toFinset, Option.getD (GenerateShares Qs S ρ i) 0 =
  ∑ a with a ∈ choose hG, Option.getD (GenerateShares Qs S ρ a) 0 ; congrh.e'_2.e_sn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pG:Set (Fin n)hG:∃ Q ∈ Qs, Q ⊆ Gthis:choose hG ∈ Qs ∧ choose hG ⊆ Gh_valid:IsValidSharing Qs S (GenerateShares Qs S ρ)⊢ ⋯.toFinset = {a | a ∈ choose hG} ; exth.e'_2.e_s.hn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyS:ZMod pρ:Fin n → ZMod pG:Set (Fin n)hG:∃ Q ∈ Qs, Q ⊆ Gthis:choose hG ∈ Qs ∧ choose hG ⊆ Gh_valid:IsValidSharing Qs S (GenerateShares Qs S ρ)a✝:Fin n⊢ a✝ ∈ ⋯.toFinset ↔ a✝ ∈ {a | a ∈ choose hG} ; aesopAll goals completed! 🐙;
  aesopAll goals completed! 🐙


open AccessStructure SecretSharingScheme

-- We define the specific Access Structure for Disjoint Sets
def DisjointAS (Qs : Set (Set (Fin n))) : AccessStructure n where
  auth := {A | ∃ Q ∈ Qs, Q ⊆ A}
  h_monotone := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))⊢ ∀ {A B : Set (Fin n)}, A ∈ {A | ∃ Q ∈ Qs, Q ⊆ A} → A ⊆ B → B ∈ {A | ∃ Q ∈ Qs, Q ⊆ A}
    intro A Bn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)B:Set (Fin n)⊢ A ∈ {A | ∃ Q ∈ Qs, Q ⊆ A} → A ⊆ B → B ∈ {A | ∃ Q ∈ Qs, Q ⊆ A} hAn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)B:Set (Fin n)hA:A ∈ {A | ∃ Q ∈ Qs, Q ⊆ A}⊢ A ⊆ B → B ∈ {A | ∃ Q ∈ Qs, Q ⊆ A} hsubn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)B:Set (Fin n)hA:A ∈ {A | ∃ Q ∈ Qs, Q ⊆ A}hsub:A ⊆ B⊢ B ∈ {A | ∃ Q ∈ Qs, Q ⊆ A}
    obtain ⟨Q, hQ, hQA⟩ := hAn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)B:Set (Fin n)hsub:A ⊆ BQ:Set (Fin n)hQ:Q ∈ QshQA:Q ⊆ A⊢ B ∈ {A | ∃ Q ∈ Qs, Q ⊆ A}
    use Q, hQrightn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))A:Set (Fin n)B:Set (Fin n)hsub:A ⊆ BQ:Set (Fin n)hQ:Q ∈ QshQA:Q ⊆ A⊢ Q ⊆ B
    exact Set.Subset.trans hQA hsubAll goals completed! 🐙


noncomputable def DisjointScheme {n : ℕ} (p : ℕ)
    [Fact p.Prime] (Qs : Set (Set (Fin n)))
    : SecretSharingScheme n := {
  Secret := ZMod p
  Random := Fin n → ZMod p
  Share := fun _ => Option (ZMod p)
  dealer := fun s ρ i => GenerateShares Qs s ρ i
  hSecret_card := byn✝:ℕp✝:ℕinst✝¹:Fact (Nat.Prime p✝)n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))⊢ Fintype.card (ZMod p) ≥ 2
    simpa using Nat.Prime.two_le Fact.outAll goals completed! 🐙
  μ := PMF.uniformOfFintype (Fin n → ZMod p)
}

noncomputable def DisjointReconstruction {n : ℕ} (p : ℕ) [Fact p.Prime] (Qs : Set (Set (Fin n))) :
  ReconstructionAlgorithm (DisjointScheme p Qs) (DisjointAS Qs) :=
  fun B _hB shares =>
    let full_shares : Fin n → Option (ZMod p) := fun i =>
      if h : i ∈ B then shares ⟨i, h⟩ else none
    match ReconstructSecret Qs full_shares B with
    | some s => s
    | none   => (0 : ZMod p)

theorem DisjointScheme_Correctness {n : ℕ} (p : ℕ) [Fact p.Prime] (Qs : Set (Set (Fin n)))
    (h_disjoint : Qs.PairwiseDisjoint id)
    (h_nonempty : ∀ Q ∈ Qs, Q.Nonempty) :
    Correctness (DisjointScheme p Qs) (DisjointAS Qs) (DisjointReconstruction p Qs) := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonempty⊢ (DisjointScheme p Qs).Correctness (DisjointAS Qs) (DisjointReconstruction p Qs)
  intro s rn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptys:(DisjointScheme p Qs).Secretr:(DisjointScheme p Qs).Random⊢ ∀ (B : Set (Fin n)) (hB : B ∈ (DisjointAS Qs).auth),
  DisjointReconstruction p Qs B hB ((DisjointScheme p Qs).shares_of_set s r B) = s Bn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptys:(DisjointScheme p Qs).Secretr:(DisjointScheme p Qs).RandomB:Set (Fin n)⊢ ∀ (hB : B ∈ (DisjointAS Qs).auth), DisjointReconstruction p Qs B hB ((DisjointScheme p Qs).shares_of_set s r B) = s hBn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptys:(DisjointScheme p Qs).Secretr:(DisjointScheme p Qs).RandomB:Set (Fin n)hB:B ∈ (DisjointAS Qs).auth⊢ DisjointReconstruction p Qs B hB ((DisjointScheme p Qs).shares_of_set s r B) = s
  simp [DisjointReconstruction, shares_of_set, DisjointScheme]n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptys:(DisjointScheme p Qs).Secretr:(DisjointScheme p Qs).RandomB:Set (Fin n)hB:B ∈ (DisjointAS Qs).auth⊢ (match ReconstructSecret Qs (fun i => if i ∈ B then GenerateShares Qs s r i else none) B with
  | some s => s
  | none => 0) =
  s
  -- We need to show `full_shares` behaves like `GenerateShares` on `B`.
  -- And since `B` contains a qualified set, `ReconstructSecret` should work.
  have h_recon := ReconstructSecret_correct Qs h_disjoint h_nonempty s r B hBn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptys:(DisjointScheme p Qs).Secretr:(DisjointScheme p Qs).RandomB:Set (Fin n)hB:B ∈ (DisjointAS Qs).authh_recon:ReconstructSecret Qs (GenerateShares Qs s r) B = some s⊢ (match ReconstructSecret Qs (fun i => if i ∈ B then GenerateShares Qs s r i else none) B with
  | some s => s
  | none => 0) =
  s
  -- The `ReconstructSecret` in `DisjointReconstruction` uses `full_shares`.
  -- We need to show that `ReconstructSecret` with `full_shares` returns `some s`.
  convert congr_arg Option.get! h_recon using 1h.e'_2n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptys:(DisjointScheme p Qs).Secretr:(DisjointScheme p Qs).RandomB:Set (Fin n)hB:B ∈ (DisjointAS Qs).authh_recon:ReconstructSecret Qs (GenerateShares Qs s r) B = some s⊢ (match ReconstructSecret Qs (fun i => if i ∈ B then GenerateShares Qs s r i else none) B with
  | some s => s
  | none => 0) =
  (ReconstructSecret Qs (GenerateShares Qs s r) B).get!;
  unfold ReconstructSecreth.e'_2n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptys:(DisjointScheme p Qs).Secretr:(DisjointScheme p Qs).RandomB:Set (Fin n)hB:B ∈ (DisjointAS Qs).authh_recon:ReconstructSecret Qs (GenerateShares Qs s r) B = some s⊢ (match
    if h : ∃ Q ∈ Qs, Q ⊆ B then
      let Q := choose h;
      have sum_shares := ∑ i ∈ ⋯.toFinset, ((fun i => if i ∈ B then GenerateShares Qs s r i else none) i).getD 0;
      some sum_shares
    else none with
  | some s => s
  | none => 0) =
  (if h : ∃ Q ∈ Qs, Q ⊆ B then
      let Q := choose h;
      have sum_shares := ∑ i ∈ ⋯.toFinset, Option.getD (GenerateShares Qs s r i) 0;
      some sum_shares
    else none).get!;
  split_ifsposn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptys:(DisjointScheme p Qs).Secretr:(DisjointScheme p Qs).RandomB:Set (Fin n)hB:B ∈ (DisjointAS Qs).authh_recon:ReconstructSecret Qs (GenerateShares Qs s r) B = some sh✝:∃ Q ∈ Qs, Q ⊆ B⊢ (match
    let Q := choose h✝;
    have sum_shares := ∑ i ∈ ⋯.toFinset, ((fun i => if i ∈ B then GenerateShares Qs s r i else none) i).getD 0;
    some sum_shares with
  | some s => s
  | none => 0) =
  (let Q := choose h✝;
    have sum_shares := ∑ i ∈ ⋯.toFinset, Option.getD (GenerateShares Qs s r i) 0;
    some sum_shares).get!negn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptys:(DisjointScheme p Qs).Secretr:(DisjointScheme p Qs).RandomB:Set (Fin n)hB:B ∈ (DisjointAS Qs).authh_recon:ReconstructSecret Qs (GenerateShares Qs s r) B = some sh✝:¬∃ Q ∈ Qs, Q ⊆ B⊢ (match none with
  | some s => s
  | none => 0) =
  none.get! <;>posn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptys:(DisjointScheme p Qs).Secretr:(DisjointScheme p Qs).RandomB:Set (Fin n)hB:B ∈ (DisjointAS Qs).authh_recon:ReconstructSecret Qs (GenerateShares Qs s r) B = some sh✝:∃ Q ∈ Qs, Q ⊆ B⊢ (match
    let Q := choose h✝;
    have sum_shares := ∑ i ∈ ⋯.toFinset, ((fun i => if i ∈ B then GenerateShares Qs s r i else none) i).getD 0;
    some sum_shares with
  | some s => s
  | none => 0) =
  (let Q := choose h✝;
    have sum_shares := ∑ i ∈ ⋯.toFinset, Option.getD (GenerateShares Qs s r i) 0;
    some sum_shares).get!negn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptys:(DisjointScheme p Qs).Secretr:(DisjointScheme p Qs).RandomB:Set (Fin n)hB:B ∈ (DisjointAS Qs).authh_recon:ReconstructSecret Qs (GenerateShares Qs s r) B = some sh✝:¬∃ Q ∈ Qs, Q ⊆ B⊢ (match none with
  | some s => s
  | none => 0) =
  none.get!
  simpnegn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptys:(DisjointScheme p Qs).Secretr:(DisjointScheme p Qs).RandomB:Set (Fin n)hB:B ∈ (DisjointAS Qs).authh_recon:ReconstructSecret Qs (GenerateShares Qs s r) B = some sh✝:¬∃ Q ∈ Qs, Q ⊆ B⊢ 0 = default
  ·posn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptys:(DisjointScheme p Qs).Secretr:(DisjointScheme p Qs).RandomB:Set (Fin n)hB:B ∈ (DisjointAS Qs).authh_recon:ReconstructSecret Qs (GenerateShares Qs s r) B = some sh✝:∃ Q ∈ Qs, Q ⊆ B⊢ ∑ x ∈ (choose h✝).toFinset, (if x ∈ B then GenerateShares Qs s r x else none).getD 0 =
  ∑ x ∈ (choose h✝).toFinset, Option.getD (GenerateShares Qs s r x) 0 exact Finset.sum_congr rfl fun x hx => byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptys:(DisjointScheme p Qs).Secretr:(DisjointScheme p Qs).RandomB:Set (Fin n)hB:B ∈ (DisjointAS Qs).authh_recon:ReconstructSecret Qs (GenerateShares Qs s r) B = some sh✝:∃ Q ∈ Qs, Q ⊆ Bx:Fin nhx:x ∈ (choose h✝).toFinset⊢ (if x ∈ B then GenerateShares Qs s r x else none).getD 0 = Option.getD (GenerateShares Qs s r x) 0 rw [ if_pos ( by exact Classical.choose_spec ( ‹∃ Q ∈ Qs, Q ⊆ B› ) |>.2 ( by simpa using hx ) ) ]All goals completed! 🐙 ;
  ·negn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonemptys:(DisjointScheme p Qs).Secretr:(DisjointScheme p Qs).RandomB:Set (Fin n)hB:B ∈ (DisjointAS Qs).authh_recon:ReconstructSecret Qs (GenerateShares Qs s r) B = some sh✝:¬∃ Q ∈ Qs, Q ⊆ B⊢ 0 = default rflAll goals completed! 🐙


/-
Perfect security theorem: The number of random tapes consistent with a given set of shares on an unauthorized set is independent of the secret.
-/
theorem PerfectSecurity_card_eq {n : ℕ} {p : ℕ} [Fact p.Prime]
    (Qs : Set (Set (Fin n)))
    (h_disjoint : Qs.PairwiseDisjoint id)
    (h_nonempty : ∀ Q ∈ Qs, Q.Nonempty)
    (A : Set (Fin n))
    (h_unauth : ∀ Q ∈ Qs, ¬(Q ⊆ A)) -- A is unauthorized
    (shares_A : ∀ i : Fin n, i ∈ A → Share p) -- Fixed shares for A
    (S1 S2 : ZMod p) :
    Set.ncard {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi} =
    Set.ncard {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi} := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyA:Set (Fin n)h_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → _root_.Share pS1:ZMod pS2:ZMod p⊢ {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}.ncard =
  {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi}.ncard
  have h_bij := shift_is_bijection h_disjoint h_nonempty h_unauth shares_A (S1 := S1) (S2 := S2)n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyA:Set (Fin n)h_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → _root_.Share pS1:ZMod pS2:ZMod ph_bij:Set.BijOn (fun ρ => ρ + shift Qs A S1 S2) {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}
  {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi}⊢ {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}.ncard =
  {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi}.ncard
  rw [← h_bij.image_eq]n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyA:Set (Fin n)h_unauth:∀ Q ∈ Qs, ¬Q ⊆ Ashares_A:(i : Fin n) → i ∈ A → _root_.Share pS1:ZMod pS2:ZMod ph_bij:Set.BijOn (fun ρ => ρ + shift Qs A S1 S2) {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}
  {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S2 ρ i = shares_A i hi}⊢ {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}.ncard =
  ((fun ρ => ρ + shift Qs A S1 S2) '' {ρ | ∀ (i : Fin n) (hi : i ∈ A), GenerateShares Qs S1 ρ i = shares_A i hi}).ncard
  rw [Set.InjOn.ncard_image h_bij.injOn]All goals completed! 🐙


theorem DisjointScheme_Security {n : ℕ} (p : ℕ) [Fact p.Prime] (Qs : Set (Set (Fin n)))
    (h_disjoint : Qs.PairwiseDisjoint id)
    (h_nonempty : ∀ Q ∈ Qs, Q.Nonempty) :
    PerfectSecurity (DisjointScheme p Qs) (DisjointAS Qs) := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonempty⊢ (DisjointScheme p Qs).PerfectSecurity (DisjointAS Qs)
  unfold SecretSharingScheme.PerfectSecurity DisjointScheme DisjointASn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonempty⊢ ∀ B ∉ { auth := {A | ∃ Q ∈ Qs, Q ⊆ A}, h_monotone := ⋯ }.auth,
  ∀
    (s s' :
      { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
          Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
          hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secret),
    PMF.map
        (fun r =>
          { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
                Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
                hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.shares_of_set
            s r B)
        { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
            Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
            hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.μ =
      PMF.map
        (fun r =>
          { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
                Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
                hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.shares_of_set
            s' r B)
        { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
            Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
            hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.μ;
  intro B hBn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyB:Set (Fin n)hB:B ∉ { auth := {A | ∃ Q ∈ Qs, Q ⊆ A}, h_monotone := ⋯ }.auth⊢ ∀
  (s s' :
    { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
        Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
        hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secret),
  PMF.map
      (fun r =>
        { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
              Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
              hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.shares_of_set
          s r B)
      { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
          Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
          hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.μ =
    PMF.map
      (fun r =>
        { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
              Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
              hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.shares_of_set
          s' r B)
      { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
          Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
          hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.μ sn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyB:Set (Fin n)hB:B ∉ { auth := {A | ∃ Q ∈ Qs, Q ⊆ A}, h_monotone := ⋯ }.auths:{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secret⊢ ∀
  (s' :
    { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
        Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
        hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secret),
  PMF.map
      (fun r =>
        { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
              Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
              hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.shares_of_set
          s r B)
      { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
          Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
          hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.μ =
    PMF.map
      (fun r =>
        { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
              Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
              hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.shares_of_set
          s' r B)
      { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
          Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
          hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.μ s'n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyB:Set (Fin n)hB:B ∉ { auth := {A | ∃ Q ∈ Qs, Q ⊆ A}, h_monotone := ⋯ }.auths:{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secrets':{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secret⊢ PMF.map
    (fun r =>
      { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
            Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
            hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.shares_of_set
        s r B)
    { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
        Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
        hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.μ =
  PMF.map
    (fun r =>
      { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
            Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
            hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.shares_of_set
        s' r B)
    { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
        Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
        hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.μ;
  ext xhn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyB:Set (Fin n)hB:B ∉ { auth := {A | ∃ Q ∈ Qs, Q ⊆ A}, h_monotone := ⋯ }.auths:{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secrets':{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secretx:(i : ↑B) →
  { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
        Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
        hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Share
    ↑i⊢ (PMF.map
      (fun r =>
        { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
              Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
              hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.shares_of_set
          s r B)
      { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
          Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
          hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.μ)
    x =
  (PMF.map
      (fun r =>
        { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
              Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
              hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.shares_of_set
          s' r B)
      { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
          Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
          hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.μ)
    x;
  have h_card : Set.ncard {ρ : Fin n → ZMod p | shares_of_set (DisjointScheme p Qs) s ρ B = x} = Set.ncard {ρ : Fin n → ZMod p | shares_of_set (DisjointScheme p Qs) s' ρ B = x} := byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.Nonempty⊢ (DisjointScheme p Qs).PerfectSecurity (DisjointAS Qs)
    have := PerfectSecurity_card_eq Qs h_disjoint h_nonempty B (byn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyB:Set (Fin n)hB:B ∉ { auth := {A | ∃ Q ∈ Qs, Q ⊆ A}, h_monotone := ⋯ }.auths:{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secrets':{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secretx:(i : ↑B) →
  { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
        Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
        hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Share
    ↑i⊢ ∀ Q ∈ Qs, ¬Q ⊆ B
    exact fun Q hQ hQB => hB ⟨ Q, hQ, hQB ⟩All goals completed! 🐙) (fun i hi => x ⟨i, hi⟩) s s';
    convert this using 1h.e'_2n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyB:Set (Fin n)hB:B ∉ { auth := {A | ∃ Q ∈ Qs, Q ⊆ A}, h_monotone := ⋯ }.auths:{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secrets':{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secretx:(i : ↑B) →
  { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
        Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
        hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Share
    ↑ithis:{ρ | ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s ρ i = x ⟨i, hi⟩}.ncard =
  {ρ | ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s' ρ i = x ⟨i, hi⟩}.ncard⊢ {ρ | (DisjointScheme p Qs).shares_of_set s ρ B = x}.ncard =
  {ρ | ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s ρ i = x ⟨i, hi⟩}.ncardh.e'_3n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyB:Set (Fin n)hB:B ∉ { auth := {A | ∃ Q ∈ Qs, Q ⊆ A}, h_monotone := ⋯ }.auths:{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secrets':{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secretx:(i : ↑B) →
  { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
        Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
        hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Share
    ↑ithis:{ρ | ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s ρ i = x ⟨i, hi⟩}.ncard =
  {ρ | ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s' ρ i = x ⟨i, hi⟩}.ncard⊢ {ρ | (DisjointScheme p Qs).shares_of_set s' ρ B = x}.ncard =
  {ρ | ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s' ρ i = x ⟨i, hi⟩}.ncard;
    ·h.e'_2n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyB:Set (Fin n)hB:B ∉ { auth := {A | ∃ Q ∈ Qs, Q ⊆ A}, h_monotone := ⋯ }.auths:{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secrets':{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secretx:(i : ↑B) →
  { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
        Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
        hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Share
    ↑ithis:{ρ | ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s ρ i = x ⟨i, hi⟩}.ncard =
  {ρ | ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s' ρ i = x ⟨i, hi⟩}.ncard⊢ {ρ | (DisjointScheme p Qs).shares_of_set s ρ B = x}.ncard =
  {ρ | ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s ρ i = x ⟨i, hi⟩}.ncard congr with ρh.e'_2.e_s.e_p.h.an:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyB:Set (Fin n)hB:B ∉ { auth := {A | ∃ Q ∈ Qs, Q ⊆ A}, h_monotone := ⋯ }.auths:{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secrets':{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secretx:(i : ↑B) →
  { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
        Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
        hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Share
    ↑ithis:{ρ | ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s ρ i = x ⟨i, hi⟩}.ncard =
  {ρ | ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s' ρ i = x ⟨i, hi⟩}.ncardρ:Fin n → ZMod p⊢ (DisjointScheme p Qs).shares_of_set s ρ B = x ↔ ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s ρ i = x ⟨i, hi⟩ ; simp +decide [ funext_iff, shares_of_set ]h.e'_2.e_s.e_p.h.an:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyB:Set (Fin n)hB:B ∉ { auth := {A | ∃ Q ∈ Qs, Q ⊆ A}, h_monotone := ⋯ }.auths:{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secrets':{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secretx:(i : ↑B) →
  { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
        Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
        hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Share
    ↑ithis:{ρ | ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s ρ i = x ⟨i, hi⟩}.ncard =
  {ρ | ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s' ρ i = x ⟨i, hi⟩}.ncardρ:Fin n → ZMod p⊢ (∀ (a : Fin n) (b : a ∈ B), (DisjointScheme p Qs).dealer s ρ a = x ⟨a, b⟩) ↔
  ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s ρ i = x ⟨i, hi⟩;
      rflAll goals completed! 🐙;
    ·h.e'_3n:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyB:Set (Fin n)hB:B ∉ { auth := {A | ∃ Q ∈ Qs, Q ⊆ A}, h_monotone := ⋯ }.auths:{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secrets':{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secretx:(i : ↑B) →
  { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
        Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
        hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Share
    ↑ithis:{ρ | ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s ρ i = x ⟨i, hi⟩}.ncard =
  {ρ | ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s' ρ i = x ⟨i, hi⟩}.ncard⊢ {ρ | (DisjointScheme p Qs).shares_of_set s' ρ B = x}.ncard =
  {ρ | ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s' ρ i = x ⟨i, hi⟩}.ncard congr with ρh.e'_3.e_s.e_p.h.an:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyB:Set (Fin n)hB:B ∉ { auth := {A | ∃ Q ∈ Qs, Q ⊆ A}, h_monotone := ⋯ }.auths:{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secrets':{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secretx:(i : ↑B) →
  { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
        Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
        hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Share
    ↑ithis:{ρ | ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s ρ i = x ⟨i, hi⟩}.ncard =
  {ρ | ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s' ρ i = x ⟨i, hi⟩}.ncardρ:Fin n → ZMod p⊢ (DisjointScheme p Qs).shares_of_set s' ρ B = x ↔ ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s' ρ i = x ⟨i, hi⟩ ; simp +decide [ funext_iff, shares_of_set ]h.e'_3.e_s.e_p.h.an:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyB:Set (Fin n)hB:B ∉ { auth := {A | ∃ Q ∈ Qs, Q ⊆ A}, h_monotone := ⋯ }.auths:{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secrets':{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secretx:(i : ↑B) →
  { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
        Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
        hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Share
    ↑ithis:{ρ | ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s ρ i = x ⟨i, hi⟩}.ncard =
  {ρ | ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s' ρ i = x ⟨i, hi⟩}.ncardρ:Fin n → ZMod p⊢ (∀ (a : Fin n) (b : a ∈ B), (DisjointScheme p Qs).dealer s' ρ a = x ⟨a, b⟩) ↔
  ∀ (i : Fin n) (hi : i ∈ B), GenerateShares Qs s' ρ i = x ⟨i, hi⟩;
      rflAll goals completed! 🐙;
  simp_all [ Set.ncard_eq_toFinset_card', tsum_fintype ]hn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyB:Set (Fin n)s:{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secrets':{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secretx:(i : ↑B) →
  { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
        Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
        hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Share
    ↑ihB:∀ Q ∈ Qs, ¬Q ⊆ Bh_card:{x_1 | (DisjointScheme p Qs).shares_of_set s x_1 B = x}.card =
  {x_1 | (DisjointScheme p Qs).shares_of_set s' x_1 B = x}.card⊢ (∑ a,
    if
        x =
          { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
                Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
                hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.shares_of_set
            s a B then
      (↑p ^ n)⁻¹
    else 0) =
  ∑ a,
    if
        x =
          { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
                Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
                hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.shares_of_set
            s' a B then
      (↑p ^ n)⁻¹
    else 0;
  simp_all [ eq_comm, Finset.sum_ite ]hn:ℕp:ℕinst✝:Fact (Nat.Prime p)Qs:Set (Set (Fin n))h_disjoint:Qs.PairwiseDisjoint idh_nonempty:∀ Q ∈ Qs, Q.NonemptyB:Set (Fin n)s:{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secrets':{ Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
    Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
    hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Secretx:(i : ↑B) →
  { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
        Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
        hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.Share
    ↑ihB:∀ Q ∈ Qs, ¬Q ⊆ Bh_card:{x_1 | x = (DisjointScheme p Qs).shares_of_set s x_1 B}.card =
  {x_1 | x = (DisjointScheme p Qs).shares_of_set s' x_1 B}.card⊢ ↑{x_1 |
          x =
            { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
                  Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
                  hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.shares_of_set
              s x_1 B}.card *
    (↑p ^ n)⁻¹ =
  ↑{x_1 |
          x =
            { Secret := ZMod p, Random := Fin n → ZMod p, hSecret := ZMod.fintype p, hSecret_card := ⋯,
                  Share := fun x => Option (ZMod p), hShare := fun i => instFintypeOption, hRandom := Pi.instFintype,
                  hRandomNonempty := ⋯, dealer := fun s ρ i => GenerateShares Qs s ρ i }.shares_of_set
              s' x_1 B}.card *
    (↑p ^ n)⁻¹;
  convert congr_arg ( · * ( p ^ n : ENNReal ) ⁻¹ ) ( congr_arg ( fun x : ℕ => ( x : ENNReal ) ) h_card )All goals completed! 🐙
  -- using 1

/--
  The function `DisjointReconstruction` realizes the disjoint access structure
-/
noncomputable def DisjointRealizedScheme {n : ℕ} (p : ℕ) [Fact p.Prime] (Qs : Set (Set (Fin n)))
    (h_disjoint : Qs.PairwiseDisjoint id)
    (h_nonempty : ∀ Q ∈ Qs, Q.Nonempty) :
    RealizedSecretSharingScheme n (DisjointAS Qs) := {
  toSecretSharingScheme := DisjointScheme p Qs
  recon := DisjointReconstruction p Qs
  h_correctness := DisjointScheme_Correctness p Qs h_disjoint h_nonempty
  h_security := DisjointScheme_Security p Qs h_disjoint h_nonempty
}

end DisjointAccessStructure