Theorem: Nat.f_img (PrimeNumberTheoremAnd/Mathlib/Data/Nat/FinMulAntidiagonal.lean)

State before:
n : ℕ
hn : Squarefree n
⊢ ∀ (a : Fin 3 → ℕ) (ha : a ∈ finMulAntidiagonal 3 n),
    Nat.f a ha ∈
      filter
        (fun x =>
          match x with
          | (x, y) => x.lcm y = n)
        (n.divisors ×ˢ n.divisors)
Tactic:
intro a ha
State after:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ Nat.f a ha ∈
    filter
      (fun x =>
        match x with
        | (x, y) => x.lcm y = n)
      (n.divisors ×ˢ n.divisors)

State before:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ Nat.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, Nat.f]
State after:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ (((a 0 * a 1, a 0 * a 2).1 ∣ n ∧ n ≠ 0) ∧ (a 0 * a 1, a 0 * a 2).2 ∣ n ∧ n ≠ 0) ∧
    match (a 0 * a 1, a 0 * a 2) with
    | (x, y) => x.lcm y = n

State before:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ (((a 0 * a 1, a 0 * a 2).1 ∣ n ∧ n ≠ 0) ∧ (a 0 * a 1, a 0 * a 2).2 ∣ n ∧ n ≠ 0) ∧
    match (a 0 * a 1, a 0 * a 2) with
    | (x, y) => x.lcm y = n
Tactic:
refine ⟨⟨⟨?_, hn.ne_zero⟩, ⟨?_, hn.ne_zero⟩⟩, ?_⟩ <;> rw [←finMulAntidiagonal_three a ha]
State after:
case refine_1
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 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 ∈ finMulAntidiagonal 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 ∈ finMulAntidiagonal 3 n
⊢ match (a 0 * a 1, a 0 * a 2) with
  | (x, y) => x.lcm y = a 0 * a 1 * a 2

State before:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 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
State after:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ (a 0 * a 1).lcm (a 0 * a 2) = a 0 * a 1 * a 2

State before:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 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]
State after:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 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 ∈ finMulAntidiagonal 3 n
⊢ (a 1).Coprime (a 2)

State before:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ (a 1).Coprime (a 2)
Tactic:
refine coprime_of_squarefree_mul (hn.squarefree_of_dvd ?_)
State after:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 1 * a 2 ∣ n

State before:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 1 * a 2 ∣ n
Tactic:
use a 0
State after:
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ n = a 1 * a 2 * a 0

State before:
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ n = a 1 * a 2 * a 0
Tactic:
rw [←finMulAntidiagonal_three a ha]
State after:
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 0 * a 1 * a 2 = a 1 * a 2 * a 0

State before:
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 0 * a 1 * a 2 = a 1 * a 2 * a 0
Tactic:
ring
State after:
no goals

State before:
case refine_1
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ (a 0 * a 1, a 0 * a 2).1 ∣ a 0 * a 1 * a 2
Tactic:
apply dvd_mul_right _ (a 2)
State after:
no goals

State before:
case refine_2
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ (a 0 * a 1, a 0 * a 2).2 ∣ a 0 * a 1 * a 2
Tactic:
use a 1
State after:
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 0 * a 1 * a 2 = (a 0 * a 1, a 0 * a 2).2 * a 1

State before:
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 0 * a 1 * a 2 = (a 0 * a 1, a 0 * a 2).2 * a 1
Tactic:
ring
State after:
no goals

State before:
case refine_3
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiagonal 3 n
⊢ a 0 * (a 1 * a 2) = a 0 * a 1 * a 2
Tactic:
ring
State after:
no goals