rw [Units.ext_iff] at h
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
h : two = 1
⊢ False
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
h : ↑two = ↑1
⊢ False