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

State before:
x : ℕ
⊢ Nat.modCore 0 x = 0
Tactic:
unfold Nat.modCore
State after:
x : ℕ
⊢ (if 0 < x ∧ x ≤ 0 then Nat.modCore (0 - x) x else 0) = 0

State before:
x : ℕ
⊢ (if 0 < x ∧ x ≤ 0 then Nat.modCore (0 - x) x else 0) = 0
Tactic:
simp only [nonpos_iff_eq_zero, ge_iff_le, _root_.zero_le, tsub_eq_zero_of_le, ite_eq_right_iff,
  and_imp]
State after:
x : ℕ
⊢ 0 < x → x = 0 → Nat.modCore 0 x = 0

State before:
x : ℕ
⊢ 0 < x → x = 0 → Nat.modCore 0 x = 0
Tactic:
rintro _ ⟨⟩
State after:
case refl
a✝ : 0 < 0
⊢ Nat.modCore 0 0 = 0

State before:
case refl
a✝ : 0 < 0
⊢ Nat.modCore 0 0 = 0
Tactic:
rfl
State after:
no goals