English
In a divisor chain c: Fin(n+1) → Associates(M) enumerating divisors of q with the chain property, the second element c(1) is irreducible.
Русский
В цепи делителей c: Fin(n+1) → Associates(M), перечисляющей делители q, вторая компонента c(1) неприводима.
LaTeX
$$$\mathrm{Irreducible}(c(1)).$$$
Lean4
/-- The second element of a chain is irreducible. -/
theorem second_of_chain_is_irreducible {q : Associates M} {n : ℕ} (hn : n ≠ 0) {c : Fin (n + 1) → Associates M}
(h₁ : StrictMono c) (h₂ : ∀ {r}, r ≤ q ↔ ∃ i, r = c i) (hq : q ≠ 0) : Irreducible (c 1) :=
by
rcases n with - | n; · contradiction
refine (Associates.isAtom_iff (ne_zero_of_dvd_ne_zero hq (h₂.2 ⟨1, rfl⟩))).mp ⟨?_, fun b hb => ?_⟩
· exact ne_bot_of_gt (h₁ (show (0 : Fin (n + 2)) < 1 from Fin.one_pos))
obtain ⟨⟨i, hi⟩, rfl⟩ := h₂.1 (hb.le.trans (h₂.2 ⟨1, rfl⟩))
cases i
· exact (Associates.isUnit_iff_eq_one _).mp (first_of_chain_isUnit h₁ @h₂)
· simpa [Fin.lt_iff_val_lt_val] using h₁.lt_iff_lt.mp hb
