Lemma_about_monoids.lean

import algebra 
import tactic
import init.data.nat.basic init.data.nat.div init.meta init.algebra.functions

lemma not_injective_pow {M : Type*} [monoid M] [fintype M] (a : M) : ∃ i j : ℕ, i ≠ j ∧ a ^ i = a ^ j :=
begin
  have := not_injective_infinite_fintype (λ i : ℕ, a ^ i),
  rw [function.injective] at this,
  push_neg at this,
  tauto,
end

lemma gt_eq_sum (i j : ℕ) (H : i < j) : ∃ k : ℕ , j = i + k:=
begin
have fact1: i≤j,
{
    exact le_of_lt H,
},
have fact2: ∃ k : ℕ , k + i = j,
{use j - i, exact nat.sub_add_cancel fact1,},
cases fact2 with k hk, use k, linarith,
end

theorem add_theorem_ {n m : ℕ} (h : m ≤ n) : m + (n - m) = n :=
by rw [add_comm, nat.sub_add_cancel h]

lemma idempotent_in_monoid (M : Type*) [monoid M] [fintype M] (x : M) (i j k: ℕ) (hij: j<i) (hk : i = j + k) (hm: ∀ m : ℕ, x^j=x^(j+m*k)):
x^(i*k)=x^(2*i*k) :=
begin
have hk': 1 ≤ k,
{
  rw ← norm_num.sub_nat_pos i j k (eq.symm hk),
  exact nat.succ_le_iff.mpr (nat.sub_pos_of_lt hij),
},
have fact: 0<i*k-j,
{
  calc 0<i-j: nat.sub_pos_of_lt hij
  ...=i*1-j: by ring
  ...≤i*k-j: nat.sub_le_sub_right (nat.mul_le_mul_left i hk') j,
},
have h2: 0 < i*k-j, {linarith,}, have h3: j ≤ i*k,{exact le_of_lt (nat.lt_of_sub_pos fact),},
have h3: i*k-j+j=i*k,{rw add_comm, rw [add_comm, nat.sub_add_cancel h3],},
have fact1: x^(i*k)=x^(i*k-j+j),{rw h3,}, have h4: (i*k-j)+(j+i*k)=i*k-j+j+i*k,{rw add_assoc,},
have h5: 2*i*k=i*k+i*k,{ring,},
have h6: i*k-j+j+i*k=2*i*k,{rw add_comm,rw h3,ring,},
have fact: x^(i*k)=x^(2*i*k),
{
  calc x^(i*k)=x^(i*k-j+j): congr_arg (pow x) (eq.symm h3)
  ...=x^(i*k-j)*x^j: pow_add x (i * k - j) j
  ...=x^(i*k-j)*x^(j+i*k): congr_arg (has_mul.mul (x ^ (i * k - j))) (hm i)
  ...=x^((i*k-j)+(j+i*k)): tactic.ring.pow_add_rev x (i * k - j) (j + i * k)
  ...=x^(i*k-j+j+i*k): congr_arg (pow x) h4
  ...=x^(2*i*k): congr_arg (pow x) h6,
},
exact fact,
end

open classical
local attribute [instance] prop_decidable

--Let M be a finite monoid such that there exists a p ∈ ℕ with the property that ∀ a : M different from the unity, a^(p+1) ≠ a. 
--Let x ∈ M, different from the unity. Prove that there exists an n ∈ ℕ bigger than 1 such that x^n=(1:M) (aka M is a group).

lemma mul_equal_fin_OJM_2018 {M:Type*} [monoid M] [fintype M] (p : ℕ) (h: ∀ a : M, a ≠ (1:M) → a^(p+1) ≠ a) (x : M) (hx: x ≠ (1:M)):
∃ n : ℕ , x^n=(1:M) ∧ 1≤n :=
begin
have h': ∀ a : M, a≠(1:M) → a^(p+1) ≠ a,{exact h,},
specialize h x hx,have fact: ∃ i j : ℕ, i ≠ j ∧ x ^ i = x ^ j,{exact not_injective_pow x,},
cases fact with i hj,
cases hj with j hj,
cases hj with neqij eqij,
have neqij2: i>j ∨ i<j,{exact lt_or_gt_of_ne (ne.symm neqij),},

--First case: i > j.

by_cases neqij2 : i>j,
{have jik: ∃ k : ℕ , i = j + k,{exact gt_eq_sum j i neqij2,},
cases jik with k hk,
have fact: x^j=x^(j+k),{exact (eq.symm eqij).trans (congr_arg (pow x) hk),},
have fact2: ∀ m : ℕ , x^j=x^(j+m*k),
{
  intro t,induction t with m hm,{ring,},
  { have fact2: x^(j+m.succ*k)=x^j,
    {calc x^(j+m.succ*k)=x^(j+(m+1)*k) : rfl
    ...=x^(j+m*k+k): by ring
    ...=x^(j+m*k)*x^k: pow_add x (j + m * k) k
    ...=x^j*x^k: congr_fun (congr_arg has_mul.mul (eq.symm hm)) (x ^ k)
    ...=x^(j+k): tactic.ring.pow_add_rev x j k
    ...=x^j: eq.symm fact,},
    exact eq.symm fact2,
  },
},have fact3: 0<i-j, {exact nat.sub_pos_of_lt neqij2,},
have kij: i-j=k, {exact norm_num.sub_nat_pos i j k (eq.symm hk),}, rw kij at fact3,
have fact4: 1≤k, {exact nat.succ_le_iff.mpr fact3,}, have observation: x^(i*k)=x^(2*i*k), {exact idempotent_in_monoid M x i j k neqij2 hk fact2,},
have zeroi: 0<i,
{calc 0 ≤ j: zero_le j
...<i: by exact neqij2,
},
have onei: 1≤i,{exact nat.succ_le_iff.mpr zeroi,},have obs: 0<i*k,{exact mul_pos zeroi fact3,},
have obs': 1≤i*k,{exact nat.succ_le_iff.mpr obs,},use i*k,
split,
{
  clear obs zeroi fact3,
  have obs: ∀ n : ℕ, 0<(n+1) ∧ x^(i*k)=x^((n+1)*i*k),
  {
  intro n,
  induction n with n hn,{split, {rw zero_add, exact nat.one_pos,}, {rw zero_add, rw one_mul,},},
  {
    cases hn with hn' prop,
    split,{exact nat.lt.step hn',},
    {
      have fact5: n.succ=n+1, {refl,}, rw fact5 at *, have fact6: n+1+1=n+2, {refl,}, rw fact6 at *, 
      have fact7: ((n+1)*i*k)=(n*i*k)+(i*k),{linarith,},
      have fact8: x^((n+1)*i*k)=x^(n*i*k)*x^(i*k),
      {
        calc x^((n+1)*i*k)=x^((n*i*k)+(i*k)): congr_arg (pow x) fact7
        ...=x^(n*i*k)*x^(i*k): pow_add x (n * i * k) (i * k),
      },
      clear fact5 fact6 fact7, rw observation at fact8,
      have fact9: n*i*k+2*i*k=(n+2)*i*k, {linarith,},
      have fact10: x^((n+1)*i*k)=x^((n+2)*i*k),
      {
        calc x^((n+1)*i*k)=x^(n*i*k)*x^(2*i*k): by exact fact8
        ...=x^(n*i*k+2*i*k): tactic.ring.pow_add_rev x (n * i * k) (2 * i * k)
        ...=x^((n+2)*i*k): congr_arg (pow x) fact9,
      },
      exact (rfl.congr fact10).mp prop,
    },
  },
  },
  clear onei obs' fact, specialize obs p, cases obs with hp ha,
  by_contradiction,
  change x^(i*k) ≠ 1 at a,
  specialize h' (x^(i*k)) a,
  have h'': (x^(i*k))^(p+1)=x^((i*k)*(p+1)), {exact eq.symm (pow_mul x (i*k) (p+1)),}, rw h'' at h',
  have obs3: (i*k)*(p+1)=(p+1)*i*k, {ring,}, clear h'' a, rw ← obs3 at ha,
  exact h' (eq.symm (ha)), 
},
{exact obs',},},

--This is where the second implication begins.

{have neqij3: i≤j, {exact not_lt.mp neqij2,},
clear neqij2 neqij2, have neqij2: i<j,{exact lt_of_le_of_ne neqij3 neqij,},clear neqij neqij3,
have jik: ∃ k : ℕ , j = i + k,{exact gt_eq_sum i j neqij2,}, cases jik with k hk,
have fact: x^i=x^(i+k),{exact eq.trans eqij (congr_arg (pow x) hk),},
have fact2: ∀ m : ℕ , x^i=x^(i+m*k), {intro t, induction t with m hm, {ring,},
  { have fact2: x^(i+m.succ*k)=x^i,
    {calc x^(i+m.succ*k)=x^(i+(m+1)*k) : rfl
    ...=x^(i+m*k+k): by ring
    ...=x^(i+m*k)*x^k: pow_add x (i + m * k) k
    ...=x^i*x^k: congr_fun (congr_arg has_mul.mul (eq.symm hm)) (x ^ k)
    ...=x^(i+k): tactic.ring.pow_add_rev x i k
    ...=x^i: eq.symm fact,},
    exact eq.symm fact2,
  },
},
have fact3: 0<j-i, {exact nat.sub_pos_of_lt neqij2,},
have kij: j-i=k, {exact norm_num.sub_nat_pos j i k (eq.symm hk),},rw kij at fact3,
have fact4: 1≤k, {exact nat.succ_le_iff.mpr fact3,},
have observation: x^(j*k)=x^(2*j*k), {exact idempotent_in_monoid M x j i k neqij2 hk fact2,  },
have zeroj: 0<j, {
  calc 0 ≤ i: zero_le i
  ...<j: by exact neqij2,
},
have onei: 1≤j, {exact nat.succ_le_iff.mpr zeroj,},have obs: 0<j*k, {exact mul_pos zeroj fact3,},
have obs': 1≤j*k, {exact nat.succ_le_iff.mpr obs,}, use j*k,
split,
{
  clear obs zeroj fact3,
  have obs: ∀ n : ℕ, 0<(n+1) ∧ x^(j*k)=x^((n+1)*j*k), 
  {intro n, induction n with n hn,
  {split, {rw zero_add, exact nat.one_pos,}, {rw zero_add,rw one_mul,},},
  {
    cases hn with hn' prop,
    split, {exact nat.lt.step hn',},
    {
      have fact5: n.succ=n+1,{refl,}, rw fact5 at *, have fact6: n+1+1=n+2, {exact rfl,}, rw fact6 at *,
      have fact7: ((n+1)*j*k)=(n*j*k)+(j*k),{linarith,},
      have fact8: x^((n+1)*j*k)=x^(n*j*k)*x^(j*k),
      {
        calc x^((n+1)*j*k)=x^((n*j*k)+(j*k)): congr_arg (pow x) fact7
        ...=x^(n*j*k)*x^(j*k): pow_add x (n * j * k) (j * k),
      },
      clear fact5 fact6 fact7, rw observation at fact8, have fact9: n*j*k+2*j*k=(n+2)*j*k, {linarith,},
      have fact10: x^((n+1)*j*k)=x^((n+2)*j*k),
      {
        calc x^((n+1)*j*k)=x^(n*j*k)*x^(2*j*k): by exact fact8
        ...=x^(n*j*k+2*j*k): tactic.ring.pow_add_rev x (n * j * k) (2 * j * k)
        ...=x^((n+2)*j*k): congr_arg (pow x) fact9,
      },
      exact (rfl.congr fact10).mp prop,
    },
  },
  },
  clear onei obs' fact, specialize obs p, cases obs with hp ha,
  by_contradiction, change x^(j*k) ≠ 1 at a, specialize h' (x^(j*k)) a,
  have h'': (x^(j*k))^(p+1)=x^((j*k)*(p+1)), {exact eq.symm (pow_mul x (j*k) (p+1)),}, rw h'' at h',
  have obs3: (j*k)*(p+1)=(p+1)*j*k, {ring,},clear h'' a, rw ← obs3 at ha, exact h' (eq.symm (ha)), 
},
{exact obs',},},

end

--Another problem about monoids: In all finite monoids, one can build an idempotent element from any element x. The first lemma 
--that I proved had one extra condition, this one is free of it.

lemma idempotent_in_fin_monoid (M:Type*) [monoid M] [fintype M] (x:M): 
∃ n : ℕ, 1 ≤ n ∧ x^n=x^(2*n):=
begin
have fact: ∃ i j : ℕ, i ≠ j ∧ x^i=x^j, {exact not_injective_pow x,},
cases fact  with i j, cases j with j hij, cases hij with neqij hij,
have obs: i < j ∨ j < i, {exact lt_or_gt_of_ne neqij,},
by_cases obs: i<j, 
{
have hk: ∃ k : ℕ, j = i + k, {exact gt_eq_sum i j obs,}, cases hk with k hk, rw hk at hij,
have fact2: ∀ m : ℕ , x^i=x^(i+m*k),
{
  intro t,
  induction t with m hm, {ring,},
  { have fact2: x^(i+m.succ*k)=x^i,
    {calc x^(i+m.succ*k)=x^(i+(m+1)*k) : rfl
    ...=x^(i+m*k+k): by ring
    ...=x^(i+m*k)*x^k: pow_add x (i + m * k) k
    ...=x^i*x^k: congr_fun (congr_arg has_mul.mul (eq.symm hm)) (x ^ k)
    ...=x^(i+k): tactic.ring.pow_add_rev x i k
    ...=x^i: eq.symm hij,},
    exact eq.symm fact2,
  },
},
have obs': k = j - i,{rw hk, rw add_comm, exact (nat.add_sub_cancel k i).symm,},
have hk': 1 ≤ k,{ rw ← norm_num.sub_nat_pos j i k (eq.symm hk), linarith,},use j*k,
have fact: 0<j*k-i,
{
  calc 0<j-i: nat.sub_pos_of_lt obs
  ...=j*1-i: by ring
  ...≤j*k-i: nat.sub_le_sub_right (nat.mul_le_mul_left j hk') i,
},
have h2: 0 ≤ j*k-i,{linarith,},
have h3: i ≤ j*k, {exact le_of_lt (nat.lt_of_sub_pos fact),},
have h4: 2*j*k=2*(j*k), {exact mul_assoc 2 j k,},
have h5: j*k-i+i=j*k, {rw add_comm,exact add_theorem_ h3,},
have h6: x^(j*k)=x^(j*k-i+i), {rw h5,},
have h7: (j*k-i)+(i+j*k)=j*k-i+i+j*k, {rw add_assoc,}, have h8: 2*j*k=j*k+j*k, {ring,},
have h9: j*k-i+i+j*k=2*j*k, {rw add_comm, rw h5, ring, },
have fact': x^(j*k)=x^(2*j*k),
{
  calc x^(j*k)=x^(j*k-i+i): congr_arg (pow x) (eq.symm h5)
  ...=x^(j*k-i)*x^i: pow_add x (j * k - i) i
  ...=x^(j*k-i)*x^(i+j*k): congr_arg (has_mul.mul (x ^ (j * k - i))) (fact2 j)
  ...=x^((j*k-i)+(i+j*k)): tactic.ring.pow_add_rev x (j * k - i) (i + j * k)
  ...=x^(j*k-i+i+j*k): congr_arg (pow x) h7
  ...=x^(2*j*k): congr_arg (pow x) h9,
},
have i0: 0 ≤ i, {exact zero_le i,},
have jk0: 0 < j*k,
{ have h1: i<j*k,{exact nat.lt_of_sub_pos fact,}, 
  calc 0 ≤ i: by exact i0
  ...< j * k: h1,
},
have jk1: 1 ≤ j*k,{exact nat.succ_le_iff.mpr jk0,}, clear h2 h3 h5 h6 h7 h8 h9 i0 jk0 fact fact2,
split, {exact jk1,}, {rw h4 at fact', exact fact',},},
{
 have ij: j ≤ i, {exact not_lt.mp obs,}, 
 have hk': ∃ k : ℕ, i = j + k, {exact gt_eq_sum j i (lt_of_le_of_ne ij (ne.symm neqij)),},
 cases hk' with k hk',
 have hk: k = i - j, {rw hk', rw add_comm, exact (nat.add_sub_cancel k j).symm},
 use i*k, clear obs obs,
 have fact': 0 < i-j, {exact nat.sub_pos_of_lt (lt_of_le_of_ne ij (ne.symm neqij)),},
 have fact : 1 ≤ i-j, {exact nat.succ_le_iff.mpr fact',},rw ← hk at fact,
 have j0: 0 ≤ j, {exact zero_le j,}, have i0: 0 < i,{linarith,}, have i1: 1 ≤ i, {exact nat.succ_le_iff.mpr i0,},
 have ik1: 1 ≤ i*k,
 {
   calc 1 ≤ i: by exact i1
   ...=i*1: by ring
   ...≤ i*k : (mul_le_mul_left i0).mpr fact,
 },


have fact3: ∀ m : ℕ , x^j=x^(j+m*k),
{
  intro t,
  induction t with m hm, {ring,},
  { have fact2: x^(j+m.succ*k)=x^j,
    {calc x^(j+m.succ*k)=x^(j+(m+1)*k) : rfl
    ...=x^(j+m*k+k): by ring
    ...=x^(j+m*k)*x^k: pow_add x (j + m * k) k
    ...=x^j*x^k: congr_fun (congr_arg has_mul.mul (eq.symm hm)) (x ^ k)
    ...=x^(j+k): tactic.ring.pow_add_rev x j k
    ...=x^i: congr_arg (pow x) (eq.symm hk')
    ...=x^j: hij,},
    exact eq.symm fact2,
  },
},
have fact: 0<i*k-j,
{
  have obs': j < i, {exact lt_of_le_of_ne ij (ne.symm neqij),},
  calc 0<i-j: nat.sub_pos_of_lt obs'
  ...=i*1-j: by ring
  ...≤i*k-j: nat.sub_le_sub_right (nat.mul_le_mul_left i fact) j,
},
have h1: j<i*k, {exact nat.lt_of_sub_pos fact,}, have h2: j ≤ i*k,{exact le_of_lt (nat.lt_of_sub_pos fact),},
have h3: 2*i*k=2*(i*k), {exact mul_assoc 2 i k,},
have h4: i*k-j+j=i*k, {rw add_comm, exact add_theorem_ h2,}, have h6: x^(i*k)=x^(i*k-j+j), {rw h4,},
have h7: (i*k-j)+(j+i*k)=i*k-j+j+i*k, {rw add_assoc,}, have h8: 2*i*k=i*k+i*k, {ring},
have h9: i*k-j+j+i*k=2*i*k, {rw add_comm,rw h4, ring,},
have fact': x^(i*k)=x^(2*i*k),
{
  calc x^(i*k)=x^(i*k-j+j): congr_arg (pow x) (eq.symm h4)
  ...=x^(i*k-j)*x^j: pow_add x (i * k - j) j
  ...=x^(i*k-j)*x^(j+i*k): congr_arg (has_mul.mul (x ^ (i * k - j))) (fact3 i)
  ...=x^((i*k-j)+(j+i*k)): tactic.ring.pow_add_rev x (i * k - j) (j + i * k)
  ...=x^(i*k-j+j+i*k): congr_arg (pow x) h7
  ...=x^(2*i*k): congr_arg (pow x) h9,
},
split, {exact ik1,}, {rw h3 at fact', exact fact',},},
end