cases hz with
| head => exact hk1
| tail w hw =>
  have h2 := hb z hw
  have h4 := modulus_of_product hk2 _ (List.mem_map_of_mem ChinesePair.modulus hw)
  exact Nat.ModEq.trans h4 h2
case h
x : ChinesePair
xs : List ChinesePair
x_coprime : (∀ a' ∈ xs, x.modulus.Coprime a'.modulus) ∧ List.Pairwise (fun x y => x.modulus.Coprime y.modulus) xs
b : ℕ
hb : ∀ x ∈ xs, b ≡ x.remainder [MOD x.modulus]
h1 : x.modulus.Coprime (List.map (fun x => x.modulus) xs).prod
k : ℕ
hk1 : k ≡ x.remainder [MOD x.modulus]
hk2 : k ≡ b [MOD (List.map (fun x => x.modulus) xs).prod]
z : ChinesePair
hz : z ∈ x :: xs
⊢ k ≡ z.remainder [MOD z.modulus]
no goals