English
Let P be a property of natural numbers. If P holds for 0 and 1, and for every prime p and every n > 0 we have P(p^n), and whenever a > 1 and b > 1 with Coprime(a,b) we have P(a) and P(b) implying P(a·b), then P(n) holds for all natural numbers n.
Русский
Пусть P — свойство натурального числа. Пусть P(0) и P(1) истинны, а для любой простоты p и любого n > 0 верно P(p^n), и если a > 1 и b > 1 и gcd(a,b)=1, то из P(a) и P(b) следует P(a·b). Тогда P(n) верно для всех n ∈ ℕ.
LaTeX
$$$\text{Let } P:\mathbb{N}\to\text{Prop}.\ P(0) \\land P(1) \\land \forall p,\ n>0,\ (Prime(p) \Rightarrow P(p^n)) \\land \forall a,b>1,\ Coprime(a,b) \Rightarrow (P(a) \land P(b) \Rightarrow P(ab)) \\Rightarrow \forall n:\mathbb{N},\ P(n).$$$
Lean4
/-- Given `P 0`, `P 1`, and `P (p ^ n)` for positive prime powers, and a way to extend `P a` and
`P b` to `P (a * b)` when `a, b` are positive coprime, we can define `P` for all natural numbers. -/
@[elab_as_elim]
def recOnPosPrimePosCoprime {motive : ℕ → Sort*} (prime_pow : ∀ p n : ℕ, Prime p → 0 < n → motive (p ^ n))
(zero : motive 0) (one : motive 1)
(coprime : ∀ a b, 1 < a → 1 < b → Coprime a b → motive a → motive b → motive (a * b)) : ∀ a, motive a :=
recOnPrimePow zero one <| by
intro a p n hp' hpa hn hPa
by_cases ha1 : a = 1
· rw [ha1, mul_one]
exact prime_pow p n hp' hn
refine coprime (p ^ n) a (hp'.one_lt.trans_le (le_self_pow hn.ne' _)) ?_ ?_ (prime_pow _ _ hp' hn) hPa
· contrapose! hpa
simp [lt_one_iff.1 (lt_of_le_of_ne hpa ha1)]
· simpa [hn, Prime.coprime_iff_not_dvd hp']
