induction lst with
| nil => simp only [List.prod_nil, Nat.coprime_one_right_eq_true]
| cons x xs ih =>
  have hy : ∀ (y : ℕ), y ∈ xs → Nat.Coprime n y :=
    fun y hy ↦ h y (List.mem_cons.mpr (Or.inr hy))
  have h1 := h x (by simp)
  rw [List.prod_cons]
  exact Nat.Coprime.mul_right h1 (ih hy)
n : ℕ
lst : List ℕ
h : ∀ y ∈ lst, n.Coprime y
⊢ n.Coprime lst.prod
no goals