English
For any z and pair xy, xy ∈ divisorsAntidiag z iff the product of its components equals z and z ≠ 0.
Русский
Для любых z и пары xy, xy ∈ divisorsAntidiag z тогда и только тогда, когда произведение компонентов пары равно z и z ≠ 0.
LaTeX
$$$(xy) \in z.\mathrm{divisorsAntidiag} \iff (xy.fst \cdot xy.snd = z) \land z \neq 0.$$$
Lean4
@[simp]
theorem mem_divisorsAntidiag : ∀ {z} {xy : ℤ × ℤ}, xy ∈ divisorsAntidiag z ↔ xy.fst * xy.snd = z ∧ z ≠ 0
| (n : ℕ), ((x : ℕ), (y : ℕ)) => by
simp [divisorsAntidiag]
norm_cast
simp +contextual [eq_comm]
| (n : ℕ), (negSucc x, negSucc y) =>
by
simp [divisorsAntidiag, negSucc_eq, -neg_add_rev]
norm_cast
simp +contextual [eq_comm]
| (n : ℕ), ((x : ℕ), negSucc y) =>
by
simp [divisorsAntidiag, negSucc_eq, -neg_add_rev]
norm_cast
aesop
| (n : ℕ), (negSucc x, (y : ℕ)) =>
by
suffices (∃ a, (n = a * y ∧ ¬n = 0) ∧ (a : ℤ) = -1 + -↑x) ↔ (n : ℤ) = (-1 + -↑x) * ↑y ∧ ¬n = 0 by
simpa [divisorsAntidiag, eq_comm, negSucc_eq]
simp only [← Int.neg_add, Int.add_comm 1, Int.neg_mul, Int.add_mul]
norm_cast
match n with
| 0 => simp
| n + 1 => simp
| .negSucc n, ((x : ℕ), (y : ℕ)) => by
simp [divisorsAntidiag]
norm_cast
| .negSucc n, (negSucc x, negSucc y) =>
by
simp [divisorsAntidiag, negSucc_eq, -neg_add_rev]
norm_cast
simp +contextual
| .negSucc n, ((x : ℕ), negSucc y) =>
by
simp [divisorsAntidiag, negSucc_eq, -neg_add_rev]
norm_cast
aesop
| .negSucc n, (negSucc x, (y : ℕ)) =>
by
simp [divisorsAntidiag, negSucc_eq, -neg_add_rev]
norm_cast
simp +contextual [eq_comm]
