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

State before:
x : ℕ
⊢ Nat.modCore x 1 = 0
Tactic:
induction x <;> (try unfold Nat.modCore; simp [*])
State after:
no goals

State before:
case succ
n✝ : ℕ
n_ih✝ : Nat.modCore n✝ 1 = 0
⊢ Nat.modCore (succ n✝) 1 = 0
Tactic:
try unfold Nat.modCore; simp [*]
State after:
no goals

State before:
case succ
n✝ : ℕ
n_ih✝ : Nat.modCore n✝ 1 = 0
⊢ Nat.modCore (succ n✝) 1 = 0
Tactic:
unfold Nat.modCore
State after:
case succ
n✝ : ℕ
n_ih✝ : Nat.modCore n✝ 1 = 0
⊢ (if 0 < 1 ∧ 1 ≤ succ n✝ then Nat.modCore (succ n✝ - 1) 1 else succ n✝) = 0

State before:
case succ
n✝ : ℕ
n_ih✝ : Nat.modCore n✝ 1 = 0
⊢ (if 0 < 1 ∧ 1 ≤ succ n✝ then Nat.modCore (succ n✝ - 1) 1 else succ n✝) = 0
Tactic:
simp [*]
State after:
no goals