let g := b.fst.gcd b.snd
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ filter (fun x => x.1.lcm x.2 = n) (n.divisors ×ˢ n.divisors)
⊢ ∃ a, ∃ (ha : a ∈ finMulAntidiagonal 3 n), Nat.f a ha = b
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ filter (fun x => x.1.lcm x.2 = n) (n.divisors ×ˢ n.divisors)
g : ℕ := b.1.gcd b.2
⊢ ∃ a, ∃ (ha : a ∈ finMulAntidiagonal 3 n), Nat.f a ha = b