Theorem: book.quadratic_reciprocity.fermat_little (FormalBook/Chapter_05.lean)

State before:
p : ℕ
h_p : p ≠ 2
inst✝ : Fact p.Prime
a : ℤ
⊢ ↑a ≠ 0 → ↑a ^ (p - 1) = -1
Tactic:
let units_finset := (Finset.univ : Finset (ZMod p)).erase 0
State after:
p : ℕ
h_p : p ≠ 2
inst✝ : Fact p.Prime
a : ℤ
units_finset : Finset (ZMod p) := univ.erase 0
⊢ ↑a ≠ 0 → ↑a ^ (p - 1) = -1

State before:
p : ℕ
h_p : p ≠ 2
inst✝ : Fact p.Prime
a : ℤ
units_finset : Finset (ZMod p) := univ.erase 0
⊢ ↑a ≠ 0 → ↑a ^ (p - 1) = -1
Tactic:
let image_finset := (units_finset).image (fun x : ZMod p => (a : ZMod p) * x)
State after:
p : ℕ
h_p : p ≠ 2
inst✝ : Fact p.Prime
a : ℤ
units_finset : Finset (ZMod p) := univ.erase 0
image_finset : Finset (ZMod p) := image (fun x => ↑a * x) units_finset
⊢ ↑a ≠ 0 → ↑a ^ (p - 1) = -1

State before:
p : ℕ
h_p : p ≠ 2
inst✝ : Fact p.Prime
a : ℤ
units_finset : Finset (ZMod p) := univ.erase 0
image_finset : Finset (ZMod p) := image (fun x => ↑a * x) units_finset
⊢ ↑a ≠ 0 → ↑a ^ (p - 1) = -1
Tactic:
have : units_finset = image_finset := by sorry
State after:
p : ℕ
h_p : p ≠ 2
inst✝ : Fact p.Prime
a : ℤ
units_finset : Finset (ZMod p) := univ.erase 0
image_finset : Finset (ZMod p) := image (fun x => ↑a * x) units_finset
this : units_finset = image_finset
⊢ ↑a ≠ 0 → ↑a ^ (p - 1) = -1

State before:
p : ℕ
h_p : p ≠ 2
inst✝ : Fact p.Prime
a : ℤ
units_finset : Finset (ZMod p) := univ.erase 0
image_finset : Finset (ZMod p) := image (fun x => ↑a * x) units_finset
this : units_finset = image_finset
⊢ ↑a ≠ 0 → ↑a ^ (p - 1) = -1
Tactic:
sorry
State after:
no goals

State before:
p : ℕ
h_p : p ≠ 2
inst✝ : Fact p.Prime
a : ℤ
units_finset : Finset (ZMod p) := univ.erase 0
image_finset : Finset (ZMod p) := image (fun x => ↑a * x) units_finset
⊢ units_finset = image_finset
Tactic:
sorry
State after:
no goals