Naive attempt at very simple Lean4 proof about pseudo-primes

mersenne-pseudo-prime.lean

import Mathlib.Tactic.Ring -- import the `ring` tactic
import Mathlib.Algebra.Algebra.ZMod
import Mathlib.Data.Nat.Init
import Mathlib.Data.Int.Notation
import Mathlib.Init
import Mathlib.Data.Nat.ModEq
import Mathlib.Data.ZMod.Basic
import Mathlib.Data.Nat.Notation

namespace Nat


-- (d^m)^n = d^(m*n)
lemma power_of_power {d m n: ℕ}: (d^m)^n = d^(m * n) := by
  ring
  
-- move a factor of two in a (2^(m/2))^n where m and n are even. This could 
-- be made much better if I understood how to talk about even numbers because 
-- we wouldn't have to introduce extra variables.
lemma move_the_two {d km kn : ℕ} (hn: n=2*kn) (hm: m=2*km): (d^(m/2))^n = (d^m)^(n/2) := by 
  rw [power_of_power, power_of_power, hn, hm]
  simp
  ring

-- playing with even numbers, this is not well done
def is_even (a : ℕ) := ∃ b, a = 2 * b

lemma even_product {a b:ℕ} (h1: is_even a) : is_even (a*b) := by
  match h1 with 
  | ⟨ka, hwa⟩ => 
    rw[hwa, is_even, Nat.mul_assoc]
    simp

-- show $a-1 ≡  0 [ZMOD d]$ implies $a = 1 [ZMOD d]$ 
-- the current approach is to express everything in terms of values in ℤ 
-- but the last step is missing. Should be easy.
theorem mod_one_of_sub_one_eq_zero {a d t: ℤ}  [NeZero d] (hd : d > 1) (ha: a ≥ 0) (hu: u = d * t)
  (h : a - 1 ≡ 0 [ZMOD d]) (h1: 1%d + d * (1/d) = 1) (h3: d * t = u) : a ≡ 1 [ZMOD d] := by
  -- The hypothesis h means a - 1 ≡ 0 (mod d), i.e., d divides (a - 1)
  -- This gives us that there exists some k such that a - 1 = k * d
  -- We need to show a ≡ 1 (mod d), i.e., d divides (a - 1)
  rw [Int.modEq_iff_add_fac] at h
  rw [← Int.sub_self 1, Int.sub_eq_add_neg, Int.sub_eq_add_neg] at h
  nth_rw 1 [Int.add_comm] at h
  nth_rw 2 [Int.add_comm] at h  -- why does add_right_inj not work here?
  rw [Int.modEq_iff_add_fac]
  rw [Int.emod_add_ediv] at h1
  sorry

-- This is very close to what we need in mod_one_of_sub_one_eq_zero
lemma sub_sub_same {a b : ℤ} :(a = b) ↔ (a-1=b-1) := by
  rw [Int.sub_eq_add_neg, Int.sub_eq_add_neg, Int.add_left_inj]

-- the goal here is to prove that a power of 2 2^p is even if p > 0
lemma power_of_2_is_even {p k : ℕ }  (h1: 2^p = 2*2^(p-1)) (h2: 2^(p-1)=k): (is_even (2^p)) := by
  rw [h2] at h1
  rw [h1]
  simp [is_even]    

-- this will be the real theorem (once it is working)
lemma thm1 {d p: ℕ} (h0: is_even p) (h1: 2^p-1 ≡ 0 [MOD d] ) (h2: 2^p = k) : (2^(p/2))^(d-1) ≡  1 [MOD d] := by
  rw [h2, mod_ones] at h1
  rw [move_the_two]
  

    
   

Yes, essentially we need the following ingredients:

1. d|M(n) <=> 2^n==1 (mod d) [this already involves notion of divisibility and congruence...]
2. x == 1 => x^m == 1 (=: by ring, if I understand well)
3. [power_of_power] (x^a)^b == x^(a*b) for positive integers a, b (=: by ring, if I understand well)
4. M odd and d|M => d odd (from "integers" or where?)
5. d odd => d-1 even (from "integers" or where?)
6. x even => x/2 entier (from "integers" or where?)
7. [move_the_two] ab/2 = a/2b (from "integers" or commutative ring, with "/2" = 2^-1 actually any element?)
8. definition of base 2 Fermat pseudoprimes : 2^(p-1)==1 (mod p)

Where do we need "power_of_2_is_even" ?