internlm/Lean-Github huggingface dataset:
Theorem: Nat.finMulAntidiagonal_exists_unique_prime_dvd
Proof 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
Proof 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
Theorem: Nat.finMulAntidiagonal_exists_unique_prime_dvd
Proof 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
Proof 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
Theorem: Nat.finMulAntidiagonal_exists_unique_prime_dvd
Proof 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, ?_⟩
Proof 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
Theorem: Nat.finMulAntidiagonal_exists_unique_prime_dvd
Proof 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
Proof 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
Theorem: Nat.finMulAntidiagonal_exists_unique_prime_dvd
Proof 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
Proof 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
Theorem: Nat.finMulAntidiagonal_exists_unique_prime_dvd
Proof 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⟩
Proof 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)
Theorem: Nat.finMulAntidiagonal_exists_unique_prime_dvd
Proof 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
Proof 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)
Theorem: Nat.finMulAntidiagonal_exists_unique_prime_dvd
Proof 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
Proof 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
Theorem: Nat.finMulAntidiagonal_exists_unique_prime_dvd
Proof 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]
Proof 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
Theorem: Nat.finMulAntidiagonal_exists_unique_prime_dvd
Proof 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
Proof state after:
no goals
Theorem: Nat.primeFactorsPiBij_img
Proof state before:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ Nat.primeFactorsPiBij d n f hf ∈ d.finMulAntidiagonal n
Tactic:
rw [mem_finMulAntidiagonal]
Proof state after:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∏ i : Fin d, Nat.primeFactorsPiBij d n f hf i = n ∧ n ≠ 0
Theorem: Nat.primeFactorsPiBij_img
Proof state before:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∏ i : Fin d, Nat.primeFactorsPiBij d n f hf i = n ∧ n ≠ 0
Tactic:
refine ⟨?_, hn.ne_zero⟩
Proof state after:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∏ i : Fin d, Nat.primeFactorsPiBij d n f hf i = n
Theorem: Nat.primeFactorsPiBij_img
Proof state before:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∏ i : Fin d, Nat.primeFactorsPiBij d n f hf i = n
Tactic:
unfold Nat.primeFactorsPiBij
Proof state after:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∏ i : Fin d, ∏ p ∈ filter (fun p => f ↑p ⋯ = i) n.primeFactors.attach, ↑p = n
Theorem: Nat.primeFactorsPiBij_img
Proof state before:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∏ i : Fin d, ∏ p ∈ filter (fun p => f ↑p ⋯ = i) n.primeFactors.attach, ↑p = n
Tactic:
rw [prod_fiberwise_of_maps_to, prod_attach (f := fun x => x)]
Proof state after:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∏ x ∈ n.primeFactors, x = n

case h
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∀ i ∈ n.primeFactors.attach, f ↑i ⋯ ∈ univ
Theorem: Nat.primeFactorsPiBij_img
Proof state before:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∏ x ∈ n.primeFactors, x = n

case h
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∀ i ∈ n.primeFactors.attach, f ↑i ⋯ ∈ univ
Tactic:
apply prod_primeFactors_of_squarefree hn
Proof state after:
case h
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∀ i ∈ n.primeFactors.attach, f ↑i ⋯ ∈ univ
Theorem: Nat.primeFactorsPiBij_img
Proof state before:
case h
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
⊢ ∀ i ∈ n.primeFactors.attach, f ↑i ⋯ ∈ univ
Tactic:
apply fun _ _ => mem_univ _
Proof state after:
no goals
Theorem: Nat.primeFactorsPiBij_inj
Proof state before:
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
⊢ Nat.primeFactorsPiBij d n f hf = Nat.primeFactorsPiBij d n g hg → f = g
Tactic:
contrapose!
Proof state after:
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
⊢ f ≠ g → Nat.primeFactorsPiBij d n f hf ≠ Nat.primeFactorsPiBij d n g hg
Theorem: Nat.primeFactorsPiBij_inj
Proof state before:
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
⊢ f ≠ g → Nat.primeFactorsPiBij d n f hf ≠ Nat.primeFactorsPiBij d n g hg
Tactic:
simp_rw [Function.ne_iff]
Proof state after:
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
⊢ (∃ a, ∃ (a_1 : a ∈ n.primeFactors), f a a_1 ≠ g a a_1) →
    ∃ a, Nat.primeFactorsPiBij d n f hf a ≠ Nat.primeFactorsPiBij d n g hg a
Theorem: Nat.primeFactorsPiBij_inj
Proof state before:
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
⊢ (∃ a, ∃ (a_1 : a ∈ n.primeFactors), f a a_1 ≠ g a a_1) →
    ∃ a, Nat.primeFactorsPiBij d n f hf a ≠ Nat.primeFactorsPiBij d n g hg a
Tactic:
intro ⟨p, hp, hfg⟩
Proof state after:
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ ∃ a, Nat.primeFactorsPiBij d n f hf a ≠ Nat.primeFactorsPiBij d n g hg a
Theorem: Nat.primeFactorsPiBij_inj
Proof state before:
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ ∃ a, Nat.primeFactorsPiBij d n f hf a ≠ Nat.primeFactorsPiBij d n g hg a
Tactic:
use f p hp
Proof state after:
case h
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ Nat.primeFactorsPiBij d n f hf (f p hp) ≠ Nat.primeFactorsPiBij d n g hg (f p hp)
Theorem: Nat.primeFactorsPiBij_inj
Proof state before:
case h
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ Nat.primeFactorsPiBij d n f hf (f p hp) ≠ Nat.primeFactorsPiBij d n g hg (f p hp)
Tactic:
dsimp only [Nat.primeFactorsPiBij]
Proof state after:
case h
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ ∏ p ∈ filter (fun p_1 => f ↑p_1 ⋯ = f p hp) n.primeFactors.attach, ↑p ≠
    ∏ p ∈ filter (fun p_1 => g ↑p_1 ⋯ = f p hp) n.primeFactors.attach, ↑p
Theorem: Nat.primeFactorsPiBij_inj
Proof state before:
case h
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ ∏ p ∈ filter (fun p_1 => f ↑p_1 ⋯ = f p hp) n.primeFactors.attach, ↑p ≠
    ∏ p ∈ filter (fun p_1 => g ↑p_1 ⋯ = f p hp) n.primeFactors.attach, ↑p
Tactic:
apply ne_of_mem_of_not_mem (s:= ({x | (p ∣ x)}:Set ℕ)) <;> simp_rw [Set.mem_setOf_eq]
Proof state after:
case h.h
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ p ∣ ∏ p ∈ filter (fun p_1 => f ↑p_1 ⋯ = f p hp) n.primeFactors.attach, ↑p

case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ ¬p ∣ ∏ p ∈ filter (fun p_1 => g ↑p_1 ⋯ = f p hp) n.primeFactors.attach, ↑p
Theorem: Nat.primeFactorsPiBij_inj
Proof state before:
case h.h
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ p ∣ ∏ p ∈ filter (fun p_1 => f ↑p_1 ⋯ = f p hp) n.primeFactors.attach, ↑p
Tactic:
rw [Finset.prod_filter]
Proof state after:
case h.h
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ p ∣ ∏ a ∈ n.primeFactors.attach, if f ↑a ⋯ = f p hp then ↑a else 1
Theorem: Nat.primeFactorsPiBij_inj
Proof state before:
case h.h
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ p ∣ ∏ a ∈ n.primeFactors.attach, if f ↑a ⋯ = f p hp then ↑a else 1
Tactic:
convert Finset.dvd_prod_of_mem _ (mem_attach (n.primeFactors) ⟨p, hp⟩)
Proof state after:
case h.e'_3
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ p = if f ↑⟨p, hp⟩ ⋯ = f p hp then ↑⟨p, hp⟩ else 1
Theorem: Nat.primeFactorsPiBij_inj
Proof state before:
case h.e'_3
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ p = if f ↑⟨p, hp⟩ ⋯ = f p hp then ↑⟨p, hp⟩ else 1
Tactic:
rw [if_pos rfl]
Proof state after:
no goals
Theorem: Nat.primeFactorsPiBij_inj
Proof state before:
case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ ¬p ∣ ∏ p ∈ filter (fun p_1 => g ↑p_1 ⋯ = f p hp) n.primeFactors.attach, ↑p
Tactic:
rw [mem_primeFactors] at hp
Proof state after:
case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : p.Prime ∧ p ∣ n ∧ n ≠ 0
hfg : f p hp✝ ≠ g p hp✝
⊢ ¬p ∣ ∏ p ∈ filter (fun p_1 => g ↑p_1 ⋯ = f p hp✝) n.primeFactors.attach, ↑p
Theorem: Nat.primeFactorsPiBij_inj
Proof state before:
case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : p.Prime ∧ p ∣ n ∧ n ≠ 0
hfg : f p hp✝ ≠ g p hp✝
⊢ ¬p ∣ ∏ p ∈ filter (fun p_1 => g ↑p_1 ⋯ = f p hp✝) n.primeFactors.attach, ↑p
Tactic:
rw [Prime.dvd_finset_prod_iff hp.1.prime]
Proof state after:
case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : p.Prime ∧ p ∣ n ∧ n ≠ 0
hfg : f p hp✝ ≠ g p hp✝
⊢ ¬∃ a ∈ filter (fun p_1 => g ↑p_1 ⋯ = f p hp✝) n.primeFactors.attach, p ∣ ↑a
Theorem: Nat.primeFactorsPiBij_inj
Proof state before:
case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : p.Prime ∧ p ∣ n ∧ n ≠ 0
hfg : f p hp✝ ≠ g p hp✝
⊢ ¬∃ a ∈ filter (fun p_1 => g ↑p_1 ⋯ = f p hp✝) n.primeFactors.attach, p ∣ ↑a
Tactic:
push_neg
Proof state after:
case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : p.Prime ∧ p ∣ n ∧ n ≠ 0
hfg : f p hp✝ ≠ g p hp✝
⊢ ∀ a ∈ filter (fun p_1 => g ↑p_1 ⋯ = f p hp✝) n.primeFactors.attach, ¬p ∣ ↑a
Theorem: Nat.primeFactorsPiBij_inj
Proof state before:
case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : p.Prime ∧ p ∣ n ∧ n ≠ 0
hfg : f p hp✝ ≠ g p hp✝
⊢ ∀ a ∈ filter (fun p_1 => g ↑p_1 ⋯ = f p hp✝) n.primeFactors.attach, ¬p ∣ ↑a
Tactic:
intro q hq
Proof state after:
case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : p.Prime ∧ p ∣ n ∧ n ≠ 0
hfg : f p hp✝ ≠ g p hp✝
q : { x // x ∈ n.primeFactors }
hq : q ∈ filter (fun p_1 => g ↑p_1 ⋯ = f p hp✝) n.primeFactors.attach
⊢ ¬p ∣ ↑q
Theorem: Nat.primeFactorsPiBij_inj
Proof state before:
case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : p.Prime ∧ p ∣ n ∧ n ≠ 0
hfg : f p hp✝ ≠ g p hp✝
q : { x // x ∈ n.primeFactors }
hq : q ∈ filter (fun p_1 => g ↑p_1 ⋯ = f p hp✝) n.primeFactors.attach
⊢ ¬p ∣ ↑q
Tactic:
rw [Nat.prime_dvd_prime_iff_eq hp.1 (Nat.prime_of_mem_factors $ List.mem_toFinset.mp q.2)]
Proof state after:
case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : p.Prime ∧ p ∣ n ∧ n ≠ 0
hfg : f p hp✝ ≠ g p hp✝
q : { x // x ∈ n.primeFactors }
hq : q ∈ filter (fun p_1 => g ↑p_1 ⋯ = f p hp✝) n.primeFactors.attach
⊢ ¬p = ↑q
Theorem: Nat.primeFactorsPiBij_inj
Proof state before:
case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : p.Prime ∧ p ∣ n ∧ n ≠ 0
hfg : f p hp✝ ≠ g p hp✝
q : { x // x ∈ n.primeFactors }
hq : q ∈ filter (fun p_1 => g ↑p_1 ⋯ = f p hp✝) n.primeFactors.attach
⊢ ¬p = ↑q
Tactic:
intro hpq
Proof state after:
case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : p.Prime ∧ p ∣ n ∧ n ≠ 0
hfg : f p hp✝ ≠ g p hp✝
q : { x // x ∈ n.primeFactors }
hq : q ∈ filter (fun p_1 => g ↑p_1 ⋯ = f p hp✝) n.primeFactors.attach
hpq : p = ↑q
⊢ False
Theorem: Nat.primeFactorsPiBij_inj
Proof state before:
case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : p.Prime ∧ p ∣ n ∧ n ≠ 0
hfg : f p hp✝ ≠ g p hp✝
q : { x // x ∈ n.primeFactors }
hq : q ∈ filter (fun p_1 => g ↑p_1 ⋯ = f p hp✝) n.primeFactors.attach
hpq : p = ↑q
⊢ False
Tactic:
subst hpq
Proof state after:
case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
q : { x // x ∈ n.primeFactors }
hp✝ : ↑q ∈ n.primeFactors
hp : (↑q).Prime ∧ ↑q ∣ n ∧ n ≠ 0
hfg : f (↑q) hp✝ ≠ g (↑q) hp✝
hq : q ∈ filter (fun p => g ↑p ⋯ = f (↑q) hp✝) n.primeFactors.attach
⊢ False
Theorem: Nat.primeFactorsPiBij_inj
Proof state before:
case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
q : { x // x ∈ n.primeFactors }
hp✝ : ↑q ∈ n.primeFactors
hp : (↑q).Prime ∧ ↑q ∣ n ∧ n ≠ 0
hfg : f (↑q) hp✝ ≠ g (↑q) hp✝
hq : q ∈ filter (fun p => g ↑p ⋯ = f (↑q) hp✝) n.primeFactors.attach
⊢ False
Tactic:
rw [(mem_filter.mp hq).2] at hfg
Proof state after:
case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
q : { x // x ∈ n.primeFactors }
hp✝ : ↑q ∈ n.primeFactors
hp : (↑q).Prime ∧ ↑q ∣ n ∧ n ≠ 0
hfg : f (↑q) hp✝ ≠ f (↑q) hp✝
hq : q ∈ filter (fun p => g ↑p ⋯ = f (↑q) hp✝) n.primeFactors.attach
⊢ False
Theorem: Nat.primeFactorsPiBij_inj
Proof state before:
case h.a
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x => univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x => univ
q : { x // x ∈ n.primeFactors }
hp✝ : ↑q ∈ n.primeFactors
hp : (↑q).Prime ∧ ↑q ∣ n ∧ n ≠ 0
hfg : f (↑q) hp✝ ≠ f (↑q) hp✝
hq : q ∈ filter (fun p => g ↑p ⋯ = f (↑q) hp✝) n.primeFactors.attach
⊢ False
Tactic:
exact hfg rfl
Proof state after:
no goals
Theorem: Nat.primeFactorsPiBij_surj
Proof state before:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
⊢ ∃ g, ∃ (hg : g ∈ n.primeFactors.pi fun x => univ), Nat.primeFactorsPiBij d n g hg = t
Tactic:
have exists_unique := fun (p : ℕ) (hp : p ∈ n.primeFactors) =>
  (finMulAntidiagonal_exists_unique_prime_dvd hn
    (mem_primeFactors_iff_mem_factors.mp hp) t ht)
Proof state after:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
exists_unique : ∀ p ∈ n.primeFactors, ∃! i, p ∣ t i
⊢ ∃ g, ∃ (hg : g ∈ n.primeFactors.pi fun x => univ), Nat.primeFactorsPiBij d n g hg = t
Theorem: Nat.primeFactorsPiBij_surj
Proof state before:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal n
exists_unique : ∀ 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 exists_unique
Proof state after:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal 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
Theorem: Nat.primeFactorsPiBij_surj
Proof state before:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal 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
Tactic:
refine ⟨f, ?_, ?_⟩
Proof state after:
case refine_1
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal 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
⊢ f ∈ n.primeFactors.pi fun x => univ

case refine_2
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiagonal 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
⊢ Nat.primeFactorsPiBij d n f ?refine_1 = t