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

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

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

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

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

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

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