-- Mathlib/GroupTheory/Goursat.lean
/-- **Goursat's lemma** for an arbitrary subgroup.

If `I` is a subgroup of `G × H`, then there exist subgroups `G' ≤ G`, `H' ≤ H` and normal subgroups
`M ⊴ G'` and `N ⊴ H'` such that `M × N ≤ I` and the image of `I` in `G' ⧸ M × H' ⧸ N` is the graph
of an isomorphism `G' ⧸ M ≃ H' ⧸ N`. -/
@[to_additive
"**Goursat's lemma** for an arbitrary subgroup.

If `I` is a subgroup of `G × H`, then there exist subgroups `G' ≤ G`, `H' ≤ H` and normal subgroups
`M ≤ G'` and `N ≤ H'` such that `M × N ≤ I` and the image of `I` in `G' ⧸ M × H' ⧸ N` is the graph
of an isomorphism `G ⧸ G' ≃ H ⧸ H'`."]
lemma goursat :
    ∃ (G' : Subgroup G) (H' : Subgroup H) (M : Subgroup G') (N : Subgroup H') (_ : M.Normal)
      (_ : N.Normal) (e : G' ⧸ M ≃* H' ⧸ N),
      I = (e.toMonoidHom.graph.comap <| (QuotientGroup.mk' M).prodMap (QuotientGroup.mk' N)).map
        (G'.subtype.prodMap H'.subtype)

Proof state:
case intro.h.mk.mpr
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
g : G
h h₁ : H
hgh₁ : (g, h₁) ∈ I
g₁ : G
hg₁h : (g₁, h) ∈ I
g₂ : G
h₂ : H
hg₂h₂ : (g₂, h₂) ∈ I
hP : ↑(P ⟨(g₂, h₂), ⋯⟩) = g
hQ : ↑(Q ⟨(g₂, h₂), ⋯⟩) = h
⊢ (g, h) ∈ I

Tactic:
rwa [← hP, ← hQ]

Result:
no goals

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
⊢ ∃ G' H' M N,
    ∃ (x : M.Normal) (x_1 : N.Normal),
      ∃ e,
        I =
          map (G'.subtype.prodMap H'.subtype)
            (comap ((QuotientGroup.mk' M).prodMap (QuotientGroup.mk' N)) e.toMonoidHom.graph)

Tactic:
let P : I →* G' := (MonoidHom.fst ..).subgroupMap I

Result:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
⊢ ∃ G' H' M N,
    ∃ (x : M.Normal) (x_1 : N.Normal),
      ∃ e,
        I =
          map (G'.subtype.prodMap H'.subtype)
            (comap ((QuotientGroup.mk' M).prodMap (QuotientGroup.mk' N)) e.toMonoidHom.graph)

Proof state:
case intro.h.mk.mp
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
g : G
h : H
hgh : (g, h) ∈ I
⊢ (g, h) ∈ map ((map (MonoidHom.fst G H) I).subtype.prodMap (map (MonoidHom.snd G H) I).subtype) (P.prod Q).range

Tactic:
simpa only [G', H', mem_map, MonoidHom.mem_range, MonoidHom.prod_apply, Subtype.exists,
  Prod.exists, MonoidHom.coe_prodMap, coe_subtype, Prod.mk.injEq, Prod.map_apply,
  MonoidHom.coe_snd, exists_eq_right, exists_and_right, exists_eq_right_right,
  MonoidHom.coe_fst]
  using ⟨⟨h, hgh⟩, ⟨g, hgh⟩, g, h, hgh, ⟨rfl, rfl⟩⟩

Result:
no goals

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
⊢ map (MonoidHom.fst ↥G' ↥H') (P.prod Q).range = ⊤

Tactic:
simp only [← MonoidHom.range_comp, MonoidHom.fst_comp_prod, MonoidHom.range_eq_top]

Result:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
⊢ Surjective ⇑P

Proof state:
case intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
⊢ ∃ G' H' M N,
    ∃ (x : M.Normal) (x_1 : N.Normal),
      ∃ e,
        I =
          map (G'.subtype.prodMap H'.subtype)
            (comap ((QuotientGroup.mk' M).prodMap (QuotientGroup.mk' N)) e.toMonoidHom.graph)

Tactic:
refine ⟨I.map (MonoidHom.fst ..), I.map (MonoidHom.snd ..),
  I'.goursatFst, I'.goursatSnd, inferInstance, inferInstance, e, ?_⟩

Result:
case intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
⊢ I =
    map ((map (MonoidHom.fst G H) I).subtype.prodMap (map (MonoidHom.snd G H) I).subtype)
      (comap ((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)) e.toMonoidHom.graph)