Theorem: Nat.ge_mod (LeanMeetup/Exercise02Solutions.lean)

State before:
n x : ℕ
⊢ (match x, n + 1 with
    | 0, x => 0
    | x@h:(succ n), y => Nat.modCore x y) <
    n + 1
Tactic:
cases x
State after:
case zero
n : ℕ
⊢ (match zero, n + 1 with
    | 0, x => 0
    | x@h:(succ n), y => Nat.modCore x y) <
    n + 1

case succ
n n✝ : ℕ
⊢ (match succ n✝, n + 1 with
    | 0, x => 0
    | x@h:(succ n), y => Nat.modCore x y) <
    n + 1

State before:
case zero
n : ℕ
⊢ (match zero, n + 1 with
    | 0, x => 0
    | x@h:(succ n), y => Nat.modCore x y) <
    n + 1

case succ
n n✝ : ℕ
⊢ (match succ n✝, n + 1 with
    | 0, x => 0
    | x@h:(succ n), y => Nat.modCore x y) <
    n + 1
Tactic:
next => simp
State after:
case succ
n n✝ : ℕ
⊢ (match succ n✝, n + 1 with
    | 0, x => 0
    | x@h:(succ n), y => Nat.modCore x y) <
    n + 1

State before:
n : ℕ
⊢ (match zero, n + 1 with
    | 0, x => 0
    | x@h:(succ n), y => Nat.modCore x y) <
    n + 1
Tactic:
simp
State after:
no goals

State before:
n x : ℕ
⊢ (match succ x, n + 1 with
    | 0, x => 0
    | x@h:(succ n), y => Nat.modCore x y) <
    n + 1
Tactic:
simp
State after:
n x : ℕ
⊢ Nat.modCore (succ x) (n + 1) < n + 1

State before:
n x : ℕ
⊢ Nat.modCore (succ x) (n + 1) < n + 1
Tactic:
induction x using Nat.strongInductionOn
State after:
case ind
n n✝ : ℕ
a✝ : ∀ m < n✝, Nat.modCore (succ m) (n + 1) < n + 1
⊢ Nat.modCore (succ n✝) (n + 1) < n + 1

State before:
n x : ℕ
ih : ∀ m < x, Nat.modCore (succ m) (n + 1) < n + 1
⊢ Nat.modCore (succ x) (n + 1) < n + 1
Tactic:
unfold Nat.modCore
State after:
n x : ℕ
ih : ∀ m < x, Nat.modCore (succ m) (n + 1) < n + 1
⊢ (if 0 < n + 1 ∧ n + 1 ≤ succ x then Nat.modCore (succ x - (n + 1)) (n + 1) else succ x) < n + 1

State before:
n x : ℕ
ih : ∀ m < x, Nat.modCore (succ m) (n + 1) < n + 1
⊢ (if 0 < n + 1 ∧ n + 1 ≤ succ x then Nat.modCore (succ x - (n + 1)) (n + 1) else succ x) < n + 1
Tactic:
cases x <;> simp [Nat.succ_le_succ_iff]
State after:
case zero
n : ℕ
ih : ∀ m < zero, Nat.modCore (succ m) (n + 1) < n + 1
⊢ (if n = 0 then 0 else succ 0) < n + 1

case succ
n n✝ : ℕ
ih : ∀ m < succ n✝, Nat.modCore (succ m) (n + 1) < n + 1
⊢ (if n ≤ n✝ + 1 then Nat.modCore (n✝ + 1 - n) (n + 1) else succ (succ n✝)) < n + 1

State before:
case zero
n : ℕ
ih : ∀ m < zero, Nat.modCore (succ m) (n + 1) < n + 1
⊢ (if n = 0 then 0 else succ 0) < n + 1

case succ
n n✝ : ℕ
ih : ∀ m < succ n✝, Nat.modCore (succ m) (n + 1) < n + 1
⊢ (if n ≤ n✝ + 1 then Nat.modCore (n✝ + 1 - n) (n + 1) else succ (succ n✝)) < n + 1
Tactic:
next =>
  cases n <;> simp
State after:
case succ
n n✝ : ℕ
ih : ∀ m < succ n✝, Nat.modCore (succ m) (n + 1) < n + 1
⊢ (if n ≤ n✝ + 1 then Nat.modCore (n✝ + 1 - n) (n + 1) else succ (succ n✝)) < n + 1

State before:
n : ℕ
ih : ∀ m < zero, Nat.modCore (succ m) (n + 1) < n + 1
⊢ (if n = 0 then 0 else succ 0) < n + 1
Tactic:
cases n <;> simp
State after:
no goals

State before:
n x : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (n + 1) < n + 1
⊢ (if n ≤ x + 1 then Nat.modCore (x + 1 - n) (n + 1) else succ (succ x)) < n + 1
Tactic:
cases' n with n <;> simp
State after:
case succ
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
⊢ (if succ n ≤ x + 1 then Nat.modCore (x - n) (succ n + 1) else succ (succ x)) < succ n + 1

State before:
case succ
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
⊢ (if succ n ≤ x + 1 then Nat.modCore (x - n) (succ n + 1) else succ (succ x)) < succ n + 1
Tactic:
split_ifs with h
State after:
case pos
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
⊢ Nat.modCore (x - n) (succ n + 1) < succ n + 1

case neg
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : ¬succ n ≤ x + 1
⊢ succ (succ x) < succ n + 1

State before:
case pos
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
⊢ Nat.modCore (x - n) (succ n + 1) < succ n + 1
Tactic:
cases hm : x - n
State after:
case pos.zero
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
hm : x - n = zero
⊢ Nat.modCore zero (succ n + 1) < succ n + 1

case pos.succ
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ Nat.modCore (succ n✝) (succ n + 1) < succ n + 1

State before:
case pos.zero
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
hm : x - n = zero
⊢ Nat.modCore zero (succ n + 1) < succ n + 1

case pos.succ
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ Nat.modCore (succ n✝) (succ n + 1) < succ n + 1
Tactic:
next => simp
State after:
case pos.succ
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ Nat.modCore (succ n✝) (succ n + 1) < succ n + 1

State before:
case pos.succ
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ Nat.modCore (succ n✝) (succ n + 1) < succ n + 1
Tactic:
next =>
  apply ih
  apply Nat.lt_of_succ_le
  apply Nat.le_succ_of_le
  rw [←hm]
  apply sub_le
State after:
no goals

State before:
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
hm : x - n = zero
⊢ Nat.modCore zero (succ n + 1) < succ n + 1
Tactic:
simp
State after:
no goals

State before:
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ Nat.modCore (succ n✝) (succ n + 1) < succ n + 1
Tactic:
apply ih
State after:
case a
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ n✝ < succ x

State before:
case a
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ n✝ < succ x
Tactic:
apply Nat.lt_of_succ_le
State after:
case a.h
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ succ n✝ ≤ succ x

State before:
case a.h
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ succ n✝ ≤ succ x
Tactic:
apply Nat.le_succ_of_le
State after:
case a.h.h
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ succ n✝ ≤ x

State before:
case a.h.h
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ succ n✝ ≤ x
Tactic:
rw [←hm]
State after:
case a.h.h
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ x - n ≤ x

State before:
case a.h.h
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : succ n ≤ x + 1
n✝ : ℕ
hm : x - n = succ n✝
⊢ x - n ≤ x
Tactic:
apply sub_le
State after:
no goals

State before:
case neg
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : ¬succ n ≤ x + 1
⊢ succ (succ x) < succ n + 1
Tactic:
apply Nat.succ_lt_succ_iff.mpr
State after:
case neg
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : ¬succ n ≤ x + 1
⊢ x + 1 < n + 1

State before:
case neg
x n : ℕ
ih : ∀ m < succ x, Nat.modCore (succ m) (succ n + 1) < succ n + 1
h : ¬succ n ≤ x + 1
⊢ x + 1 < n + 1
Tactic:
apply not_le.mp h
State after:
no goals