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

State before:
m n : ℕ
h : m * n % 4 = 3
⊢ m % 4 = 3 ∨ n % 4 = 3
Tactic:
revert h
State after:
m n : ℕ
⊢ m * n % 4 = 3 → m % 4 = 3 ∨ n % 4 = 3

State before:
m n : ℕ
⊢ m * n % 4 = 3 → m % 4 = 3 ∨ n % 4 = 3
Tactic:
rw [Nat.mul_mod]
State after:
m n : ℕ
⊢ m % 4 * (n % 4) % 4 = 3 → m % 4 = 3 ∨ n % 4 = 3

State before:
m n : ℕ
⊢ m % 4 * (n % 4) % 4 = 3 → m % 4 = 3 ∨ n % 4 = 3
Tactic:
have : m % 4 < 4 := Nat.mod_lt m (by norm_num)
State after:
m n : ℕ
this : m % 4 < 4
⊢ m % 4 * (n % 4) % 4 = 3 → m % 4 = 3 ∨ n % 4 = 3

State before:
m n : ℕ
this : m % 4 < 4
⊢ m % 4 * (n % 4) % 4 = 3 → m % 4 = 3 ∨ n % 4 = 3
Tactic:
interval_cases hm : m % 4 <;> simp [hm]
State after:
case «2»
m n : ℕ
hm : m % 4 = 2
this : 2 < 4
⊢ 2 * (n % 4) % 4 = 3 → n % 4 = 3

State before:
case «2»
m n : ℕ
hm : m % 4 = 2
this : 2 < 4
⊢ 2 * (n % 4) % 4 = 3 → n % 4 = 3
Tactic:
have : n % 4 < 4 := Nat.mod_lt n (by norm_num)
State after:
case «2»
m n : ℕ
hm : m % 4 = 2
this✝ : 2 < 4
this : n % 4 < 4
⊢ 2 * (n % 4) % 4 = 3 → n % 4 = 3

State before:
case «2»
m n : ℕ
hm : m % 4 = 2
this✝ : 2 < 4
this : n % 4 < 4
⊢ 2 * (n % 4) % 4 = 3 → n % 4 = 3
Tactic:
interval_cases hn : n % 4 <;> simp [hn]
State after:
no goals

State before:
m n : ℕ
⊢ 4 > 0
Tactic:
norm_num
State after:
no goals

State before:
m n : ℕ
hm : m % 4 = 2
this : 2 < 4
⊢ 4 > 0
Tactic:
norm_num
State after:
no goals