Theorem: C05S03.two_le (LeanCourse/MIL/C05_Elementary_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean)

State before:
m : ℕ
h0 : m ≠ 0
h1 : m ≠ 1
⊢ 2 ≤ m
Tactic:
cases m
State after:
case zero
h0 : 0 ≠ 0
h1 : 0 ≠ 1
⊢ 2 ≤ 0

case succ
n✝ : ℕ
h0 : n✝ + 1 ≠ 0
h1 : n✝ + 1 ≠ 1
a✝ : n✝ + 1 = n✝ → 2 ≤ n✝ + 1
⊢ 2 ≤ n✝ + 1

State before:
case zero
h0 : 0 ≠ 0
h1 : 0 ≠ 1
⊢ 2 ≤ 0

case succ
n✝ : ℕ
h0 : n✝ + 1 ≠ 0
h1 : n✝ + 1 ≠ 1
a✝ : n✝ + 1 = n✝ → 2 ≤ n✝ + 1
⊢ 2 ≤ n✝ + 1
Tactic:
contradiction
State after:
case succ
n✝ : ℕ
h0 : n✝ + 1 ≠ 0
h1 : n✝ + 1 ≠ 1
a✝ : n✝ + 1 = n✝ → 2 ≤ n✝ + 1
⊢ 2 ≤ n✝ + 1

State before:
m : ℕ
h0 : m + 1 ≠ 0
h1 : m + 1 ≠ 1
hm : m + 1 = m → 2 ≤ m + 1
⊢ 2 ≤ m + 1
Tactic:
case succ m hm =>
  cases m; contradiction
  repeat' apply Nat.succ_le_succ
  apply zero_le
State after:
no goals

State before:
m : ℕ
h0 : m + 1 ≠ 0
h1 : m + 1 ≠ 1
hm : m + 1 = m → 2 ≤ m + 1
⊢ 2 ≤ m + 1
Tactic:
cases m
State after:
case zero
h0 : 0 + 1 ≠ 0
h1 : 0 + 1 ≠ 1
hm : 0 + 1 = 0 → 2 ≤ 0 + 1
⊢ 2 ≤ 0 + 1

case succ
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
hm : n✝ + 1 + 1 = n✝ + 1 → 2 ≤ n✝ + 1 + 1
a✝ : n✝ + 1 = n✝ → 2 ≤ n✝ + 1 + 1
⊢ 2 ≤ n✝ + 1 + 1

State before:
case zero
h0 : 0 + 1 ≠ 0
h1 : 0 + 1 ≠ 1
hm : 0 + 1 = 0 → 2 ≤ 0 + 1
⊢ 2 ≤ 0 + 1

case succ
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
hm : n✝ + 1 + 1 = n✝ + 1 → 2 ≤ n✝ + 1 + 1
a✝ : n✝ + 1 = n✝ → 2 ≤ n✝ + 1 + 1
⊢ 2 ≤ n✝ + 1 + 1
Tactic:
contradiction
State after:
case succ
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
hm : n✝ + 1 + 1 = n✝ + 1 → 2 ≤ n✝ + 1 + 1
a✝ : n✝ + 1 = n✝ → 2 ≤ n✝ + 1 + 1
⊢ 2 ≤ n✝ + 1 + 1

State before:
case succ
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
hm : n✝ + 1 + 1 = n✝ + 1 → 2 ≤ n✝ + 1 + 1
a✝ : n✝ + 1 = n✝ → 2 ≤ n✝ + 1 + 1
⊢ 2 ≤ n✝ + 1 + 1
Tactic:
repeat' apply Nat.succ_le_succ
State after:
case succ.a.a
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
hm : n✝ + 1 + 1 = n✝ + 1 → 2 ≤ n✝ + 1 + 1
a✝ : n✝ + 1 = n✝ → 2 ≤ n✝ + 1 + 1
⊢ 0 ≤ n✝

State before:
case succ.a.a
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
hm : n✝ + 1 + 1 = n✝ + 1 → 2 ≤ n✝ + 1 + 1
a✝ : n✝ + 1 = n✝ → 2 ≤ n✝ + 1 + 1
⊢ 0 ≤ n✝
Tactic:
apply zero_le
State after:
no goals

State before:
case succ.a
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
hm : n✝ + 1 + 1 = n✝ + 1 → 2 ≤ n✝ + 1 + 1
a✝ : n✝ + 1 = n✝ → 2 ≤ n✝ + 1 + 1
⊢ 1 ≤ n✝ + 1
Tactic:
apply Nat.succ_le_succ
State after:
case succ.a.a
n✝ : ℕ
h0 : n✝ + 1 + 1 ≠ 0
h1 : n✝ + 1 + 1 ≠ 1
hm : n✝ + 1 + 1 = n✝ + 1 → 2 ≤ n✝ + 1 + 1
a✝ : n✝ + 1 = n✝ → 2 ≤ n✝ + 1 + 1
⊢ 0 ≤ n✝