A lean proof that every prime congruent to 1 mod 4 is a sum of two squares, uses mathlib

zagier.lean

import data.nat.basic
import data.int.basic
import data.int.modeq
import init.data.fin.ops
import data.zmod.basic
import data.fintype
import data.nat.prime
import tactic.interactive
import tactic.find
import tactic.tidy
import tactic.library_search
import tactic.ring
import tactic.linarith
import tactic.norm_cast
import group_theory.group_action
import group_theory.sylow
import algebra.group

-- TODO probably there is an easier way of getting
-- the cylic group of order 2 as a multiplicative group
-- maybe using multiplicative (zmod 2) ?

def mul : fin 2 → fin 2 → fin 2 :=
λ a b, (a + b) % 2

instance : group (fin 2) :=
{ mul := mul,
  mul_assoc := dec_trivial,
  one := 0,
  one_mul := dec_trivial,
  mul_one := dec_trivial,
  inv := id,
  mul_left_inv := dec_trivial,
}

variable {SS : Type*}
variable {iS : SS → SS}

-- TODO do I need all these
local attribute [instance, priority 0] subtype.fintype set_fintype classical.prop_decidable

-- define iterated function composition
-- we need the well_founded as recursion is on second variable
-- TODO there was a PR from Neil Strickland? with something similar I think, compare
def funcpow {α : Type*} : (α → α) → ℕ → (α → α) 
| f 0 := (id : (α → α))
| f (n + 1) := f ∘ funcpow f n
using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf psigma.snd⟩]}

@[simp] lemma funcpow_zero {α : Type*} (f : α → α) : funcpow f 0 = id := rfl
@[simp] lemma funcpow_succ {α : Type*} (f : α → α) (n : ℕ) : funcpow f (n + 1) = f ∘ funcpow f n := rfl

@[simp] lemma sum_succ (n m :ℕ) : n + nat.succ m = nat.succ (n  + m) :=
rfl

lemma funcpow_add {α : Type*} (f : α → α) (n m : ℕ) : funcpow f (n + m) = funcpow f n ∘ funcpow f m :=
begin
induction n,
simp only [funcpow_zero, nat.nat_zero_eq_zero, zero_add, function.comp.left_id] at *,
simp only [add_comm, sum_succ, funcpow_succ] at *,
solve_by_elim,
end

lemma mul_succ (n m: ℕ) : (nat.succ n) * m = m + n * m :=
begin 
rw add_mul n 1 m,
simp,
end

lemma funcpow_mul {α : Type*} (f : α → α) (n m : ℕ) : funcpow f (n * m) = funcpow (funcpow f m) n :=
begin
induction n,
simp only [funcpow_zero, nat.nat_zero_eq_zero, zero_mul],
simp only [funcpow_succ],
rw [mul_succ, funcpow_add, n_ih],
end

lemma funcpow_id {α : Type*} (n : ℕ) : funcpow id n = (id : α → α) :=
begin
induction n,
simp only [funcpow_zero, nat.nat_zero_eq_zero],
simpa only [funcpow_succ, function.comp.left_id],
end

instance endpow {α : Type} : has_pow (α → α) ℕ := {
    pow := funcpow,
}

-- TODO lean doesn't like notation here....
-- I couldn't get (f ^ n) to do what I wanted

-- def ttt : (fin 2) → S → S := λ n s, funcpow i (n.val) (s)

@[simp] lemma mod2 (a: fin 2) : a % 2 = a:=
begin
apply fin.eq_of_veq,
rw fin.mod_def,
exact nat.mod_def (a.val) (2 : fin 2),
end

lemma fin_add_cast (x y : fin 2) : (↑x + ↑y : ℕ) % 2 = ↑(x + y) :=
begin
change (x.val + y.val) % 2 = (x+ y).val,
rw fin.add_def,
end

instance finorder_end_cyclic_action (i2 : funcpow iS 2 = id) : mul_action (fin 2) SS := { smul := λ n s, (funcpow iS n) (s),
  one_smul := λ b, rfl,
  mul_smul := begin
  intros x y b,
  simp only [(*), semigroup.mul, monoid.mul, group.mul, mul],
  change funcpow iS ↑((x + y) % 2) b = (funcpow iS ↑x ∘ funcpow iS ↑y) b,
  rw [←(funcpow_add iS ↑x ↑y),
  mod2,
  ←nat.mod_add_div (x + y) 2,
  funcpow_add,
  mul_comm,
  funcpow_mul,
  i2,
  funcpow_id,
  function.comp.right_id,
  fin_add_cast],
  end }


-- Now onto Zagier's proof
-- the basic set we will construct a subset of
-- Zagier uses ℕ^3, but ℕ is annoying for subtraction
-- so we will work with a subtype where all entries are positive
def ℤ3 := ℤ × ℤ × ℤ

open mul_action

-- TODO is this general for mathlib?
lemma fixed_points_finset (α β : Type*) [monoid α] [mul_action α β] [fintype β] [decidable_eq β] :
  set.finite (fixed_points α β) := set.finite.of_fintype (fixed_points α β)


-- some lemmas for later
lemma card_fin_two : fintype.card (fin 2) = 2^1 := rfl
lemma two_prime : nat.prime 2 := dec_trivial

lemma nat_lt_two_is_zero_one {n : ℕ} (h : n < 2) : (n  = 0) ∨ (n = 1) :=begin
have b : (¬ (n > 1)) := nat.lt_le_antisymm h,
by_contradiction,
push_neg at a,
have := nat.one_lt_iff_ne_zero_and_ne_one.mpr a,
tauto,
end


-- The main theorem!

def property (p : ℕ) : (ℤ3 → Prop) :=
    λ ⟨x,y,z⟩, (x^2 + 4 * y * z = p ∧ x > 0 ∧ y > 0 ∧ z > 0 : Prop)

def S (p : ℕ) := { a : ℤ3 // property p a }
-- an auxiliary set that is "easy" to show larger than S but still finite
def big_set (p : ℕ) := (fin p) × (fin p) × (fin p)

instance finbig (p : ℕ) : fintype (big_set p) := 
    by unfold big_set; apply_instance

def random_func (p : ℕ) : S p → big_set p :=
begin
    rintro ⟨⟨X, Y, Z⟩, P⟩,
    exact ⟨
    ⟨int.nat_abs X, begin
        rcases P with ⟨ cond, xpos, ypos, zpos ⟩,
        rw ←int.coe_nat_lt,
        rw int.nat_abs_of_nonneg (le_of_lt xpos),
        rw pow_two X at cond,
        by_contradiction,
        have ale := le_of_not_lt a,
        have ppos : (0 : ℤ) ≤ p := int.coe_zero_le p,
        have : 1 ≤ X := (ge_from_le X 1).mp xpos,
        have p_le_X_mul_X := mul_le_mul this ale ppos (le_of_lt xpos),
        rw one_mul at p_le_X_mul_X,
        have zero_lt_four_y_z := int.mul_pos (dec_trivial : (0 : ℤ) < 4) (int.mul_pos ypos zpos),
        have := add_lt_add_of_lt_of_le zero_lt_four_y_z p_le_X_mul_X,
        simp at this,
        rw [← mul_assoc, cond] at this,
        exact absurd this (irrefl p),
    end⟩,
    ⟨int.nat_abs Y, begin
        rcases P with ⟨ cond, xpos, ypos, zpos ⟩,
        rw ←int.coe_nat_lt,
        rw int.nat_abs_of_nonneg (le_of_lt ypos),
        rw pow_two X at cond,
        by_contradiction,
        have ale := le_of_not_lt a,
        have ppos : (0 : ℤ) ≤ p := int.coe_zero_le p,
        have : 1 ≤ X := (ge_from_le X 1).mp xpos,
        have zero_lt_X_mul_X := mul_pos xpos xpos,
        --have one_le_X_mul_X := mul_le_mul this this ppos (le_of_lt xpos), TODO wTFF this didn't complain
        have : 1 ≤ Z := (ge_from_le Z 1).mp zpos,
        have ttt : (p : ℤ) * 1 ≤ Y * Z := mul_le_mul ale this dec_trivial (le_of_lt ypos),
        rw mul_one at ttt,
        have p_le_four_y_z : 1 * (p : ℤ) ≤ 4 * (Y * Z) := mul_le_mul (dec_trivial : (1:ℤ) ≤ 4) ttt ppos dec_trivial,
        simp at *,
        have := add_lt_add_of_lt_of_le zero_lt_X_mul_X p_le_four_y_z,
        simp at this,
        rw [← mul_assoc, cond] at this,
        exact absurd this (irrefl p),
    end⟩,
    ⟨int.nat_abs Z, begin
        rcases P with ⟨ cond, xpos, ypos, zpos ⟩,
        rw ←int.coe_nat_lt,
        rw int.nat_abs_of_nonneg (le_of_lt zpos),
        rw pow_two X at cond,
        by_contradiction,
        have ale := le_of_not_lt a,
        have ppos : (0 : ℤ) ≤ p := int.coe_zero_le p,
        have : 1 ≤ X := (ge_from_le X 1).mp xpos,
        have zero_lt_X_mul_X := mul_pos xpos xpos,
        --have one_le_X_mul_X := mul_le_mul this this ppos (le_of_lt xpos), wTFF
        have : 1 ≤ Y := (ge_from_le Y 1).mp ypos,
        have ttt : 1 * (p : ℤ) ≤ Y * Z := mul_le_mul this ale dec_trivial (le_of_lt ypos),
        rw one_mul at ttt,
        have p_le_four_y_z : 1 * (p : ℤ) ≤ 4 * (Y * Z) := mul_le_mul (dec_trivial : (1:ℤ) ≤ 4) ttt ppos dec_trivial,
        simp at *,
        have := add_lt_add_of_lt_of_le zero_lt_X_mul_X p_le_four_y_z,
        simp at this,
        rw [← mul_assoc, cond] at this,
        exact absurd this (irrefl p),
    end⟩⟩,

end


lemma random_inj (p : ℕ): function.injective (random_func p) :=
begin
    rintros ⟨⟨X1, Y1, Z1⟩, ⟨cond1, x1pos, y1pos, z1pos⟩⟩ ⟨⟨X2, Y2, Z2⟩, ⟨cond2, x2pos, y2pos, z2pos⟩⟩,
    intro h,
    injections_and_clear,
    injections_and_clear,
    injections_and_clear,
    simp,
    rw ←int.nat_abs_of_nonneg (le_of_lt x1pos),
    rw ←int.nat_abs_of_nonneg (le_of_lt x2pos),
    rw ←int.nat_abs_of_nonneg (le_of_lt y1pos),
    rw ←int.nat_abs_of_nonneg (le_of_lt y2pos),
    rw ←int.nat_abs_of_nonneg (le_of_lt z1pos),
    rw ←int.nat_abs_of_nonneg (le_of_lt z2pos),
    norm_cast,
    tauto,
end

noncomputable instance (p : ℕ): fintype (S p) := fintype.of_injective _ (random_inj p)


def i (p : ℕ) (pprime : nat.prime p) (p1mod4 : p % 4 = 1) : (S p) → (S p) :=
begin
    rintro ⟨⟨X, Y, Z⟩, P⟩,
    exact if h1 : X + Z < Y then
        ⟨(X + 2 * Z, Z, Y - X - Z),
        begin
            rcases P with ⟨ cond, xpos, ypos, zpos ⟩,
            simp,
            split,
            rw [←cond],
            ring,
            repeat{split, linarith},
            ring,
            linarith,
        end
        ⟩
    else if h2 : X < 2 * Y then 
        ⟨(2 * Y - X, Y, X - Y + Z),
        begin
            rcases P with ⟨ cond, xpos, ypos, zpos ⟩,
            dsimp,
            split,
            rw [←cond],
            ring,
            repeat{split, linarith},
            rw not_lt at h1,
            have := eq_or_lt_of_le h1,
            cases this,
            {
                have posss : 0 ≤ (X + 2*Z) := by linarith,
                rw this at cond,
                have : X^2 + 4*(X+Z)*Z = (X + 2*Z)^2 := by ring,
                rw this at cond,
                have : (X + 2*Z) ∣ p := dvd.intro (monoid.pow (X + 2 * Z) (1)) cond,
                have : int.nat_abs (X + 2*Z) ∣ p := int.coe_nat_dvd_right.mp this,
                have := pprime.2 (int.nat_abs (X + 2*Z)) this,
                cases this,
                {
                    have : 2 < (X + 2*Z) := by linarith,
                    rw ←(int.nat_abs_of_nonneg posss) at this,
                    linarith,
                },
                rw ←(int.nat_abs_of_nonneg posss) at cond,
                rw this_1 at cond,
                have p2subpzero:= sub_eq_zero.mpr cond,
                have : (↑p:ℤ) *( ↑ p - 1) = ↑ p^2 - ↑ p :=begin
                    rw [mul_sub, pow_two, mul_one],
                end,
                rw [←this,mul_eq_zero_iff_eq_zero_or_eq_zero] at p2subpzero,
                have := pprime.1,
                cases p2subpzero,
                norm_cast at p2subpzero,
                rw p2subpzero at this,
                exact absurd this (dec_trivial),
                rw sub_eq_zero at p2subpzero,
                linarith,
            },
            linarith,
        end
        ⟩
    else
        ⟨(X - 2 * Y, X - Y + Z, Y),
        begin
            rcases P with ⟨ cond, xpos, ypos, zpos ⟩,
            dsimp,
            rw not_lt at h1 h2,
            split,
            rw [←cond],
            ring,
            split,
            ring,
            have := eq_or_lt_of_le h2,
            cases this with xeq2y,
            {
                rw ←xeq2y at cond,
                have : (2*Y)^2 + 4*Y*Z = 4*(Y^2 + Y*Z) := by ring,
                rw this at cond,
                have fourdivp : (4:ℤ) ∣ p := dvd.intro (Y^2 + Y*Z) cond,
                have natfourdivp : int.nat_abs 4 ∣ p := int.coe_nat_dvd_right.mp fourdivp,
                have : int.nat_abs 4 = 4 := rfl,
                rw this at natfourdivp,
                have : p % 4 = 0 := nat.mod_eq_zero_of_dvd natfourdivp,
                rw this at p1mod4,
                finish,
            },
            linarith,
            split, linarith, exact ypos,
        end
        ⟩,
end


lemma i_invo (p : ℕ) (pprime : nat.prime p) (p1mod4 : p % 4 = 1) : funcpow (i p pprime p1mod4) 2 =  @id (S p) :=
begin
    ext1 v,
    rcases v with ⟨⟨X1, Y1, Z1⟩, ⟨cond, x1pos, y1pos, z1pos⟩⟩,
    unfold funcpow,
    simp [i],
    dsimp,
    split_ifs,
    {
        rw dif_pos h,
        simp,
        have : ¬ (X1 + 2 * Z1 + (Y1 +(- X1 +- Z1)) < Z1) := 
            by linarith,
        rw dif_neg this,
        have : ¬ (X1 + 2 * Z1 < 2 * Z1) :=
            by linarith,
        rw dif_neg this,
        simp,
        ring,
    },
    {
        rw dif_neg h,
        split_ifs,
        {
            rw dif_pos h_1,
            simp,
            have : ¬ (2 * Y1 +- X1 + (X1 +(Z1 +- Y1)) < Y1) :=
                by linarith,
            rw dif_neg this,
            have : (2 * Y1 +- X1 < 2 * Y1) :=
                by linarith,
            rw dif_pos this,
            simp,
            ring,
        },
        {
            rw dif_neg h_1,
            simp,
            have : (X1 +- (2 * Y1) + Y1 < X1 +(Z1 +- Y1)) :=
                by linarith,
            rw dif_pos this,
            simp,
            ring,
        },
    },
end

lemma mainn (p : ℕ) (pprime : nat.prime p) (p1mod4 : p % 4 = 1) : fintype.card (S p) ≡ 1 [MOD 2] := begin
    -- Because of this we have an action of Z/2
    letI actioni : mul_action (fin 2) (S p) := finorder_end_cyclic_action (i_invo p pprime p1mod4),
    let fixp_i := fixed_points (fin 2) (S p),

    haveI : fintype fixp_i := set_fintype _,

    have one_fixed_i : fintype.card fixp_i = 1 := begin
    rw fintype.card_eq_one_iff,

    -- A result that will be useful later
    have p_eq_one_plus_four_mul := nat.mod_add_div p 4,
    rw p1mod4 at p_eq_one_plus_four_mul,

    use [1,1,p/4],
    -- We will show (1,1, p/4) is the unique fixed point of i
    -- Note this is floor division, so really it is (p - 1)/4
    {
        repeat{split},
        -- Show that this is in the set
        -- TODO omg this is so ugly
        rw [one_pow, mul_one],
        norm_cast,
        exact p_eq_one_plus_four_mul,
        cases pprime,
        have : p ≥ 4 := begin
            by_contradiction,
            have : p < 4 := not_le.mp a,
            have : p = 1 := begin
                have := nat.mod_eq_of_lt this,
                rwa this at p1mod4,
            end,
            rw this at pprime_left,
            exact absurd pprime_left dec_trivial,
        end,
        have this : p / 4 ≥ 4 / 4 := nat.div_le_div_right this,
        rw @nat.div_self 4 dec_trivial at this,
        --exact (gt_from_lt (p / 4) 0).mp this,
        exact int.coe_nat_lt.mpr this,
    },
    {
        -- Now we show this is a fixed point
        intros v,
        simp only [one_pow, add_zero, mul_one, one_mul, mem_stabilizer_iff, nat.cast_id,
            zero_mul, not_lt, add_comm, int.coe_nat_inj', not_le, int.coe_nat_bit0,
            int.coe_nat_one, pow_one, int.coe_nat_lt, zero_add, add_right_inj, sub_nonpos, int.nat_abs,
            nat.div_self, sub_eq_add_neg, zero_ne_one, mul_zero, add_left_comm],
        cases nat_lt_two_is_zero_one v.is_lt,
        {
            -- Fixed by the identity element
            have vone : v = monoid.one (fin 2) := (fin.ext_iff v (monoid.one (fin 2))).mpr h,
            simp only [vone],
            exact mul_action.one_smul (fin 2) _,
        },
        {
            -- Fixed by the non-identity element, i.e. by i
            have : v = (⟨1, nat.lt_succ_self 1⟩ : (fin 2)) := (fin.ext_iff v ⟨1, nat.lt_succ_self 1⟩).mpr h,
            unfold has_scalar.smul,
            simp only [this],
            unfold_coes,
            dsimp,
            simp only [i, one_pow, add_zero, mul_one, one_mul, nat.cast_id, zero_mul, not_lt,
                add_comm, int.coe_nat_inj', not_le, int.coe_nat_bit0, int.coe_nat_one, pow_one, int.coe_nat_lt,
                zero_add, add_right_inj, sub_nonpos, int.nat_abs, nat.div_self, sub_eq_add_neg,
                zero_ne_one, mul_zero, add_left_comm],
            apply subtype.eq,
            have not_one_plus_p_div_four_lt_one : ¬ (1 + int.of_nat p / 4 < 1) := begin simp only [not_lt, le_add_iff_nonneg_right], end,
            have one_lt_two_mul_one : ((1 :ℤ) < 2*1) := dec_trivial,
            -- have : 1 + int.of_nat p / 4 ≥ 1 := sub_le_iff_le_add'.mp (int.coe_zero_le (p / 4)), end,
            simp only [dif_neg not_one_plus_p_div_four_lt_one, dif_pos one_lt_two_mul_one, true_and,
                one_pow, add_zero, mul_one, dif_pos, one_mul, nat.cast_id,
                zero_mul, not_lt, prod.mk.inj_iff, add_comm, int.coe_nat_inj', not_le,
                int.coe_nat_bit0, int.coe_nat_one, pow_one, int.coe_nat_lt, add_neg_cancel_left, dif_neg,
                zero_add, add_right_inj, sub_nonpos, int.nat_abs, nat.div_self,
                sub_eq_add_neg, zero_ne_one, mul_zero, add_left_comm],
            norm_num,
        },
    },
    {
        -- Now show the fixed point was unique, any other is the same
        rintro ⟨⟨⟨ X, Y, Z⟩, ⟨cond, xpos, ypos, zpos ⟩⟩, hf⟩,
        simp only [one_pow, add_zero, mul_one, dif_pos, one_mul,
            mem_stabilizer_iff, zero_mul, not_lt, prod.mk.inj_iff, add_comm, int.coe_nat_inj', not_le, int.coe_nat_one,
            subtype.mk_eq_mk, pow_one, le_add_iff_nonneg_right, int.coe_nat_lt, add_neg_cancel_left, dif_neg, zero_add, and_self,
            sub_nonpos, int.nat_abs, nat.div_self, sub_eq_add_neg, zero_ne_one, mul_zero, add_left_comm, mem_fixed_points] at *,
        simp only [mem_fixed_points] at *,
        have := hf (⟨ 1, nat.lt_succ_self 1 ⟩ : (fin 2)),
        unfold has_scalar.smul at this,
        unfold_coes at *,
        simp only [i, funcpow_zero, add_zero, mul_one, one_mul, zero_mul,
            not_lt, add_comm, function.comp.right_id, pow_one, funcpow_succ, zero_add,
            sub_nonpos, int.nat_abs, sub_eq_add_neg, zero_ne_one,
            mul_zero, add_left_comm] at this,
        split_ifs at this,
        {
            simp at this,
            cases this,
            
            have := eq_sub_of_add_eq' this_left,
            simp only [add_right_neg, sub_eq_add_neg, mul_eq_zero] at this,
            have two_not_zero : ¬(2=(0:ℤ)):= begin norm_num, end,
            have := or.resolve_left this two_not_zero,
            exact absurd (ne_of_gt zpos) (not_not.mpr this),
        },
        {
            simp at this,
            cases this with eq1 eq2,
            have xeqy : X = Y := begin
                have : X + (-Y  + Z) = Z := begin
                rwa (add_comm (-Y) Z),
                end,
                rw [←add_assoc] at this,
                have : (X + (-Y)) = Z-Z := eq_sub_of_add_eq this,
                rw [sub_self Z] at this,
                have : X = -(-Y) := eq_neg_of_add_eq_zero this,
                rwa neg_neg at this,
            end,
            rw [xeqy, pow_two, (mul_comm 4 Y), mul_assoc, ←(mul_add Y Y (4*Z))] at cond,
            have : Y ∣ p := begin
                simp only [(∣)],
                use (Y + 4 * Z),
                exact eq.symm cond,
            end,
            have : (int.nat_abs Y) ∣ p := int.coe_nat_dvd_right.mp this,
            have := pprime.2 (int.nat_abs Y) this,
            cases this,
            {
                have : Y = 1 := begin rwa ←int.nat_abs_of_nonneg (le_of_lt ypos), finish, end,
                split, rw xeqy, exact this,
                split, exact this,
                rw this at cond,
                rw one_mul at cond,
                have := eq_sub_of_add_eq' cond,

                rw ←p_eq_one_plus_four_mul at this,
                norm_num at this,
                rw [←sub_eq_zero, ←mul_sub, mul_eq_zero_iff_eq_zero_or_eq_zero] at this,
                cases this with four_zero z_eq_p_div_four,
                {
                    exact absurd four_zero (by norm_num),
                },
                {
                    rwa [←sub_eq_zero],
                }
            },
            {
                have : Y = p := begin rwa [←int.nat_abs_of_nonneg (le_of_lt ypos), int.coe_nat_eq_coe_nat_iff], end,
                rw this at cond,
                have : 1 < ((p : ℤ) + 4 * Z) := begin linarith [zpos], end,
                rw ←(mul_lt_mul_left (int.coe_nat_lt.mpr (nat.lt_of_succ_lt pprime.1))) at this,
                rw [mul_one, cond] at this,
                exact absurd this (irrefl (p : ℤ))
            }
        },
        {
            simp only [not_lt, prod.mk.inj_iff] at *,
            simp at this,
            cases this,
            
            have := eq_sub_of_add_eq' this_left,
            simp only [add_right_neg, sub_eq_add_neg, mul_eq_zero, add_right_neg, neg_eq_zero, sub_eq_add_neg, mul_eq_zero] at this,
            have two_not_zero: ¬(2=(0:ℤ)):= begin norm_num, end,
            have := or.resolve_left this two_not_zero,
            exact absurd (ne_of_gt ypos) (not_not.mpr this),
        },
    },
    end,
    have mainn := @card_modeq_card_fixed_points (fin 2) (S p) _ _ _ _ _ 2 1 two_prime card_fin_two,
    rw one_fixed_i at mainn,
    exact mainn,
end


-- introduce another involution
def j (p : ℕ) : (S p) → (S p) :=
begin
    rintro ⟨⟨X, Y, Z⟩, P⟩,
    exact ⟨(X, Z, Y),
        begin
            rcases P with ⟨ cond, xpos, ypos, zpos ⟩,
            unfold property,
            rw [←cond] at *,
            finish,
        end ⟩
end

lemma j_invo (p : ℕ): funcpow (j p) 2 = id :=
begin
    funext v,
    rcases v with ⟨⟨X1, Y1, Z1⟩, P⟩,
    apply subtype.eq,
    simp [j],
end

instance (p : ℕ) : mul_action (fin 2) (S p) := finorder_end_cyclic_action (j_invo p)

def fixp_j (p : ℕ) := fixed_points (fin 2) (S p)

noncomputable instance finj (p : ℕ) : fintype (fixp_j p) := set_fintype _

lemma exists_fixed_j (p : ℕ) (pprime : nat.prime p) (p1mod4 : p % 4 = 1): nonempty (fixp_j p) := begin
    have mainj := @card_modeq_card_fixed_points _ _ _ _ _ _ (finj p) 2 1 two_prime card_fin_two,
    have l1 : 1 ≡ fintype.card ↥(fixed_points (fin 2) (S p)) [MOD 2] :=
        nat.modeq.trans (nat.modeq.symm (mainn p pprime p1mod4)) mainj,
    have l2 : fintype.card ↥(fixed_points (fin 2) (S p)) ≥ 0 :=
        zero_le (fintype.card ↥(fixed_points (fin 2) (S p))),
    have l3 : fintype.card ↥(fixed_points (fin 2) (S p)) ≠ 0 :=
    begin
        by_contradiction,
        finish,
    end,
    rw ←@fintype.card_pos_iff _ (finj p),
    exact zero_lt_iff_ne_zero.mpr l3,
end


theorem prime_1_mod_4_sum_square_square
(p : ℕ) (pprime : nat.prime p) (p1mod4 : p % 4 = 1) :
∃ (a b : ℤ), a^2 + b^2 = p :=
begin


-- TODO maybe there is a function like classical.inhabited_of_nonempty that can be used here
-- TODO as these are fintypes my non-logicial brain says I don't need choice really? Is that true
have one_fix' :=
begin
    choose t tw using exists_true_iff_nonempty.mpr (exists_fixed_j p pprime p1mod4),
    exact t,
end,

rcases one_fix' with ⟨ ⟨ ⟨Xfix, Yfix, Zfix⟩, ⟨cond, xpos, ypos, zpos⟩ ⟩, fixprop⟩,

have fix_pt_z_y_eq : Zfix = Yfix :=
begin
    dunfold fixp_j at fixprop,
    rw mem_fixed_points (S p) at fixprop,
    have := fixprop (⟨1, nat.lt_succ_self 1⟩ : (fin 2)),
    unfold has_scalar.smul at this,
    unfold_coes at this,
    simp only [funcpow, j, true_and, prod.mk.inj_iff, function.comp.right_id] at this,
    simp at this,
    exact this.left,
end,

have four_y_y_is_sq : 4 * Yfix * Yfix = (2 * Yfix) ^ 2 := 
begin
rw [pow_two],
rw [←mul_assoc],
conv in (2 * Yfix * 2)
begin
rw mul_comm,
end,
rw [← mul_assoc],
rw (dec_trivial : (2:ℤ) * 2 = 4),
end,
rw [fix_pt_z_y_eq, four_y_y_is_sq] at cond,

use [Xfix, 2 * Yfix],
exact cond,
end