have hy : ∀ (y : ℕ), y ∈ xs → Nat.Coprime n y :=
  fun y hy ↦ h y (List.mem_cons.mpr (Or.inr hy))
case cons
n x : ℕ
xs : List ℕ
ih : (∀ y ∈ xs, n.Coprime y) → n.Coprime xs.prod
h : ∀ y ∈ x :: xs, n.Coprime y
⊢ n.Coprime (x :: xs).prod
case cons
n x : ℕ
xs : List ℕ
ih : (∀ y ∈ xs, n.Coprime y) → n.Coprime xs.prod
h : ∀ y ∈ x :: xs, n.Coprime y
hy : ∀ y ∈ xs, n.Coprime y
⊢ n.Coprime (x :: xs).prod