Mathlib.Algebra.Group.SecondIsomorphism.Image

import Std.Logic.Eq
import Mathlib.Logic.EqReasoning
import Mathlib.Algebra.Group.Basic
import Mathlib.Algebra.Group.Subgroup
import Mathlib.Algebra.Group.Quotient
import Mathlib.Algebra.Group.Quotient.Mul
import Mathlib.Algebra.Group.Quotient.Group
import Mathlib.Algebra.Group.SecondIsomorphism.Map

def SecondIsoImagePred.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (normal_args : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (Hpred : forall (x : G), Prop), forall (q : @NormalQuot.{u} G one mul inv N group_args normal_args), Prop :=
  fun G => fun one => fun mul => fun inv => fun N => fun group_args => fun normal_args => fun Hpred => fun q => forall (P : Prop), forall (mk : forall (h : G), forall (hh : Hpred h), forall (eq_phi : @Eq.{succ u} (@NormalQuot.{u} G one mul inv N group_args normal_args) (@SecondIsoPhi.{u} G one mul inv N group_args normal_args Hpred h hh) q), P), P

def SecondIsoProductQuotPred.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (normal_args : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (Hpred : forall (x : G), Prop), forall (q : @NormalQuot.{u} G one mul inv N group_args normal_args), Prop :=
  fun G => fun one => fun mul => fun inv => fun N => fun group_args => fun normal_args => fun Hpred => fun q => forall (P : Prop), forall (mk : forall (x : G), forall (hx : @SubgroupProductPred.{succ u} G mul Hpred N x), forall (eq_q : @Eq.{succ u} (@NormalQuot.{u} G one mul inv N group_args normal_args) (@NormalQuotMk.{u} G one mul inv N group_args normal_args x) q), P), P

theorem second_iso_image_intro.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (normal_args : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (Hpred : forall (x : G), Prop), forall (h : G), forall (hh : Hpred h), @SecondIsoImagePred.{u} G one mul inv N group_args normal_args Hpred (@SecondIsoPhi.{u} G one mul inv N group_args normal_args Hpred h hh) :=
  fun G => fun one => fun mul => fun inv => fun N => fun group_args => fun normal_args => fun Hpred => fun h => fun hh => fun (P : Prop) => fun (mk : forall (h2 : G), forall (hh2 : Hpred h2), forall (eq_phi : @Eq.{succ u} (@NormalQuot.{u} G one mul inv N group_args normal_args) (@SecondIsoPhi.{u} G one mul inv N group_args normal_args Hpred h2 hh2) (@SecondIsoPhi.{u} G one mul inv N group_args normal_args Hpred h hh)), P) => mk h hh (@Eq.refl.{succ u} (@NormalQuot.{u} G one mul inv N group_args normal_args) (@SecondIsoPhi.{u} G one mul inv N group_args normal_args Hpred h hh))

theorem second_iso_image_elim.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (normal_args : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (Hpred : forall (x : G), Prop), forall (q : @NormalQuot.{u} G one mul inv N group_args normal_args), forall (img : @SecondIsoImagePred.{u} G one mul inv N group_args normal_args Hpred q), forall (P : Prop), forall (mk : forall (h : G), forall (hh : Hpred h), forall (eq_phi : @Eq.{succ u} (@NormalQuot.{u} G one mul inv N group_args normal_args) (@SecondIsoPhi.{u} G one mul inv N group_args normal_args Hpred h hh) q), P), P :=
  fun G => fun one => fun mul => fun inv => fun N => fun group_args => fun normal_args => fun Hpred => fun q => fun img => fun P => fun mk => img P mk

theorem second_iso_product_quot_intro.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (normal_args : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (Hpred : forall (x : G), Prop), forall (q : @NormalQuot.{u} G one mul inv N group_args normal_args), forall (x : G), forall (hx : @SubgroupProductPred.{succ u} G mul Hpred N x), forall (eq_q : @Eq.{succ u} (@NormalQuot.{u} G one mul inv N group_args normal_args) (@NormalQuotMk.{u} G one mul inv N group_args normal_args x) q), @SecondIsoProductQuotPred.{u} G one mul inv N group_args normal_args Hpred q :=
  fun G => fun one => fun mul => fun inv => fun N => fun group_args => fun normal_args => fun Hpred => fun q => fun x => fun hx => fun eq_q => fun (P : Prop) => fun (mk : forall (x2 : G), forall (hx2 : @SubgroupProductPred.{succ u} G mul Hpred N x2), forall (eq_q2 : @Eq.{succ u} (@NormalQuot.{u} G one mul inv N group_args normal_args) (@NormalQuotMk.{u} G one mul inv N group_args normal_args x2) q), P) => mk x hx eq_q

theorem second_iso_product_quot_elim.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (normal_args : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (Hpred : forall (x : G), Prop), forall (q : @NormalQuot.{u} G one mul inv N group_args normal_args), forall (prod : @SecondIsoProductQuotPred.{u} G one mul inv N group_args normal_args Hpred q), forall (P : Prop), forall (mk : forall (x : G), forall (hx : @SubgroupProductPred.{succ u} G mul Hpred N x), forall (eq_q : @Eq.{succ u} (@NormalQuot.{u} G one mul inv N group_args normal_args) (@NormalQuotMk.{u} G one mul inv N group_args normal_args x) q), P), P :=
  fun G => fun one => fun mul => fun inv => fun N => fun group_args => fun normal_args => fun Hpred => fun q => fun prod => fun P => fun mk => prod P mk

theorem second_iso_image_to_product_quot.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (normal_args : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (Hpred : forall (x : G), Prop), forall (q : @NormalQuot.{u} G one mul inv N group_args normal_args), forall (img : @SecondIsoImagePred.{u} G one mul inv N group_args normal_args Hpred q), @SecondIsoProductQuotPred.{u} G one mul inv N group_args normal_args Hpred q :=
  fun G => fun one => fun mul => fun inv => fun N => fun group_args => fun normal_args => fun Hpred => fun q => fun img => img (@SecondIsoProductQuotPred.{u} G one mul inv N group_args normal_args Hpred q) (fun (h : G) => fun (hh : Hpred h) => fun (eq_phi : @Eq.{succ u} (@NormalQuot.{u} G one mul inv N group_args normal_args) (@SecondIsoPhi.{u} G one mul inv N group_args normal_args Hpred h hh) q) => @second_iso_product_quot_intro.{u} G one mul inv N group_args normal_args Hpred q h (@subgroup_product_intro.{succ u} G mul Hpred N h h one hh (@subgroup_one.{succ u} G one mul inv N (@normal_subgroup_laws.{succ u} G one mul inv N normal_args)) (@group_mul_one.{succ u} G one mul inv group_args h)) (@eq_trans.{succ u} (@NormalQuot.{u} G one mul inv N group_args normal_args) (@NormalQuotMk.{u} G one mul inv N group_args normal_args h) (@SecondIsoPhi.{u} G one mul inv N group_args normal_args Hpred h hh) q (@eq_symm.{succ u} (@NormalQuot.{u} G one mul inv N group_args normal_args) (@SecondIsoPhi.{u} G one mul inv N group_args normal_args Hpred h hh) (@NormalQuotMk.{u} G one mul inv N group_args normal_args h) (@second_iso_phi_mk.{u} G one mul inv N group_args normal_args Hpred h hh)) eq_phi))

theorem second_iso_product_quot_to_image.{u} :
  forall (G : Sort succ u), forall (one : G), forall (mul : forall (a : G), forall (b : G), G), forall (inv : forall (a : G), G), forall (N : forall (x : G), Prop), forall (group_args : @GroupLawArgs.{succ u} G one mul inv), forall (normal_args : @NormalSubgroupLawArgs.{succ u} G one mul inv N), forall (Hpred : forall (x : G), Prop), forall (q : @NormalQuot.{u} G one mul inv N group_args normal_args), forall (prod : @SecondIsoProductQuotPred.{u} G one mul inv N group_args normal_args Hpred q), @SecondIsoImagePred.{u} G one mul inv N group_args normal_args Hpred q :=
  fun G => fun one => fun mul => fun inv => fun N => fun group_args => fun normal_args => fun Hpred => fun q => fun prod => prod (@SecondIsoImagePred.{u} G one mul inv N group_args normal_args Hpred q) (fun (x : G) => fun (hx : @SubgroupProductPred.{succ u} G mul Hpred N x) => fun (eq_q : @Eq.{succ u} (@NormalQuot.{u} G one mul inv N group_args normal_args) (@NormalQuotMk.{u} G one mul inv N group_args normal_args x) q) => hx (@SecondIsoImagePred.{u} G one mul inv N group_args normal_args Hpred q) (fun (h : G) => fun (n : G) => fun (hh : Hpred h) => fun (hn : N n) => fun (hx_eq : @Eq.{succ u} G (mul h n) x) => fun (P : Prop) => fun (mk : forall (h2 : G), forall (hh2 : Hpred h2), forall (eq_phi : @Eq.{succ u} (@NormalQuot.{u} G one mul inv N group_args normal_args) (@SecondIsoPhi.{u} G one mul inv N group_args normal_args Hpred h2 hh2) q), P) => mk h hh (@eq_trans.{succ u} (@NormalQuot.{u} G one mul inv N group_args normal_args) (@SecondIsoPhi.{u} G one mul inv N group_args normal_args Hpred h hh) (@NormalQuotMk.{u} G one mul inv N group_args normal_args h) q (@second_iso_phi_mk.{u} G one mul inv N group_args normal_args Hpred h hh) (@eq_trans.{succ u} (@NormalQuot.{u} G one mul inv N group_args normal_args) (@NormalQuotMk.{u} G one mul inv N group_args normal_args h) (@NormalQuotMk.{u} G one mul inv N group_args normal_args x) q (@normal_quot_sound.{u} G one mul inv N group_args normal_args h x (@normal_rel_product_right.{succ u} G one mul inv group_args N h n x hn hx_eq)) eq_q))))