AMC_problem.lean

import algebra
import algebra.gcd_domain
import tactic
import data.nat.gcd
import data.int.gcd

-- Let G be a group. Prove that, if there exist m and n coprime such that (xy)^m=(yx)^m 
-- and (xy)^n=(yx)^n, then G is commutative.

variables [G : Type] [group G] 
variables (m n : ℕ) 

lemma gcd_domain_integers: gcd_domain ℤ :=
begin
exact int.gcd_domain,
end

theorem Bezout_for_one (hmn: nat.gcd m n = 1): ∃ a b : ℤ, a * m + b * n = (1:ℕ):=
begin
use m.gcd_a n,
use m.gcd_b n,
rw ← hmn,
have fact: m.gcd_a n * m = m * m.gcd_a n,
{
    ring,
},
rw fact,
have fact': m.gcd_b n * n = n * m.gcd_b n,
{
    ring,
},
rw fact',
rw eq_comm,
exact nat.gcd_eq_gcd_ab m n,
end 

theorem AMC_problem (hmn: nat.gcd m n = 1) (hxym: ∀ x y : G, (x*y)^m=(y*x)^m) (hxyn: ∀ x y : G, (x * y)^n = (y * x)^n):
∀ x y : G, x * y = y * x:=
begin
intros x y,
specialize hxym x y,
specialize hxyn x y,
have fact1: ∃ a b : ℤ, a * m + b * n = (1:ℕ),
{
    exact Bezout_for_one m n hmn,
},
cases fact1 with a hab,
cases hab with b hab,
have factm: ∀ a : ℤ, (x * y)^(a * m) = (y * x)^(a * m),
{
   intro a,
   calc (x*y)^(a * ↑m)=(x*y)^(↑m * a): congr_arg (pow (x * y)) (mul_comm a m)
   ...=((x*y)^m)^a: by exact gpow_mul (x*y) m a
   ...=((y*x)^m)^a: congr_fun (congr_arg pow hxym) a
   ...=(y*x)^(↑m * a): by exact eq.symm (gpow_mul (y*x) m a)
   ...=(y*x)^(a * m): congr_arg (pow (y * x)) (eq.symm (mul_comm a m)),
},
have factn: ∀ b : ℤ, (x*y) ^ (b*n) = (y * x) ^ (b * n),
{
    intro b,
    calc (x * y)^(b * ↑n) = (x * y)^(↑n * b): congr_arg (pow (x*y)) (mul_comm b n)
    ...=((x*y)^n)^b: by exact gpow_mul (x*y) n b
    ...=((y*x)^n)^b: congr_fun (congr_arg pow hxyn) b
    ...=(y*x)^(↑n * b): by exact eq.symm(gpow_mul  (y*x) n b)
    ...=(y * x)^(b * ↑n): congr_arg (pow (y*x)) (eq.symm (mul_comm b n)),
},
specialize factm a,
specialize factn b,
have factmn: (x*y)^(a*m+b*n)=(y*x)^(a*m+b*n),
{
   calc (x*y)^(a*m+b*n)=(x*y)^(a*m) * (x*y)^(b*n): gpow_add (x * y) (a * ↑m) (b * ↑n)
   ...= (y*x)^(a*m) * (x * y)^(b*n): congr_fun (congr_arg has_mul.mul factm) ((x * y) ^ (b * ↑n))
   ...= (y*x)^(a*m) * (y*x)^(b*n): congr_arg (has_mul.mul ((y * x) ^ (a * ↑m))) factn
   ...= (y*x)^(a*m+b*n): (gpow_add (y * x) (a * ↑m) (b * ↑n)).symm,
},
rw hab at factmn,
rw ← gpow_one (x*y),
rw ← gpow_one (y*x),
exact factmn,
end