rw [lin_rel, Set.subset_def] at is_fn
is_fn : lin_rel ⊆ Set.univ ×ˢ Set.univ ∧ ∀ (x : ℤ), ∃! y, (x, y) ∈ lin_rel
⊢ False
is_fn : (∀ x ∈ {p | p.1 + 3 * p.2 = 4}, x ∈ Set.univ ×ˢ Set.univ) ∧ ∀ (x : ℤ), ∃! y, (x, y) ∈ {p | p.1 + 3 * p.2 = 4}
⊢ False