-- Mathlib/Algebra/Order/Antidiag/Nat.lean
lemma finMulAntidiag_existsUnique_prime_dvd {d n p : ℕ} (hn : Squarefree n)
    (hp : p ∈ n.primeFactorsList) (f : Fin d → ℕ) (hf : f ∈ finMulAntidiag d n) :
    ∃! i, p ∣ f i

Proof state:
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
⊢ ∃! i, p ∣ f i

Tactic:
obtain ⟨i, his, hi⟩ := hp.2

Result:
case intro.intro
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : i ∈ univ
hi : p ∣ f i
⊢ ∃! i, p ∣ f i

Proof state:
case intro.intro
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : i ∈ univ
hi : p ∣ f i
⊢ ∀ (y : Fin d), (fun i => p ∣ f i) y → y = i

Tactic:
intro j hj

Result:
case intro.intro
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : i ∈ univ
hi : p ∣ f i
j : Fin d
hj : p ∣ f j
⊢ j = i

Proof state:
case intro.intro
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : i ∈ univ
hi : p ∣ f i
⊢ ∃! i, p ∣ f i

Tactic:
refine ⟨i, hi, ?_⟩

Result:
case intro.intro
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : i ∈ univ
hi : p ∣ f i
⊢ ∀ (y : Fin d), (fun i => p ∣ f i) y → y = i

Proof state:
d n p : ℕ
hn : Squarefree n
hp : p ∈ n.primeFactorsList
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
⊢ ∃! i, p ∣ f i

Tactic:
rw [mem_primeFactorsList hf.2, ← hf.1, hp.1.prime.dvd_finset_prod_iff] at hp

Result:
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
⊢ ∃! i, p ∣ f i

Proof state:
case intro.intro
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : i ∈ univ
hi : p ∣ f i
j : Fin d
hj : p ∣ f j
⊢ j = i

Tactic:
by_contra hij

Result:
case intro.intro
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : i ∈ univ
hi : p ∣ f i
j : Fin d
hj : p ∣ f j
hij : ¬j = i
⊢ False

Proof state:
case intro.intro.h
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : i ∈ univ
hi : p ∣ f i
j : Fin d
hj : p ∣ f j
hij : ¬j = i
⊢ f i * f j ∣ n

Tactic:
rw [← hf.1, ← Finset.mul_prod_erase _ _ his,
  ← Finset.mul_prod_erase _ _ (mem_erase.mpr ⟨hij, mem_univ _⟩), ← mul_assoc]

Result:
case intro.intro.h
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : i ∈ univ
hi : p ∣ f i
j : Fin d
hj : p ∣ f j
hij : ¬j = i
⊢ f i * f j ∣ f i * f j * ∏ x ∈ (univ.erase i).erase j, f x

Proof state:
case intro.intro.h
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : i ∈ univ
hi : p ∣ f i
j : Fin d
hj : p ∣ f j
hij : ¬j = i
⊢ Squarefree (f i * f j)

Tactic:
apply hn.squarefree_of_dvd

Result:
case intro.intro.h
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : i ∈ univ
hi : p ∣ f i
j : Fin d
hj : p ∣ f j
hij : ¬j = i
⊢ f i * f j ∣ n

Proof state:
d n p : ℕ
hn : Squarefree n
hp : p ∈ n.primeFactorsList
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiag n
⊢ ∃! i, p ∣ f i

Tactic:
rw [mem_finMulAntidiag] at hf

Result:
d n p : ℕ
hn : Squarefree n
hp : p ∈ n.primeFactorsList
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
⊢ ∃! i, p ∣ f i

Proof state:
case intro.intro
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : i ∈ univ
hi : p ∣ f i
j : Fin d
hj : p ∣ f j
hij : ¬j = i
⊢ False

Tactic:
apply Nat.Prime.not_coprime_iff_dvd.mpr ⟨p, hp.1, hi, hj⟩

Result:
case intro.intro
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : i ∈ univ
hi : p ∣ f i
j : Fin d
hj : p ∣ f j
hij : ¬j = i
⊢ (f i).Coprime (f j)

Proof state:
case intro.intro
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : i ∈ univ
hi : p ∣ f i
j : Fin d
hj : p ∣ f j
hij : ¬j = i
⊢ (f i).Coprime (f j)

Tactic:
apply Nat.coprime_of_squarefree_mul

Result:
case intro.intro.h
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : i ∈ univ
hi : p ∣ f i
j : Fin d
hj : p ∣ f j
hij : ¬j = i
⊢ Squarefree (f i * f j)

Proof state:
case intro.intro.h
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : i ∈ univ
hi : p ∣ f i
j : Fin d
hj : p ∣ f j
hij : ¬j = i
⊢ f i * f j ∣ f i * f j * ∏ x ∈ (univ.erase i).erase j, f x

Tactic:
apply Nat.dvd_mul_right

Result:
no goals