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

Proof state:
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]
⊢ ∏ i : Fin 3, a i = n ∧ n ≠ 0

Tactic:
rw [mem_filter, Finset.mem_product] at hb

Result:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ ∏ i : Fin 3, a i = n ∧ n ≠ 0

Proof state:
case h.fst.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 ∈ finMulAntidiag 3 n
⊢ a 0 ∣ b.1

Tactic:
apply Nat.gcd_dvd_left

Result:
no goals

Proof state:
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 ∈ finMulAntidiag 3 n
⊢ ∃ (ha : a ∈ finMulAntidiag 3 n), Nat.card_pair_lcm_eq.f a ha = b

Tactic:
use ha

Result:
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 ∈ finMulAntidiag 3 n
⊢ Nat.card_pair_lcm_eq.f a ha = b

Proof state:
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 ∈ finMulAntidiag 3 n), Nat.card_pair_lcm_eq.f a ha = b

Tactic:
let a := ![g, b.fst/g, b.snd/g]

Result:
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]
⊢ ∃ a, ∃ (ha : a ∈ finMulAntidiag 3 n), Nat.card_pair_lcm_eq.f a ha = b

Proof state:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ a 0 * a 1 * a 2 = n

Tactic:
simp only [a, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons,
Matrix.cons_val_two, Matrix.tail_cons]

Result:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ g * (b.1 / g) * (b.2 / g) = n

Proof state:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ filter (fun x => x.1.lcm x.2 = n) (n.divisors ×ˢ n.divisors)
⊢ ∃ a, ∃ (ha : a ∈ finMulAntidiag 3 n), Nat.card_pair_lcm_eq.f a ha = b

Tactic:
let g := b.fst.gcd b.snd

Result:
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 ∈ finMulAntidiag 3 n), Nat.card_pair_lcm_eq.f a ha = b

Proof state:
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]
⊢ a ∈ finMulAntidiag 3 n

Tactic:
rw [mem_finMulAntidiag]

Result:
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]
⊢ ∏ i : Fin 3, a i = n ∧ n ≠ 0

Proof state:
case h.snd.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 ∈ finMulAntidiag 3 n
⊢ a 0 ∣ b.2

Tactic:
apply Nat.gcd_dvd_right

Result:
no goals

Proof state:
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 ∈ finMulAntidiag 3 n
⊢ Nat.card_pair_lcm_eq.f a ha = b

Tactic:
apply Prod.ext <;> simp only [Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons]
  <;> apply Nat.mul_div_cancel'

Result:
case h.fst.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 ∈ finMulAntidiag 3 n
⊢ a 0 ∣ b.1

case h.snd.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 ∈ finMulAntidiag 3 n
⊢ a 0 ∣ b.2

Proof state:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ g * (b.1 / g) * (b.2 / g) = n

Tactic:
rw [Nat.mul_div_cancel_left' (Nat.gcd_dvd_left _ _), ← hb.2, lcm,
  Nat.mul_div_assoc b.fst (Nat.gcd_dvd_right b.fst b.snd)]

Result:
no goals

Proof state:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ ∏ i : Fin 3, a i = n

Tactic:
rw [Fin.prod_univ_three a]

Result:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ a 0 * a 1 * a 2 = n

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

Tactic:
dsimp only at hb

Result:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : b ∈ filter (fun x => x.1.lcm x.2 = n) (n.divisors ×ˢ n.divisors)
⊢ ∃ a, ∃ (ha : a ∈ finMulAntidiag 3 n), Nat.card_pair_lcm_eq.f a ha = b

Proof state:
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 ∈ finMulAntidiag 3 n
⊢ ∃ a, ∃ (ha : a ∈ finMulAntidiag 3 n), Nat.card_pair_lcm_eq.f a ha = b

Tactic:
use a

Result:
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 ∈ finMulAntidiag 3 n
⊢ ∃ (ha : a ∈ finMulAntidiag 3 n), Nat.card_pair_lcm_eq.f a ha = b

Proof state:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ ∏ i : Fin 3, a i = n ∧ n ≠ 0

Tactic:
refine ⟨?_, hn⟩

Result:
n : ℕ
hn : n ≠ 0
b : ℕ × ℕ
hb : (b.1 ∈ n.divisors ∧ b.2 ∈ n.divisors) ∧ b.1.lcm b.2 = n
g : ℕ := b.1.gcd b.2
a : Fin (succ 0).succ.succ → ℕ := ![g, b.1 / g, b.2 / g]
⊢ ∏ i : Fin 3, a i = n