Mathlib.Algebra.Group.Subgroup.Order

import Std.Logic.Eq
import Mathlib.Logic.EqReasoning
import Mathlib.Algebra.Group.Basic
import Mathlib.Algebra.Group.Subgroup

def SubgroupLe.{u} :
  forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), Prop :=
  fun G => fun H => fun K => forall (x : G), forall (hx : H x), K x

def SubgroupEquiv.{u} :
  forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), Prop :=
  fun G => fun H => fun K => forall (P : Prop), forall (mk : forall (left : @SubgroupLe.{u} G H K), forall (right : @SubgroupLe.{u} G K H), P), P

def NormalContains.{u} :
  forall (G : Sort u), forall (N : forall (x : G), Prop), forall (H : forall (x : G), Prop), Prop :=
  fun G => fun N => fun H => forall (x : G), forall (hn : N x), H x

theorem subgroup_le_refl.{u} :
  forall (G : Sort u), forall (H : forall (x : G), Prop), @SubgroupLe.{u} G H H :=
  fun G => fun H => fun (x : G) => fun (hx : H x) => hx

theorem subgroup_le_trans.{u} :
  forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), forall (L : forall (x : G), Prop), forall (hk : @SubgroupLe.{u} G H K), forall (kl : @SubgroupLe.{u} G K L), @SubgroupLe.{u} G H L :=
  fun G => fun H => fun K => fun L => fun hk => fun kl => fun (x : G) => fun (hx : H x) => kl x (hk x hx)

theorem subgroup_equiv_intro.{u} :
  forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), forall (hk : @SubgroupLe.{u} G H K), forall (kh : @SubgroupLe.{u} G K H), @SubgroupEquiv.{u} G H K :=
  fun G => fun H => fun K => fun hk => fun kh => fun (P : Prop) => fun (mk : forall (left : @SubgroupLe.{u} G H K), forall (right : @SubgroupLe.{u} G K H), P) => mk hk kh

theorem subgroup_equiv_left.{u} :
  forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), forall (h_equiv_k : @SubgroupEquiv.{u} G H K), @SubgroupLe.{u} G H K :=
  fun G => fun H => fun K => fun h_equiv_k => h_equiv_k (@SubgroupLe.{u} G H K) (fun (hk : @SubgroupLe.{u} G H K) => fun (kh : @SubgroupLe.{u} G K H) => hk)

theorem subgroup_equiv_right.{u} :
  forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), forall (h_equiv_k : @SubgroupEquiv.{u} G H K), @SubgroupLe.{u} G K H :=
  fun G => fun H => fun K => fun h_equiv_k => h_equiv_k (@SubgroupLe.{u} G K H) (fun (hk : @SubgroupLe.{u} G H K) => fun (kh : @SubgroupLe.{u} G K H) => kh)

theorem subgroup_equiv_refl.{u} :
  forall (G : Sort u), forall (H : forall (x : G), Prop), @SubgroupEquiv.{u} G H H :=
  fun G => fun H => @subgroup_equiv_intro.{u} G H H (@subgroup_le_refl.{u} G H) (@subgroup_le_refl.{u} G H)

theorem subgroup_equiv_symm.{u} :
  forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), forall (h_equiv_k : @SubgroupEquiv.{u} G H K), @SubgroupEquiv.{u} G K H :=
  fun G => fun H => fun K => fun h_equiv_k => @subgroup_equiv_intro.{u} G K H (@subgroup_equiv_right.{u} G H K h_equiv_k) (@subgroup_equiv_left.{u} G H K h_equiv_k)

theorem subgroup_equiv_trans.{u} :
  forall (G : Sort u), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), forall (L : forall (x : G), Prop), forall (h_equiv_k : @SubgroupEquiv.{u} G H K), forall (k_equiv_l : @SubgroupEquiv.{u} G K L), @SubgroupEquiv.{u} G H L :=
  fun G => fun H => fun K => fun L => fun h_equiv_k => fun k_equiv_l => @subgroup_equiv_intro.{u} G H L (@subgroup_le_trans.{u} G H K L (@subgroup_equiv_left.{u} G H K h_equiv_k) (@subgroup_equiv_left.{u} G K L k_equiv_l)) (@subgroup_le_trans.{u} G L K H (@subgroup_equiv_right.{u} G K L k_equiv_l) (@subgroup_equiv_right.{u} G H K h_equiv_k))

theorem normal_contains_to_subgroup_le.{u} :
  forall (G : Sort u), forall (N : forall (x : G), Prop), forall (H : forall (x : G), Prop), forall (contains : @NormalContains.{u} G N H), @SubgroupLe.{u} G N H :=
  fun G => fun N => fun H => fun contains => contains

theorem subgroup_le_to_normal_contains.{u} :
  forall (G : Sort u), forall (N : forall (x : G), Prop), forall (H : forall (x : G), Prop), forall (le : @SubgroupLe.{u} G N H), @NormalContains.{u} G N H :=
  fun G => fun N => fun H => fun le => le

theorem normal_contains_refl.{u} :
  forall (G : Sort u), forall (N : forall (x : G), Prop), @NormalContains.{u} G N N :=
  fun G => fun N => fun (x : G) => fun (hn : N x) => hn

theorem normal_contains_trans.{u} :
  forall (G : Sort u), forall (N : forall (x : G), Prop), forall (H : forall (x : G), Prop), forall (K : forall (x : G), Prop), forall (nh : @NormalContains.{u} G N H), forall (hk : @NormalContains.{u} G H K), @NormalContains.{u} G N K :=
  fun G => fun N => fun H => fun K => fun nh => fun hk => fun (x : G) => fun (hn : N x) => hk x (nh x hn)