-- Mathlib/GroupTheory/Goursat.lean
/-- **Goursat's lemma** for a subgroup of a product with surjective projections.

If `I` is a subgroup of `G × H` which projects fully on both factors, then there exist normal
subgroups `M ≤ G` and `N ≤ H` such that `G' × H' ≤ I` and the image of `I` in `G ⧸ M × H ⧸ N` is the
graph of an isomorphism `G ⧸ M ≃ H ⧸ N'`.

`G'` and `H'` can be explicitly constructed as `I.goursatFst` and `I.goursatSnd` respectively. -/
@[to_additive
"**Goursat's lemma** for a subgroup of a product with surjective projections.

If `I` is a subgroup of `G × H` which projects fully on both factors, then there exist normal
subgroups `M ≤ G` and `N ≤ H` such that `G' × H' ≤ I` and the image of `I` in `G ⧸ M × H ⧸ N` is the
graph of an isomorphism `G ⧸ M ≃ H ⧸ N'`.

`G'` and `H'` can be explicitly constructed as `I.goursatFst` and `I.goursatSnd` respectively."]
lemma goursat_surjective :
    have := normal_goursatFst hI₁
    have := normal_goursatSnd hI₂
    ∃ e : G ⧸ I.goursatFst ≃* H ⧸ I.goursatSnd,
      (((QuotientGroup.mk' _).prodMap (QuotientGroup.mk' _)).comp I.subtype).range =
        e.toMonoidHom.graph

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
⊢ let_fun this := ⋯;
  let_fun this_1 := ⋯;
  ∃ e,
    (((QuotientGroup.mk' I.goursatFst).prodMap (QuotientGroup.mk' I.goursatSnd)).comp I.subtype).range =
      e.toMonoidHom.graph

Tactic:
have := normal_goursatFst hI₁

Result:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
this : I.goursatFst.Normal
⊢ let_fun this := ⋯;
  let_fun this_1 := ⋯;
  ∃ e,
    (((QuotientGroup.mk' I.goursatFst).prodMap (QuotientGroup.mk' I.goursatSnd)).comp I.subtype).range =
      e.toMonoidHom.graph

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
this✝ : I.goursatFst.Normal
this : I.goursatSnd.Normal
⊢ let_fun this := ⋯;
  let_fun this_1 := ⋯;
  ∃ e,
    (((QuotientGroup.mk' I.goursatFst).prodMap (QuotientGroup.mk' I.goursatSnd)).comp I.subtype).range =
      e.toMonoidHom.graph

Tactic:
exact (((QuotientGroup.mk' I.goursatFst).prodMap
  (QuotientGroup.mk' I.goursatSnd)).comp I.subtype).exists_mulEquiv_range_eq_graph
  ((QuotientGroup.mk'_surjective _).comp hI₁) ((QuotientGroup.mk'_surjective _).comp hI₂)
  fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ mk_goursatFst_eq_iff_mk_goursatSnd_eq hI₁ hI₂ hx hy

Result:
no goals

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
this : I.goursatFst.Normal
⊢ let_fun this := ⋯;
  let_fun this_1 := ⋯;
  ∃ e,
    (((QuotientGroup.mk' I.goursatFst).prodMap (QuotientGroup.mk' I.goursatSnd)).comp I.subtype).range =
      e.toMonoidHom.graph

Tactic:
have := normal_goursatSnd hI₂

Result:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
this✝ : I.goursatFst.Normal
this : I.goursatSnd.Normal
⊢ let_fun this := ⋯;
  let_fun this_1 := ⋯;
  ∃ e,
    (((QuotientGroup.mk' I.goursatFst).prodMap (QuotientGroup.mk' I.goursatSnd)).comp I.subtype).range =
      e.toMonoidHom.graph