obtain ⟨k, hk1, hk2⟩ := Nat.chineseRemainder h1 x.remainder b
case cons.intro
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
⊢ ∃ m, ∀ x_1 ∈ x :: xs, m ≡ x_1.remainder [MOD x_1.modulus]
case cons.intro.mk.intro
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]
⊢ ∃ m, ∀ x_1 ∈ x :: xs, m ≡ x_1.remainder [MOD x_1.modulus]