R : Type ?u.849581
n : ℕ
x : ℤ
hx : Odd x
⊢ x ^ 2 % 4 = 1
R : Type ?u.849581
n : ℕ
x : ℤ
⊢ Odd x → x ^ 2 % 4 = 1
intro hx
R : Type ?u.849581
n : ℕ
x : ℤ
hx : ∃ k, x = 2 * k + 1
⊢ x ^ 2 % 4 = 1
R : Type ?u.849581
n : ℕ
x : ℤ
hx : Odd x
⊢ x ^ 2 % 4 = 1
unfold Odd at hx
case intro
R : Type ?u.849581
n : ℕ
w✝ : ℤ
⊢ (2 * w✝ + 1) ^ 2 % 4 = 1
R : Type ?u.849581
n : ℕ
x : ℤ
hx : ∃ k, x = 2 * k + 1
⊢ x ^ 2 % 4 = 1
rcases hx with ⟨_, rfl⟩
case intro
R : Type ?u.849581
n : ℕ
w✝ : ℤ
⊢ (1 + w✝ * 4 + w✝ ^ 2 * 4) % 4 = 1
case intro
R : Type ?u.849581
n : ℕ
w✝ : ℤ
⊢ (2 * w✝ + 1) ^ 2 % 4 = 1
ring_nf
case intro
R : Type ?u.849581
n : ℕ
w✝ : ℤ
⊢ 1 % 4 = 1
case intro
R : Type ?u.849581
n : ℕ
w✝ : ℤ
⊢ (1 + w✝ * 4 + w✝ ^ 2 * 4) % 4 = 1
rw [add_assoc, ← add_mul, Int.add_mul_emod_self]
no goals
case intro
R : Type ?u.849581
n : ℕ
w✝ : ℤ
⊢ 1 % 4 = 1
norm_num