-- Mathlib/Algebra/Order/Antidiag/Nat.lean
theorem primeFactorsPiBij_inj (d n : ℕ)
    (f : (p : ℕ) → p ∈ n.primeFactors → Fin d) (hf : f ∈ pi n.primeFactors fun _ => univ)
    (g : (p : ℕ) → p ∈ n.primeFactors → Fin d) (hg : g ∈ pi n.primeFactors fun _ => univ) :
    Nat.primeFactorsPiBij d n f hf = Nat.primeFactorsPiBij d n g hg → f = g

Proof state:
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 : Prime p ∧ 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_primeFactorsList
  <| List.mem_toFinset.mp q.2)]

Result:
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 : Prime p ∧ 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

Proof state:
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

Result:
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 : Prime p ∧ 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

Proof state:
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

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

Proof state:
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 : Prime p ∧ 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:
rintro rfl

Result:
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 : Prime ↑q ∧ ↑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

Proof state:
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 : Prime p ∧ 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

Result:
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 : Prime p ∧ 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

Proof state:
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 : Prime ↑q ∧ ↑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

Result:
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 : Prime ↑q ∧ ↑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

Proof state:
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]

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

Proof state:
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 : Prime ↑q ∧ ↑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

Result:
no goals

Proof state:
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 : Prime p ∧ 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

Result:
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 : Prime p ∧ 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

Proof state:
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⟩

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