simp only [Set.mem_singleton_iff, OfNat.one_ne_ofNat, Set.singleton_subset_iff,
  Set.mem_insert_iff, or_false, Set.iInter_iInter_eq_left, Set.iInter_iInter_eq_or_left,
  Set.subset_inter_iff, not_false_eq_true, Set.insert_subset_insert_iff, Set.subset_singleton_iff,
  imp_self, forall_const, forall_eq, and_false, and_self]
case h
A : ℕ → Set ℕ := fun n => {0, n}
⊢ {1} ⊆ {1, 2} ∧ ¬⋂ j ∈ {1}, A j ⊆ ⋂ i ∈ {1, 2}, A i
no goals