-- Mathlib/Algebra/Order/Antidiag/Nat.lean
theorem f_img {n : ℕ} (hn : Squarefree n) (a : Fin 3 → ℕ)
    (ha : a ∈ finMulAntidiag 3 n) :
    f a ha ∈ Finset.filter (fun ⟨x, y⟩ => x.lcm y = n) (n.divisors ×ˢ n.divisors)

Proof state:
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ a 0 * a 1 * a 2 = a 1 * a 2 * a 0

Tactic:
ring

Result:
no goals

Proof state:
case refine_2
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (a 0 * a 1, a 0 * a 2).2 ∣ a 0 * a 1 * a 2

Tactic:
use a 1

Result:
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ a 0 * a 1 * a 2 = (a 0 * a 1, a 0 * a 2).2 * a 1

Proof state:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ match (a 0 * a 1, a 0 * a 2) with
  | (x, y) => x.lcm y = a 0 * a 1 * a 2

Tactic:
dsimp only

Result:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (a 0 * a 1).lcm (a 0 * a 2) = a 0 * a 1 * a 2

Proof state:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (a 0 * a 1).lcm (a 0 * a 2) = a 0 * a 1 * a 2

Tactic:
rw [lcm_mul_left, Nat.Coprime.lcm_eq_mul]

Result:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ a 0 * (a 1 * a 2) = a 0 * a 1 * a 2

case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (a 1).Coprime (a 2)

Proof state:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ a 1 * a 2 ∣ n

Tactic:
use a 0

Result:
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ n = a 1 * a 2 * a 0

Proof state:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (((Nat.card_pair_lcm_eq.f a ha).1 ∣ n ∧ n ≠ 0) ∧ (Nat.card_pair_lcm_eq.f a ha).2 ∣ n ∧ n ≠ 0) ∧
    match Nat.card_pair_lcm_eq.f a ha with
    | (x, y) => x.lcm y = n

Tactic:
refine ⟨⟨⟨?_, hn.ne_zero⟩, ⟨?_, hn.ne_zero⟩⟩, ?_⟩ <;> rw [f, ← finMulAntidiag_three a ha]

Result:
case refine_1
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (a 0 * a 1, a 0 * a 2).1 ∣ a 0 * a 1 * a 2

case refine_2
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (a 0 * a 1, a 0 * a 2).2 ∣ a 0 * a 1 * a 2

case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ match (a 0 * a 1, a 0 * a 2) with
  | (x, y) => x.lcm y = a 0 * a 1 * a 2

Proof state:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (a 1).Coprime (a 2)

Tactic:
refine coprime_of_squarefree_mul (hn.squarefree_of_dvd ?_)

Result:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ a 1 * a 2 ∣ n

Proof state:
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ n = a 1 * a 2 * a 0

Tactic:
rw [← finMulAntidiag_three a ha]

Result:
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ a 0 * a 1 * a 2 = a 1 * a 2 * a 0

Proof state:
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ a 0 * a 1 * a 2 = (a 0 * a 1, a 0 * a 2).2 * a 1

Tactic:
ring

Result:
no goals

Proof state:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ Nat.card_pair_lcm_eq.f a ha ∈
    filter
      (fun x =>
        match x with
        | (x, y) => x.lcm y = n)
      (n.divisors ×ˢ n.divisors)

Tactic:
rw [mem_filter, Finset.mem_product, mem_divisors, mem_divisors]

Result:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (((Nat.card_pair_lcm_eq.f a ha).1 ∣ n ∧ n ≠ 0) ∧ (Nat.card_pair_lcm_eq.f a ha).2 ∣ n ∧ n ≠ 0) ∧
    match Nat.card_pair_lcm_eq.f a ha with
    | (x, y) => x.lcm y = n

Proof state:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ a 0 * (a 1 * a 2) = a 0 * a 1 * a 2

Tactic:
ring

Result:
no goals

Proof state:
case refine_1
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ (a 0 * a 1, a 0 * a 2).1 ∣ a 0 * a 1 * a 2

Tactic:
apply dvd_mul_right

Result:
no goals