-- Mathlib/NumberTheory/Divisors.lean
@[simp]
lemma 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
    simp [divisorsAntidiag]
    norm_cast
    aesop
  | .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 [eq_comm]
  | .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]

Proof state:
n x y : ℕ
⊢ (-[x+1], ↑y) ∈ -[n+1].divisorsAntidiag ↔ (-[x+1], ↑y).1 * (-[x+1], ↑y).2 = -[n+1] ∧ -[n+1] ≠ 0

Tactic:
simp [divisorsAntidiag, negSucc_eq, -neg_add_rev]

Result:
n x y : ℕ
⊢ (∃ a, a * y = n + 1 ∧ ↑a = ↑x + 1) ↔ (↑x + 1) * ↑y = ↑n + 1 ∧ ¬↑n + 1 = 0

Proof state:
n x y : ℕ
⊢ ((∃ a b, (a * b = n ∧ ¬n = 0) ∧ ↑a = -(↑x + 1) ∧ ↑b = -(↑y + 1)) ∨
      ∃ a b, (a * b = n ∧ ¬n = 0) ∧ ↑a = ↑x + 1 ∧ ↑b = ↑y + 1) ↔
    (↑x + 1) * (↑y + 1) = ↑n ∧ ¬n = 0

Tactic:
norm_cast

Result:
n x y : ℕ
⊢ ((∃ a b, (a * b = n ∧ ¬n = 0) ∧ False ∧ False) ∨ ∃ a b, (a * b = n ∧ ¬n = 0) ∧ a = x + 1 ∧ b = y + 1) ↔
    (x + 1) * (y + 1) = n ∧ ¬n = 0

Proof state:
n x y : ℕ
⊢ ¬↑x * ↑y = -[n+1]

Tactic:
norm_cast

Result:
no goals

Proof state:
n x y : ℕ
⊢ ((∃ a b, (a * b = n ∧ ¬n = 0) ∧ False ∧ False) ∨ ∃ a b, (a * b = n ∧ ¬n = 0) ∧ a = x + 1 ∧ b = y + 1) ↔
    (x + 1) * (y + 1) = n ∧ ¬n = 0

Tactic:
simp +contextual [eq_comm]

Result:
no goals

Proof state:
n x y : ℕ
⊢ (-[x+1], -[y+1]) ∈ -[n+1].divisorsAntidiag ↔ (-[x+1], -[y+1]).1 * (-[x+1], -[y+1]).2 = -[n+1] ∧ -[n+1] ≠ 0

Tactic:
simp [divisorsAntidiag, negSucc_eq, -neg_add_rev]

Result:
n x y : ℕ
⊢ ((∃ a b, a * b = n + 1 ∧ ↑a = -(↑x + 1) ∧ ↑b = ↑y + 1) ∨ ∃ a b, a * b = n + 1 ∧ ↑a = ↑x + 1 ∧ ↑b = -(↑y + 1)) ↔
    (↑x + 1) * (↑y + 1) = -(↑n + 1) ∧ ¬↑n + 1 = 0

Proof state:
n x y : ℕ
⊢ ((∃ a b, a * b = n + 1 ∧ ↑a = -(↑x + 1) ∧ ↑b = ↑y + 1) ∨ ∃ a b, a * b = n + 1 ∧ ↑a = ↑x + 1 ∧ ↑b = -(↑y + 1)) ↔
    (↑x + 1) * (↑y + 1) = -(↑n + 1) ∧ ¬↑n + 1 = 0

Tactic:
norm_cast

Result:
n x y : ℕ
⊢ ((∃ a b, a * b = n + 1 ∧ False ∧ b = y + 1) ∨ ∃ a b, a * b = n + 1 ∧ a = x + 1 ∧ False) ↔ False ∧ ¬False

Proof state:
n x y : ℕ
⊢ x * y = n ∧ ¬n = 0 ∨ (0 = n ∧ ¬n = 0) ∧ x = 0 ∧ y = 0 ↔ ↑x * ↑y = ↑n ∧ ¬n = 0

Tactic:
norm_cast

Result:
n x y : ℕ
⊢ x * y = n ∧ ¬n = 0 ∨ (0 = n ∧ ¬n = 0) ∧ x = 0 ∧ y = 0 ↔ x * y = n ∧ ¬n = 0

Proof state:
n x y : ℕ
⊢ ((∃ a b, (a * b = n ∧ ¬n = 0) ∧ a = x ∧ ↑b = -(↑y + 1)) ∨
      ∃ a b, (a * b = n ∧ ¬n = 0) ∧ (a = 0 ∧ x = 0) ∧ ↑b = ↑y + 1) ↔
    -(↑x * (↑y + 1)) = ↑n ∧ ¬n = 0

Tactic:
norm_cast

Result:
n x y : ℕ
⊢ ((∃ a b, (a * b = n ∧ ¬n = 0) ∧ a = x ∧ False) ∨ ∃ a b, (a * b = n ∧ ¬n = 0) ∧ (a = 0 ∧ x = 0) ∧ b = y + 1) ↔
    (x * (y + 1) = 0 ∧ n = 0) ∧ ¬n = 0

Proof state:
n x y : ℕ
⊢ (↑x, ↑y) ∈ -[n+1].divisorsAntidiag ↔ (↑x, ↑y).1 * (↑x, ↑y).2 = -[n+1] ∧ -[n+1] ≠ 0

Tactic:
simp [divisorsAntidiag]

Result:
n x y : ℕ
⊢ ¬↑x * ↑y = -[n+1]

Proof state:
n x y : ℕ
⊢ ((∃ a b, (a * b = n ∧ ¬n = 0) ∧ a = x ∧ False) ∨ ∃ a b, (a * b = n ∧ ¬n = 0) ∧ (a = 0 ∧ x = 0) ∧ b = y + 1) ↔
    (x * (y + 1) = 0 ∧ n = 0) ∧ ¬n = 0

Tactic:
aesop

Result:
no goals

Proof state:
n x y : ℕ
⊢ (-[x+1], ↑y) ∈ (↑n).divisorsAntidiag ↔ (-[x+1], ↑y).1 * (-[x+1], ↑y).2 = ↑n ∧ ↑n ≠ 0

Tactic:
simp [divisorsAntidiag]

Result:
n x y : ℕ
⊢ (0 = n ∧ ¬n = 0) ∧ (∃ x_1, -↑x_1 = -[x+1]) ∧ y = 0 ↔ -((↑x + 1) * ↑y) = ↑n ∧ ¬n = 0

Proof state:
n x y : ℕ
⊢ ((∃ a b, a * b = n + 1 ∧ a = x ∧ ↑b = ↑y + 1) ∨ ∃ a b, a * b = n + 1 ∧ (a = 0 ∧ x = 0) ∧ ↑b = -(↑y + 1)) ↔
    ↑x * (↑y + 1) = ↑n + 1 ∧ ¬↑n + 1 = 0

Tactic:
norm_cast

Result:
n x y : ℕ
⊢ ((∃ a b, a * b = n + 1 ∧ a = x ∧ b = y + 1) ∨ ∃ a b, a * b = n + 1 ∧ (a = 0 ∧ x = 0) ∧ False) ↔
    x * (y + 1) = n + 1 ∧ ¬False

Proof state:
n x y : ℕ
⊢ (∃ a, a * y = n + 1 ∧ a = x + 1) ↔ (x + 1) * y = n + 1 ∧ ¬False

Tactic:
simp +contextual [eq_comm]

Result:
no goals

Proof state:
n x y : ℕ
⊢ (0 = n ∧ ¬n = 0) ∧ (∃ x_1, -↑x_1 = -[x+1]) ∧ y = 0 ↔ -((↑x + 1) * ↑y) = ↑n ∧ ¬n = 0

Tactic:
norm_cast

Result:
n x y : ℕ
⊢ (0 = n ∧ ¬n = 0) ∧ (∃ x_1, -↑x_1 = -[x+1]) ∧ y = 0 ↔ ((x + 1) * y = 0 ∧ n = 0) ∧ ¬n = 0

Proof state:
n x y : ℕ
⊢ ((∃ a b, a * b = n + 1 ∧ a = x ∧ b = y + 1) ∨ ∃ a b, a * b = n + 1 ∧ (a = 0 ∧ x = 0) ∧ False) ↔
    x * (y + 1) = n + 1 ∧ ¬False

Tactic:
aesop

Result:
no goals

Proof state:
n x y : ℕ
⊢ (↑x, -[y+1]) ∈ -[n+1].divisorsAntidiag ↔ (↑x, -[y+1]).1 * (↑x, -[y+1]).2 = -[n+1] ∧ -[n+1] ≠ 0

Tactic:
simp [divisorsAntidiag, negSucc_eq, -neg_add_rev]

Result:
n x y : ℕ
⊢ ((∃ a b, a * b = n + 1 ∧ a = x ∧ ↑b = ↑y + 1) ∨ ∃ a b, a * b = n + 1 ∧ (a = 0 ∧ x = 0) ∧ ↑b = -(↑y + 1)) ↔
    ↑x * (↑y + 1) = ↑n + 1 ∧ ¬↑n + 1 = 0

Proof state:
n x y : ℕ
⊢ (∃ a, a * y = n + 1 ∧ ↑a = ↑x + 1) ↔ (↑x + 1) * ↑y = ↑n + 1 ∧ ¬↑n + 1 = 0

Tactic:
norm_cast

Result:
n x y : ℕ
⊢ (∃ a, a * y = n + 1 ∧ a = x + 1) ↔ (x + 1) * y = n + 1 ∧ ¬False

Proof state:
n x y : ℕ
⊢ (0 = n ∧ ¬n = 0) ∧ (∃ x_1, -↑x_1 = -[x+1]) ∧ y = 0 ↔ ((x + 1) * y = 0 ∧ n = 0) ∧ ¬n = 0

Tactic:
aesop

Result:
no goals

Proof state:
n x y : ℕ
⊢ x * y = n ∧ ¬n = 0 ∨ (0 = n ∧ ¬n = 0) ∧ x = 0 ∧ y = 0 ↔ x * y = n ∧ ¬n = 0

Tactic:
simp +contextual [eq_comm]

Result:
no goals

Proof state:
n x y : ℕ
⊢ ((∃ a b, a * b = n + 1 ∧ False ∧ b = y + 1) ∨ ∃ a b, a * b = n + 1 ∧ a = x + 1 ∧ False) ↔ False ∧ ¬False

Tactic:
simp +contextual [eq_comm]

Result:
no goals

Proof state:
n x y : ℕ
⊢ (-[x+1], -[y+1]) ∈ (↑n).divisorsAntidiag ↔ (-[x+1], -[y+1]).1 * (-[x+1], -[y+1]).2 = ↑n ∧ ↑n ≠ 0

Tactic:
simp [divisorsAntidiag, negSucc_eq, -neg_add_rev]

Result:
n x y : ℕ
⊢ ((∃ a b, (a * b = n ∧ ¬n = 0) ∧ ↑a = -(↑x + 1) ∧ ↑b = -(↑y + 1)) ∨
      ∃ a b, (a * b = n ∧ ¬n = 0) ∧ ↑a = ↑x + 1 ∧ ↑b = ↑y + 1) ↔
    (↑x + 1) * (↑y + 1) = ↑n ∧ ¬n = 0

Proof state:
n x y : ℕ
⊢ (↑x, -[y+1]) ∈ (↑n).divisorsAntidiag ↔ (↑x, -[y+1]).1 * (↑x, -[y+1]).2 = ↑n ∧ ↑n ≠ 0

Tactic:
simp [divisorsAntidiag, negSucc_eq, -neg_add_rev]

Result:
n x y : ℕ
⊢ ((∃ a b, (a * b = n ∧ ¬n = 0) ∧ a = x ∧ ↑b = -(↑y + 1)) ∨
      ∃ a b, (a * b = n ∧ ¬n = 0) ∧ (a = 0 ∧ x = 0) ∧ ↑b = ↑y + 1) ↔
    -(↑x * (↑y + 1)) = ↑n ∧ ¬n = 0

Proof state:
n x y : ℕ
⊢ (↑x, ↑y) ∈ (↑n).divisorsAntidiag ↔ (↑x, ↑y).1 * (↑x, ↑y).2 = ↑n ∧ ↑n ≠ 0

Tactic:
simp [divisorsAntidiag]

Result:
n x y : ℕ
⊢ x * y = n ∧ ¬n = 0 ∨ (0 = n ∧ ¬n = 0) ∧ x = 0 ∧ y = 0 ↔ ↑x * ↑y = ↑n ∧ ¬n = 0