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

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!
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

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]
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

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⟩
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

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
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)

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]
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

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]
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

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]
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

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⟩)
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

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

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
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

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]
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

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
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

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
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

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)]
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

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
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

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
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

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
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

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