group_theory_theorems.lean

import group.definitions -- definition of a group

namespace mygroup

variables {G : Type} [group G] -- let G be a group

/- 

Axioms for a group:

mul_assoc : ∀ (a b c : G), (a * b) * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
mul_left_inv : ∀ (a : G), a⁻¹ * a = 1

-/

-- First goal: prove a * 1 = a and a * a⁻¹ = 1


namespace group

attribute [simp] mul_left_inv one_mul

lemma mul_left_cancel (a x y : G)
  (Habac : a * x = a * y) : x = y := 
begin
  calc x = 1 * x         : by rw one_mul
  ...    = (a⁻¹ * a) * x : by rw mul_left_inv
  ...    = a⁻¹ * (a * x) : by rw mul_assoc
  ...    = a⁻¹ * (a * y) : by rw Habac
  ...    = y             : by rw [←mul_assoc, mul_left_inv, one_mul] 
end

lemma mul_eq_of_eq_inv_mul {a x y : G}
  (h : x = a⁻¹ * y) : a * x = y :=
begin
  apply mul_left_cancel a⁻¹,
  rw ←mul_assoc,
  simp,
  assumption
end

@[simp]
theorem mul_one (a : G) : a * 1 = a :=
begin
  apply mul_eq_of_eq_inv_mul,
  simp,
end

@[simp]
theorem mul_right_inv (a : G) : a * a⁻¹ = 1 :=
begin
  apply mul_eq_of_eq_inv_mul,
  simp
end

lemma eq_mul_inv_of_mul_eq {a b c : G} (h : a * c = b) : a = b * c⁻¹ :=
begin
  rw ←h,
  simp [mul_assoc],
end

lemma mul_left_eq_self {a b : G} : a * b = b ↔ a = 1 :=
begin
  sorry
end

lemma eq_inv_of_mul_eq_one {a b : G} (h : a * b = 1) : a = b⁻¹ :=
begin
  have h2 : (a * b) * b⁻¹ = 1 * b⁻¹,
    rw h, 
  simp [mul_assoc] at h2,
  assumption,
end

lemma inv_inv (a : G) : a ⁻¹ ⁻¹ = a :=
begin
  symmetry,
  apply eq_inv_of_mul_eq_one _,
  simp,
end

lemma inv_eq_of_mul_eq_one {a b : G} (h : a * b = 1) : a⁻¹ = b :=
begin
  sorry
end

end group

end mygroup