Mathlib.Algebra.Group.FirstIsomorphism.Image

import Std.Logic.Eq
import Mathlib.Logic.EqReasoning
import Mathlib.Algebra.Group.Basic
import Mathlib.Algebra.Group.Image
import Mathlib.Algebra.Group.Kernel.Quotient
import Mathlib.Algebra.Group.Kernel.Quotient.Mul
import Mathlib.Algebra.Group.Kernel.Quotient.Group
import Mathlib.Algebra.Group.FirstIsomorphism

inductive FirstIsoQuotientAssocEvidence.{u,v} :
  forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), Prop where
| mk : forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), forall (law : forall (q1 : @KerQuot.{u,v} G H f), forall (q2 : @KerQuot.{u,v} G H f), forall (q3 : @KerQuot.{u,v} G H f), @Eq.{succ u} (@KerQuot.{u,v} G H f) (@KerQuotMul.{u,v} G oneG mulG invG H oneH mulH invH f hom_args (@KerQuotMul.{u,v} G oneG mulG invG H oneH mulH invH f hom_args q1 q2) q3) (@KerQuotMul.{u,v} G oneG mulG invG H oneH mulH invH f hom_args q1 (@KerQuotMul.{u,v} G oneG mulG invG H oneH mulH invH f hom_args q2 q3))), @FirstIsoQuotientAssocEvidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args

inductive FirstIsoQuotientOneMulEvidence.{u,v} :
  forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), Prop where
| mk : forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), forall (law : forall (q : @KerQuot.{u,v} G H f), @Eq.{succ u} (@KerQuot.{u,v} G H f) (@KerQuotMul.{u,v} G oneG mulG invG H oneH mulH invH f hom_args (@KerQuotOne.{u,v} G oneG H f) q) q), @FirstIsoQuotientOneMulEvidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args

inductive FirstIsoQuotientMulOneEvidence.{u,v} :
  forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), Prop where
| mk : forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), forall (law : forall (q : @KerQuot.{u,v} G H f), @Eq.{succ u} (@KerQuot.{u,v} G H f) (@KerQuotMul.{u,v} G oneG mulG invG H oneH mulH invH f hom_args q (@KerQuotOne.{u,v} G oneG H f)) q), @FirstIsoQuotientMulOneEvidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args

inductive FirstIsoQuotientInvMulEvidence.{u,v} :
  forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), Prop where
| mk : forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), forall (law : forall (q : @KerQuot.{u,v} G H f), @Eq.{succ u} (@KerQuot.{u,v} G H f) (@KerQuotMul.{u,v} G oneG mulG invG H oneH mulH invH f hom_args (@KerQuotInv.{u,v} G oneG mulG invG H oneH mulH invH f hom_args q) q) (@KerQuotOne.{u,v} G oneG H f)), @FirstIsoQuotientInvMulEvidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args

inductive FirstIsoQuotientMulInvEvidence.{u,v} :
  forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), Prop where
| mk : forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), forall (law : forall (q : @KerQuot.{u,v} G H f), @Eq.{succ u} (@KerQuot.{u,v} G H f) (@KerQuotMul.{u,v} G oneG mulG invG H oneH mulH invH f hom_args q (@KerQuotInv.{u,v} G oneG mulG invG H oneH mulH invH f hom_args q)) (@KerQuotOne.{u,v} G oneG H f)), @FirstIsoQuotientMulInvEvidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args

inductive FirstIsoQuotientGroupEvidence.{u,v} :
  forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), Prop where
| mk : forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), forall (assoc : @FirstIsoQuotientAssocEvidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args), forall (one_mul : @FirstIsoQuotientOneMulEvidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args), forall (mul_one : @FirstIsoQuotientMulOneEvidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args), forall (inv_mul : @FirstIsoQuotientInvMulEvidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args), forall (mul_inv : @FirstIsoQuotientMulInvEvidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args), @FirstIsoQuotientGroupEvidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args

inductive FirstIsoImageGroupEvidence.{u,v} :
  forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), Prop where
| mk : forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), forall (one_member : @ImagePred.{succ u,succ v} G H f oneH), forall (mul_closed : forall (x : H), forall (y : H), forall (hx : @ImagePred.{succ u,succ v} G H f x), forall (hy : @ImagePred.{succ u,succ v} G H f y), @ImagePred.{succ u,succ v} G H f (mulH x y)), forall (inv_closed : forall (y : H), forall (hy : @ImagePred.{succ u,succ v} G H f y), @ImagePred.{succ u,succ v} G H f (invH y)), @FirstIsoImageGroupEvidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args

inductive FirstIsoTheoremEvidence.{u,v} :
  forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), Prop where
| mk : forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), forall (quotient_group : @FirstIsoQuotientGroupEvidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args), forall (image_group : @FirstIsoImageGroupEvidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args), forall (mul_compat : forall (q1 : @KerQuot.{u,v} G H f), forall (q2 : @KerQuot.{u,v} G H f), @Eq.{succ v} H (@KerQuotToH.{u,v} G H f (@KerQuotMul.{u,v} G oneG mulG invG H oneH mulH invH f hom_args q1 q2)) (mulH (@KerQuotToH.{u,v} G H f q1) (@KerQuotToH.{u,v} G H f q2))), forall (injective : forall (q1 : @KerQuot.{u,v} G H f), forall (q2 : @KerQuot.{u,v} G H f), forall (h : @Eq.{succ v} H (@KerQuotToH.{u,v} G H f q1) (@KerQuotToH.{u,v} G H f q2)), @Eq.{succ u} (@KerQuot.{u,v} G H f) q1 q2), forall (hits_image : forall (q : @KerQuot.{u,v} G H f), @ImagePred.{succ u,succ v} G H f (@KerQuotToH.{u,v} G H f q)), forall (surj_image : forall (y : H), forall (hy : @ImagePred.{succ u,succ v} G H f y), forall (Q : Prop), forall (mk_surj : forall (q : @KerQuot.{u,v} G H f), forall (h : @Eq.{succ v} H (@KerQuotToH.{u,v} G H f q) y), Q), Q), @FirstIsoTheoremEvidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args

def FirstIsoImageGroupFacts.{u,v} :
  forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), Prop :=
  fun G => fun oneG => fun mulG => fun invG => fun H => fun oneH => fun mulH => fun invH => fun f => fun hom_args => forall (P : Prop), forall (mk : forall (one_member : @ImagePred.{succ u,succ v} G H f oneH), forall (mul_closed : forall (x : H), forall (y : H), forall (hx : @ImagePred.{succ u,succ v} G H f x), forall (hy : @ImagePred.{succ u,succ v} G H f y), @ImagePred.{succ u,succ v} G H f (mulH x y)), forall (inv_closed : forall (y : H), forall (hy : @ImagePred.{succ u,succ v} G H f y), @ImagePred.{succ u,succ v} G H f (invH y)), P), P

def FirstIsoImage.{u,v} :
  forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (group_args : @GroupLawArgs.{succ u} G oneG mulG invG), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), Prop :=
  fun G => fun oneG => fun mulG => fun invG => fun H => fun oneH => fun mulH => fun invH => fun f => fun group_args => fun hom_args => forall (P : Prop), forall (mk : forall (image_group : @FirstIsoImageGroupFacts.{u,v} G oneG mulG invG H oneH mulH invH f hom_args), forall (mul_compat : forall (q1 : @KerQuot.{u,v} G H f), forall (q2 : @KerQuot.{u,v} G H f), @Eq.{succ v} H (@KerQuotToH.{u,v} G H f (@KerQuotMul.{u,v} G oneG mulG invG H oneH mulH invH f hom_args q1 q2)) (mulH (@KerQuotToH.{u,v} G H f q1) (@KerQuotToH.{u,v} G H f q2))), forall (injective : forall (q1 : @KerQuot.{u,v} G H f), forall (q2 : @KerQuot.{u,v} G H f), forall (h : @Eq.{succ v} H (@KerQuotToH.{u,v} G H f q1) (@KerQuotToH.{u,v} G H f q2)), @Eq.{succ u} (@KerQuot.{u,v} G H f) q1 q2), forall (hits_image : forall (q : @KerQuot.{u,v} G H f), @ImagePred.{succ u,succ v} G H f (@KerQuotToH.{u,v} G H f q)), forall (surj_image : forall (y : H), forall (hy : @ImagePred.{succ u,succ v} G H f y), forall (Q : Prop), forall (mk_surj : forall (q : @KerQuot.{u,v} G H f), forall (h : @Eq.{succ v} H (@KerQuotToH.{u,v} G H f q) y), Q), Q), P), P

theorem first_iso_quotient_assoc_evidence.{u,v} :
  forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (group_args : @GroupLawArgs.{succ u} G oneG mulG invG), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), @FirstIsoQuotientAssocEvidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args :=
  fun G => fun oneG => fun mulG => fun invG => fun H => fun oneH => fun mulH => fun invH => fun f => fun group_args => fun hom_args => @FirstIsoQuotientAssocEvidence.mk.{u,v} G oneG mulG invG H oneH mulH invH f hom_args (@ker_quot_mul_assoc.{u,v} G oneG mulG invG H oneH mulH invH f group_args hom_args)

theorem first_iso_quotient_one_mul_evidence.{u,v} :
  forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (group_args : @GroupLawArgs.{succ u} G oneG mulG invG), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), @FirstIsoQuotientOneMulEvidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args :=
  fun G => fun oneG => fun mulG => fun invG => fun H => fun oneH => fun mulH => fun invH => fun f => fun group_args => fun hom_args => @FirstIsoQuotientOneMulEvidence.mk.{u,v} G oneG mulG invG H oneH mulH invH f hom_args (@ker_quot_one_mul.{u,v} G oneG mulG invG H oneH mulH invH f group_args hom_args)

theorem first_iso_quotient_mul_one_evidence.{u,v} :
  forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (group_args : @GroupLawArgs.{succ u} G oneG mulG invG), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), @FirstIsoQuotientMulOneEvidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args :=
  fun G => fun oneG => fun mulG => fun invG => fun H => fun oneH => fun mulH => fun invH => fun f => fun group_args => fun hom_args => @FirstIsoQuotientMulOneEvidence.mk.{u,v} G oneG mulG invG H oneH mulH invH f hom_args (@ker_quot_mul_one.{u,v} G oneG mulG invG H oneH mulH invH f group_args hom_args)

theorem first_iso_quotient_inv_mul_evidence.{u,v} :
  forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (group_args : @GroupLawArgs.{succ u} G oneG mulG invG), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), @FirstIsoQuotientInvMulEvidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args :=
  fun G => fun oneG => fun mulG => fun invG => fun H => fun oneH => fun mulH => fun invH => fun f => fun group_args => fun hom_args => @FirstIsoQuotientInvMulEvidence.mk.{u,v} G oneG mulG invG H oneH mulH invH f hom_args (@ker_quot_inv_mul.{u,v} G oneG mulG invG H oneH mulH invH f group_args hom_args)

theorem first_iso_quotient_mul_inv_evidence.{u,v} :
  forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (group_args : @GroupLawArgs.{succ u} G oneG mulG invG), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), @FirstIsoQuotientMulInvEvidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args :=
  fun G => fun oneG => fun mulG => fun invG => fun H => fun oneH => fun mulH => fun invH => fun f => fun group_args => fun hom_args => @FirstIsoQuotientMulInvEvidence.mk.{u,v} G oneG mulG invG H oneH mulH invH f hom_args (@ker_quot_mul_inv.{u,v} G oneG mulG invG H oneH mulH invH f group_args hom_args)

theorem first_iso_quotient_group_evidence.{u,v} :
  forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (group_args : @GroupLawArgs.{succ u} G oneG mulG invG), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), @FirstIsoQuotientGroupEvidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args :=
  fun G => fun oneG => fun mulG => fun invG => fun H => fun oneH => fun mulH => fun invH => fun f => fun group_args => fun hom_args => @FirstIsoQuotientGroupEvidence.mk.{u,v} G oneG mulG invG H oneH mulH invH f hom_args (@first_iso_quotient_assoc_evidence.{u,v} G oneG mulG invG H oneH mulH invH f group_args hom_args) (@first_iso_quotient_one_mul_evidence.{u,v} G oneG mulG invG H oneH mulH invH f group_args hom_args) (@first_iso_quotient_mul_one_evidence.{u,v} G oneG mulG invG H oneH mulH invH f group_args hom_args) (@first_iso_quotient_inv_mul_evidence.{u,v} G oneG mulG invG H oneH mulH invH f group_args hom_args) (@first_iso_quotient_mul_inv_evidence.{u,v} G oneG mulG invG H oneH mulH invH f group_args hom_args)

theorem first_iso_image_group_evidence.{u,v} :
  forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), @FirstIsoImageGroupEvidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args :=
  fun G => fun oneG => fun mulG => fun invG => fun H => fun oneH => fun mulH => fun invH => fun f => fun hom_args => @FirstIsoImageGroupEvidence.mk.{u,v} G oneG mulG invG H oneH mulH invH f hom_args (@image_one.{succ u,succ v} G oneG mulG invG H oneH mulH invH f hom_args) (@image_mul_closed.{succ u,succ v} G oneG mulG invG H oneH mulH invH f hom_args) (@image_inv_closed.{succ u,succ v} G oneG mulG invG H oneH mulH invH f hom_args)

theorem first_iso_image_group_facts.{u,v} :
  forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), forall (P : Prop), forall (mk : forall (one_member : @ImagePred.{succ u,succ v} G H f oneH), forall (mul_closed : forall (x : H), forall (y : H), forall (hx : @ImagePred.{succ u,succ v} G H f x), forall (hy : @ImagePred.{succ u,succ v} G H f y), @ImagePred.{succ u,succ v} G H f (mulH x y)), forall (inv_closed : forall (y : H), forall (hy : @ImagePred.{succ u,succ v} G H f y), @ImagePred.{succ u,succ v} G H f (invH y)), P), P :=
  fun G => fun oneG => fun mulG => fun invG => fun H => fun oneH => fun mulH => fun invH => fun f => fun hom_args => fun (P : Prop) => fun mk => mk (@image_one.{succ u,succ v} G oneG mulG invG H oneH mulH invH f hom_args) (@image_mul_closed.{succ u,succ v} G oneG mulG invG H oneH mulH invH f hom_args) (@image_inv_closed.{succ u,succ v} G oneG mulG invG H oneH mulH invH f hom_args)

theorem first_isomorphism_theorem_evidence.{u,v} :
  forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (group_args : @GroupLawArgs.{succ u} G oneG mulG invG), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), @FirstIsoTheoremEvidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args :=
  fun G => fun oneG => fun mulG => fun invG => fun H => fun oneH => fun mulH => fun invH => fun f => fun group_args => fun hom_args => @FirstIsoTheoremEvidence.mk.{u,v} G oneG mulG invG H oneH mulH invH f hom_args (@first_iso_quotient_group_evidence.{u,v} G oneG mulG invG H oneH mulH invH f group_args hom_args) (@first_iso_image_group_evidence.{u,v} G oneG mulG invG H oneH mulH invH f hom_args) (@first_iso_phi_mul.{u,v} G oneG mulG invG H oneH mulH invH f hom_args) (@first_iso_phi_injective.{u,v} G H f) (@first_iso_phi_hits_image.{u,v} G H f) (@first_iso_phi_surj_image.{u,v} G H f)

theorem first_isomorphism_to_image.{u,v} :
  forall (G : Sort succ u), forall (oneG : G), forall (mulG : forall (a : G), forall (b : G), G), forall (invG : forall (a : G), G), forall (H : Sort succ v), forall (oneH : H), forall (mulH : forall (a : H), forall (b : H), H), forall (invH : forall (a : H), H), forall (f : forall (x : G), H), forall (group_args : @GroupLawArgs.{succ u} G oneG mulG invG), forall (hom_args : @GroupHomLawArgs.{succ u,succ v} G oneG mulG invG H oneH mulH invH f), forall (P : Prop), forall (mk : forall (image_group : @FirstIsoImageGroupFacts.{u,v} G oneG mulG invG H oneH mulH invH f hom_args), forall (mul_compat : forall (q1 : @KerQuot.{u,v} G H f), forall (q2 : @KerQuot.{u,v} G H f), @Eq.{succ v} H (@KerQuotToH.{u,v} G H f (@KerQuotMul.{u,v} G oneG mulG invG H oneH mulH invH f hom_args q1 q2)) (mulH (@KerQuotToH.{u,v} G H f q1) (@KerQuotToH.{u,v} G H f q2))), forall (injective : forall (q1 : @KerQuot.{u,v} G H f), forall (q2 : @KerQuot.{u,v} G H f), forall (h : @Eq.{succ v} H (@KerQuotToH.{u,v} G H f q1) (@KerQuotToH.{u,v} G H f q2)), @Eq.{succ u} (@KerQuot.{u,v} G H f) q1 q2), forall (hits_image : forall (q : @KerQuot.{u,v} G H f), @ImagePred.{succ u,succ v} G H f (@KerQuotToH.{u,v} G H f q)), forall (surj_image : forall (y : H), forall (hy : @ImagePred.{succ u,succ v} G H f y), forall (Q : Prop), forall (mk_surj : forall (q : @KerQuot.{u,v} G H f), forall (h : @Eq.{succ v} H (@KerQuotToH.{u,v} G H f q) y), Q), Q), P), P :=
  fun G => fun oneG => fun mulG => fun invG => fun H => fun oneH => fun mulH => fun invH => fun f => fun group_args => fun hom_args => fun (P : Prop) => fun mk => mk (@first_iso_image_group_facts.{u,v} G oneG mulG invG H oneH mulH invH f hom_args) (@first_iso_phi_mul.{u,v} G oneG mulG invG H oneH mulH invH f hom_args) (@first_iso_phi_injective.{u,v} G H f) (@first_iso_phi_hits_image.{u,v} G H f) (@first_iso_phi_surj_image.{u,v} G H f)