apply Prod.ext <;> simp only [Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons]
  <;> apply Nat.mul_div_cancel'
case h
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 : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : a ∈ finMulAntidiagonal 3 n
⊢ Nat.f a ha = b
case h.a.H
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 : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 0 ∣ b.1

case h.a.H
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 : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 0 ∣ b.2