Theorem: C05S03.two_le_of_mod_4_eq_3 (LeanCourse/MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean)

State before:
case h1
n : ℕ
h : n % 4 = 3
⊢ n ≠ 1
Tactic:
intro neq
State after:
case h1
n : ℕ
h : n % 4 = 3
neq : n = 1
⊢ False

State before:
case h1
n : ℕ
h : n % 4 = 3
neq : n = 1
⊢ False
Tactic:
rw [neq] at h
State after:
case h1
n : ℕ
h : 1 % 4 = 3
neq : n = 1
⊢ False

State before:
case h1
n : ℕ
h : 1 % 4 = 3
neq : n = 1
⊢ False
Tactic:
norm_num at h
State after:
no goals