English
Let q and r be Associates(M) with a chain c: Fin(n+1) → Associates(M) satisfying the chain conditions and hr: r ≤ q. If i is the unique index corresponding to r in the chain, then r = c(1)^i.
Русский
Пусть q и r — Associates(M) и существует цепь c: Fin(n+1) → Associates(M) с условиями цепи; если r ≤ q и r = c(i) для некоторого i, то r = c(1)^i.
LaTeX
$$$\exists i:\mathrm{Fin}(n+1),\ r=c(1)^i.$$$
Lean4
theorem element_of_chain_eq_pow_second_of_chain {q r : Associates M} {n : ℕ} (hn : n ≠ 0)
{c : Fin (n + 1) → Associates M} (h₁ : StrictMono c) (h₂ : ∀ {r}, r ≤ q ↔ ∃ i, r = c i) (hr : r ∣ q) (hq : q ≠ 0) :
∃ i : Fin (n + 1), r = c 1 ^ (i : ℕ) := by
classical
let i := Multiset.card (normalizedFactors r)
have hi : normalizedFactors r = Multiset.replicate i (c 1) :=
by
apply Multiset.eq_replicate_of_mem
intro b hb
refine
eq_second_of_chain_of_prime_dvd hn h₁ (@fun r' => h₂) (prime_of_normalized_factor b hb) hr
(dvd_of_mem_normalizedFactors hb)
have H : r = c 1 ^ i :=
by
have := UniqueFactorizationMonoid.prod_normalizedFactors (ne_zero_of_dvd_ne_zero hq hr)
rw [associated_iff_eq, hi, Multiset.prod_replicate] at this
rw [this]
refine ⟨⟨i, ?_⟩, H⟩
have : (Finset.univ.image fun m : Fin (i + 1) => c 1 ^ (m : ℕ)).card = i + 1 :=
by
conv_rhs => rw [← Finset.card_fin (i + 1)]
cases n
· contradiction
rw [Finset.card_image_iff]
refine Set.injOn_of_injective (fun m m' h => Fin.ext ?_)
refine pow_injective_of_not_isUnit (element_of_chain_not_isUnit_of_index_ne_zero (by simp) h₁) ?_ h
exact Irreducible.ne_zero (second_of_chain_is_irreducible hn h₁ (@h₂) hq)
suffices H' : ∀ r ∈ Finset.univ.image fun m : Fin (i + 1) => c 1 ^ (m : ℕ), r ≤ q
by
simp only [← Nat.succ_le_iff, Nat.succ_eq_add_one, ← this]
apply card_subset_divisors_le_length_of_chain (@h₂) H'
simp only [Finset.mem_image]
rintro r ⟨a, _, rfl⟩
refine dvd_trans ?_ hr
use c 1 ^ (i - (a : ℕ))
rw [pow_mul_pow_sub (c 1)]
· exact H
· exact Nat.succ_le_succ_iff.mp a.2
