Theorem: caseStrongRecOnOddPrimes (FromTheBook/Ch02/Bertrand/ProdPrimes.lean)

State before:
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
⊢ ∀ (n : ℕ), p n
Tactic:
intro n
State after:
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
n : ℕ
⊢ p n

State before:
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
n : ℕ
⊢ p n
Tactic:
induction n using Nat.caseStrongInductionOn with
| zero => exact zero
| ind k h_ind =>
  cases dec_em (Nat.Prime k.succ) with
  | inr hk_prime =>
    apply not_prime _ hk_prime
    exact h_ind
  | inl hk_prime =>
    cases Nat.Prime.eq_two_or_odd' hk_prime with
    | inl hk_two => rw [hk_two]; exact two
    | inr hk_two =>
      cases hk_two with
      | intro m hm =>
        simp [Nat.add_one] at hm
        simp [hm] at *
        apply odd_prime _ hk_prime h_ind
State after:
no goals

State before:
case zero
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
⊢ p 0
Tactic:
exact zero
State after:
no goals

State before:
case ind
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
⊢ p (Nat.succ k)
Tactic:
cases dec_em (Nat.Prime k.succ) with
| inr hk_prime =>
  apply not_prime _ hk_prime
  exact h_ind
| inl hk_prime =>
  cases Nat.Prime.eq_two_or_odd' hk_prime with
  | inl hk_two => rw [hk_two]; exact two
  | inr hk_two =>
    cases hk_two with
    | intro m hm =>
      simp [Nat.add_one] at hm
      simp [hm] at *
      apply odd_prime _ hk_prime h_ind
State after:
no goals

State before:
case ind.inr
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
hk_prime : ¬Nat.Prime (Nat.succ k)
⊢ p (Nat.succ k)
Tactic:
apply not_prime _ hk_prime
State after:
case ind.inr
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
hk_prime : ¬Nat.Prime (Nat.succ k)
⊢ ∀ (x : ℕ), x ≤ k → p x

State before:
case ind.inr
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
hk_prime : ¬Nat.Prime (Nat.succ k)
⊢ ∀ (x : ℕ), x ≤ k → p x
Tactic:
exact h_ind
State after:
no goals

State before:
case ind.inl
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
hk_prime : Nat.Prime (Nat.succ k)
⊢ p (Nat.succ k)
Tactic:
cases Nat.Prime.eq_two_or_odd' hk_prime with
| inl hk_two => rw [hk_two]; exact two
| inr hk_two =>
  cases hk_two with
  | intro m hm =>
    simp [Nat.add_one] at hm
    simp [hm] at *
    apply odd_prime _ hk_prime h_ind
State after:
no goals

State before:
case ind.inl.inl
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
hk_prime : Nat.Prime (Nat.succ k)
hk_two : Nat.succ k = 2
⊢ p (Nat.succ k)
Tactic:
rw [hk_two]
State after:
case ind.inl.inl
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
hk_prime : Nat.Prime (Nat.succ k)
hk_two : Nat.succ k = 2
⊢ p 2

State before:
case ind.inl.inl
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
hk_prime : Nat.Prime (Nat.succ k)
hk_two : Nat.succ k = 2
⊢ p 2
Tactic:
exact two
State after:
no goals

State before:
case ind.inl.inr
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
hk_prime : Nat.Prime (Nat.succ k)
hk_two : Odd (Nat.succ k)
⊢ p (Nat.succ k)
Tactic:
cases hk_two with
| intro m hm =>
  simp [Nat.add_one] at hm
  simp [hm] at *
  apply odd_prime _ hk_prime h_ind
State after:
no goals

State before:
case ind.inl.inr.intro
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
hk_prime : Nat.Prime (Nat.succ k)
m : ℕ
hm : Nat.succ k = 2 * m + 1
⊢ p (Nat.succ k)
Tactic:
simp [Nat.add_one] at hm
State after:
case ind.inl.inr.intro
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
hk_prime : Nat.Prime (Nat.succ k)
m : ℕ
hm : k = 2 * m
⊢ p (Nat.succ k)

State before:
case ind.inl.inr.intro
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
hk_prime : Nat.Prime (Nat.succ k)
m : ℕ
hm : k = 2 * m
⊢ p (Nat.succ k)
Tactic:
simp [hm] at *
State after:
case ind.inl.inr.intro
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k m : ℕ
h_ind : ∀ (m_1 : ℕ), m_1 ≤ 2 * m → p m_1
hk_prime : Nat.Prime (Nat.succ (2 * m))
hm : True
⊢ p (Nat.succ (2 * m))

State before:
case ind.inl.inr.intro
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k m : ℕ
h_ind : ∀ (m_1 : ℕ), m_1 ≤ 2 * m → p m_1
hk_prime : Nat.Prime (Nat.succ (2 * m))
hm : True
⊢ p (Nat.succ (2 * m))
Tactic:
apply odd_prime _ hk_prime h_ind
State after:
no goals