-- Mathlib/Algebra/Order/Antidiag/Nat.lean
theorem primeFactorsPiBij_surj (d n : ℕ) (hn : Squarefree n)
    (t : Fin d → ℕ) (ht : t ∈ finMulAntidiag d n) : ∃ (g : _)
    (hg : g ∈ pi n.primeFactors fun _ => univ), Nat.primeFactorsPiBij d n g hg = t

Proof state:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ ∏ p ∈ filter (fun p => f ↑p ⋯ = i) n.primeFactors.attach, ↑p =
    ∏ a ∈ filter (fun a => ↑a ∣ t i) n.primeFactors.attach, ↑a

Tactic:
congr

Result:
case e_s.e_p
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ (fun p => f ↑p ⋯ = i) = fun a => ↑a ∣ t i

Proof state:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ ∏ a ∈ filter (fun a => a ∣ t i) n.primeFactors, a = t i

Tactic:
rw [primeFactors_filter_dvd_of_dvd hn.ne_zero this]

Result:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ ∏ a ∈ (t i).primeFactors, a = t i

Proof state:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
existsUnique : ∀ p ∈ n.primeFactors, ∃! i, p ∣ t i
⊢ ∃ g, ∃ (hg : g ∈ n.primeFactors.pi fun x => univ), Nat.primeFactorsPiBij d n g hg = t

Tactic:
choose f hf hf_unique using existsUnique

Result:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
⊢ ∃ g, ∃ (hg : g ∈ n.primeFactors.pi fun x => univ), Nat.primeFactorsPiBij d n g hg = t

Proof state:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
p : ℕ
hp : p ∈ n.primeFactors
this : t (f ↑⟨p, hp⟩ ⋯) ∣ n
⊢ ↑⟨p, hp⟩ ∣ t (f ↑⟨p, hp⟩ ⋯)

Tactic:
apply hf

Result:
no goals

Proof state:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
⊢ ∃ g, ∃ (hg : g ∈ n.primeFactors.pi fun x => univ), Nat.primeFactorsPiBij d n g hg = t

Tactic:
have existsUnique := fun (p : ℕ) (hp : p ∈ n.primeFactors) =>
  (finMulAntidiag_existsUnique_prime_dvd hn
    (mem_primeFactors_iff_mem_primeFactorsList.mp hp) t ht)

Result:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
existsUnique : ∀ p ∈ n.primeFactors, ∃! i, p ∣ t i
⊢ ∃ g, ∃ (hg : g ∈ n.primeFactors.pi fun x => univ), Nat.primeFactorsPiBij d n g hg = t

Proof state:
case refine_2.h
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
⊢ Nat.primeFactorsPiBij d n f ⋯ i = t i

Tactic:
have : t i ∣ n := dvd_of_mem_finMulAntidiag ht _

Result:
case refine_2.h
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ Nat.primeFactorsPiBij d n f ⋯ i = t i

Proof state:
case e_s.e_p.h.mk.a
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i => p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i => p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
p : ℕ
hp : p ∈ n.primeFactors
⊢ f ↑⟨p, hp⟩ ⋯ = i ↔ ↑⟨p, hp⟩ ∣ t i

Tactic:
refine ⟨by rintro rfl; apply hf, fun h => (hf_unique p hp i h).symm⟩

Result:
no goals