Theorem: Nat.prime_composite_induction (LeanCamCombi/Mathlib/RingTheory/Int/Basic.lean)

State before:
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), p.Prime → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n : ℕ
⊢ P n
Tactic:
refine induction_on_primes zero one ?_ _
State after:
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), p.Prime → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n : ℕ
⊢ ∀ (p a : ℕ), p.Prime → P a → P (p * a)

State before:
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), p.Prime → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n : ℕ
⊢ ∀ (p a : ℕ), p.Prime → P a → P (p * a)
Tactic:
rintro p (_ | _ | a) hp ha
State after:
case zero
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), p.Prime → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n p : ℕ
hp : p.Prime
ha : P 0
⊢ P (p * 0)

case succ.zero
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), p.Prime → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n p : ℕ
hp : p.Prime
ha : P (0 + 1)
⊢ P (p * (0 + 1))

case succ.succ
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), p.Prime → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n p a : ℕ
hp : p.Prime
ha : P (a + 1 + 1)
⊢ P (p * (a + 1 + 1))

State before:
case zero
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), p.Prime → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n p : ℕ
hp : p.Prime
ha : P 0
⊢ P (p * 0)
Tactic:
simpa
State after:
no goals

State before:
case succ.zero
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), p.Prime → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n p : ℕ
hp : p.Prime
ha : P (0 + 1)
⊢ P (p * (0 + 1))
Tactic:
simpa using prime _ hp
State after:
no goals

State before:
case succ.succ
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), p.Prime → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n p a : ℕ
hp : p.Prime
ha : P (a + 1 + 1)
⊢ P (p * (a + 1 + 1))
Tactic:
exact composite _ hp.two_le (prime _ hp) _ a.one_lt_succ_succ ha
State after:
no goals