n : ℕ
x : ℕ × ℕ
⊢ ((1 ≤ x.fst ∧ x.fst < n + 1) ∧ 1 ≤ x.snd ∧ x.snd < n + 1) ∧ x.fst * x.snd = n ↔ x.fst * x.snd = n ∧ ¬n = 0
n : ℕ
x : ℕ × ℕ
⊢ x ∈ divisorsAntidiagonal n ↔ x.fst * x.snd = n ∧ n ≠ 0
simp only [divisorsAntidiagonal, Finset.mem_Ico, Ne.def, Finset.mem_filter, Finset.mem_product]
n : ℕ
x : ℕ × ℕ
⊢ x.fst * x.snd = n ∧ (1 ≤ x.fst ∧ x.fst < n + 1) ∧ 1 ≤ x.snd ∧ x.snd < n + 1 ↔ x.fst * x.snd = n ∧ ¬n = 0
n : ℕ
x : ℕ × ℕ
⊢ ((1 ≤ x.fst ∧ x.fst < n + 1) ∧ 1 ≤ x.snd ∧ x.snd < n + 1) ∧ x.fst * x.snd = n ↔ x.fst * x.snd = n ∧ ¬n = 0
rw [and_comm]
case h
n : ℕ
x : ℕ × ℕ
⊢ x.fst * x.snd = n → ((1 ≤ x.fst ∧ x.fst < n + 1) ∧ 1 ≤ x.snd ∧ x.snd < n + 1 ↔ ¬n = 0)
n : ℕ
x : ℕ × ℕ
⊢ x.fst * x.snd = n ∧ (1 ≤ x.fst ∧ x.fst < n + 1) ∧ 1 ≤ x.snd ∧ x.snd < n + 1 ↔ x.fst * x.snd = n ∧ ¬n = 0
apply and_congr_right
case h
x : ℕ × ℕ
⊢ (1 ≤ x.fst ∧ x.fst < x.fst * x.snd + 1) ∧ 1 ≤ x.snd ∧ x.snd < x.fst * x.snd + 1 ↔ ¬x.fst * x.snd = 0
case h
n : ℕ
x : ℕ × ℕ
⊢ x.fst * x.snd = n → ((1 ≤ x.fst ∧ x.fst < n + 1) ∧ 1 ≤ x.snd ∧ x.snd < n + 1 ↔ ¬n = 0)
rintro rfl
case h.mp
x : ℕ × ℕ
h : (1 ≤ x.fst ∧ x.fst < x.fst * x.snd + 1) ∧ 1 ≤ x.snd ∧ x.snd < x.fst * x.snd + 1
⊢ ¬x.fst * x.snd = 0

case h.mpr
x : ℕ × ℕ
h : ¬x.fst * x.snd = 0
⊢ (1 ≤ x.fst ∧ x.fst < x.fst * x.snd + 1) ∧ 1 ≤ x.snd ∧ x.snd < x.fst * x.snd + 1
case h
x : ℕ × ℕ
⊢ (1 ≤ x.fst ∧ x.fst < x.fst * x.snd + 1) ∧ 1 ≤ x.snd ∧ x.snd < x.fst * x.snd + 1 ↔ ¬x.fst * x.snd = 0
constructor <;> intro h
case h.mp
x : ℕ × ℕ
h : x.fst * x.snd = 0
⊢ 1 ≤ x.fst ∧ x.fst < x.fst * x.snd + 1 → 1 ≤ x.snd → x.fst * x.snd + 1 ≤ x.snd
case h.mp
x : ℕ × ℕ
h : (1 ≤ x.fst ∧ x.fst < x.fst * x.snd + 1) ∧ 1 ≤ x.snd ∧ x.snd < x.fst * x.snd + 1
⊢ ¬x.fst * x.snd = 0
contrapose! h
no goals
case h.mp
x : ℕ × ℕ
h : x.fst * x.snd = 0
⊢ 1 ≤ x.fst ∧ x.fst < x.fst * x.snd + 1 → 1 ≤ x.snd → x.fst * x.snd + 1 ≤ x.snd
simp [h]
case h.mpr
x : ℕ × ℕ
h : ¬x.fst * x.snd = 0
⊢ (1 ≤ x.fst ∧ x.fst ≤ x.fst * x.snd) ∧ 1 ≤ x.snd ∧ x.snd ≤ x.fst * x.snd
case h.mpr
x : ℕ × ℕ
h : ¬x.fst * x.snd = 0
⊢ (1 ≤ x.fst ∧ x.fst < x.fst * x.snd + 1) ∧ 1 ≤ x.snd ∧ x.snd < x.fst * x.snd + 1
rw [Nat.lt_add_one_iff, Nat.lt_add_one_iff]
case h.mpr
x : ℕ × ℕ
h : ¬x.fst = 0 ∧ ¬x.snd = 0
⊢ (1 ≤ x.fst ∧ x.fst ≤ x.fst * x.snd) ∧ 1 ≤ x.snd ∧ x.snd ≤ x.fst * x.snd
case h.mpr
x : ℕ × ℕ
h : ¬x.fst * x.snd = 0
⊢ (1 ≤ x.fst ∧ x.fst ≤ x.fst * x.snd) ∧ 1 ≤ x.snd ∧ x.snd ≤ x.fst * x.snd
rw [mul_eq_zero, not_or] at h
case h.mpr
x : ℕ × ℕ
h : ¬x.fst = 0 ∧ ¬x.snd = 0
⊢ x.fst ≤ x.fst * x.snd ∧ x.snd ≤ x.fst * x.snd
case h.mpr
x : ℕ × ℕ
h : ¬x.fst = 0 ∧ ¬x.snd = 0
⊢ (1 ≤ x.fst ∧ x.fst ≤ x.fst * x.snd) ∧ 1 ≤ x.snd ∧ x.snd ≤ x.fst * x.snd
simp only [succ_le_of_lt (Nat.pos_of_ne_zero h.1), succ_le_of_lt (Nat.pos_of_ne_zero h.2),
  true_and_iff]
no goals
case h.mpr
x : ℕ × ℕ
h : ¬x.fst = 0 ∧ ¬x.snd = 0
⊢ x.fst ≤ x.fst * x.snd ∧ x.snd ≤ x.fst * x.snd
exact
  ⟨le_mul_of_pos_right (Nat.pos_of_ne_zero h.2), le_mul_of_pos_left (Nat.pos_of_ne_zero h.1)⟩