eq_second_of_chain_of_prime_dvd — Mathlib

English

Let p be a prime dividing r and r divides q in a divisor chain for q. Then p equals the second element c(1) of the chain.

Русский

Пусть p — простое, и p делит r, а r делит q в цепи делителей q. Тогда p = c(1).

LaTeX

$$$\text{If } hp:\mathrm{Prime}(p),\ hr:\, r\mid q,\ hp' : p \mid r,\text{ and } (\forall r',\ r'\le q \iff \exists i, r'=c(i)),\text{ then } p=c(1).$$$

Lean4

theorem eq_second_of_chain_of_prime_dvd {p q r : Associates M} {n : ℕ} (hn : n ≠ 0) {c : Fin (n + 1) → Associates M}
    (h₁ : StrictMono c) (h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i) (hp : Prime p) (hr : r ∣ q) (hp' : p ∣ r) :
    p = c 1 := by
  rcases n with - | n
  · contradiction
  obtain ⟨i, rfl⟩ := h₂.1 (dvd_trans hp' hr)
  refine congr_arg c (eq_of_le_of_not_lt' ?_ fun hi => ?_)
  · rw [Fin.le_iff_val_le_val, Fin.val_one, Nat.succ_le_iff, ← Fin.val_zero (n.succ + 1), ← Fin.lt_iff_val_lt_val,
      Fin.pos_iff_ne_zero]
    rintro rfl
    exact hp.not_unit (first_of_chain_isUnit h₁ @h₂)
  obtain rfl | ⟨j, rfl⟩ := i.eq_zero_or_eq_succ
  · cases hi
  refine
    not_irreducible_of_not_unit_dvdNotUnit
      (DvdNotUnit.not_unit (Associates.dvdNotUnit_iff_lt.2 (h₁ (show (0 : Fin (n + 2)) < j.castSucc from ?_)))) ?_
      hp.irreducible
  · simpa using Fin.lt_def.mp hi
  · refine Associates.dvdNotUnit_iff_lt.2 (h₁ ?_)
    simpa only [Fin.coe_eq_castSucc] using Fin.lt_succ

Похожие утверждения