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

State before:
n : ℕ
hn : n ≠ 0
⊢ ∀
    b ∈
      filter
        (fun x =>
          match x with
          | (x, y) => x.lcm y = n)
        (n.divisors ×ˢ n.divisors),
    ∃ a, ∃ (ha : a ∈ finMulAntidiagonal 3 n), Nat.f a ha = b
Tactic:
intro b hb
State after:
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 ∈ finMulAntidiagonal 3 n), Nat.f a ha = b

State before:
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 ∈ finMulAntidiagonal 3 n), Nat.f a ha = b
Tactic:
dsimp only at hb
State after:
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

State before:
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
Tactic:
let g := b.fst.gcd b.snd
State after:
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

State before:
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
Tactic:
let a := ![g, b.fst/g, b.snd/g]
State after:
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 ∈ finMulAntidiagonal 3 n), Nat.f a ha = b

State before:
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, ∃ (ha : a ∈ finMulAntidiagonal 3 n), Nat.f a ha = b
Tactic:
use a
State after:
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
⊢ ∃ (ha : a ∈ finMulAntidiagonal 3 n), Nat.f a ha = b

State before:
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
⊢ ∃ (ha : a ∈ finMulAntidiagonal 3 n), Nat.f a ha = b
Tactic:
use ha
State after:
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

State before:
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
Tactic:
apply Prod.ext <;> simp only [Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons]
  <;> apply Nat.mul_div_cancel'
State after:
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

State before:
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 ∈ finMulAntidiagonal 3 n
Tactic:
rw [mem_finMulAntidiagonal]
State after:
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 (succ 0).succ.succ, a i = n ∧ n ≠ 0

State before:
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 (succ 0).succ.succ, a i = n ∧ n ≠ 0
Tactic:
rw [mem_filter, Finset.mem_product] at hb
State after:
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 (succ 0).succ.succ, a i = n ∧ n ≠ 0

State before:
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 (succ 0).succ.succ, a i = n ∧ n ≠ 0
Tactic:
refine ⟨?_, hn⟩
State after:
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 (succ 0).succ.succ, a i = n

State before:
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 (succ 0).succ.succ, a i = n
Tactic:
rw [Fin.prod_univ_three a]
State after:
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

State before:
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:
unfold_let a
State after:
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] 0 * ![g, b.1 / g, b.2 / g] 1 * ![g, b.1 / g, b.2 / g] 2 = n

State before:
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] 0 * ![g, b.1 / g, b.2 / g] 1 * ![g, b.1 / g, b.2 / g] 2 = n
Tactic:
simp only [Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons, Matrix.cons_val_two,
  Matrix.tail_cons]
State after:
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

State before:
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)]
State after:
no goals

State before:
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
Tactic:
apply Nat.gcd_dvd_left
State after:
no goals

State before:
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
Tactic:
apply Nat.gcd_dvd_right
State after:
no goals