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

State before:
d n p : ℕ
hn : Squarefree n
hp : p ∈ n.factors
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiagonal n
⊢ ∃! i, p ∣ f i
Tactic:
rw [mem_finMulAntidiagonal] at hf
State after:
d n p : ℕ
hn : Squarefree n
hp : p ∈ n.factors
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
⊢ ∃! i, p ∣ f i

State before:
d n p : ℕ
hn : Squarefree n
hp : p ∈ n.factors
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
⊢ ∃! i, p ∣ f i
Tactic:
rw [mem_factors hf.2, ← hf.1, hp.1.prime.dvd_finset_prod_iff] at hp
State after:
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : p.Prime ∧ ∃ a ∈ univ, p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
⊢ ∃! i, p ∣ f i

State before:
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : p.Prime ∧ ∃ 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
State after:
case intro.intro
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : p.Prime ∧ ∃ 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

State before:
case intro.intro
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : p.Prime ∧ ∃ 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, ?_⟩
State after:
case intro.intro
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : p.Prime ∧ ∃ 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

State before:
case intro.intro
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : p.Prime ∧ ∃ 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
State after:
case intro.intro
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : p.Prime ∧ ∃ 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

State before:
case intro.intro
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : p.Prime ∧ ∃ 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
State after:
case intro.intro
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : p.Prime ∧ ∃ 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

State before:
case intro.intro
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : p.Prime ∧ ∃ 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⟩
State after:
case intro.intro
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : p.Prime ∧ ∃ 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)

State before:
case intro.intro
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : p.Prime ∧ ∃ 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
State after:
case intro.intro.h
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : p.Prime ∧ ∃ 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)

State before:
case intro.intro.h
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : p.Prime ∧ ∃ 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
State after:
case intro.intro.h
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : p.Prime ∧ ∃ 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

State before:
case intro.intro.h
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : p.Prime ∧ ∃ 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]
State after:
case intro.intro.h
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : p.Prime ∧ ∃ 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

State before:
case intro.intro.h
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : p.Prime ∧ ∃ 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
State after:
no goals