awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
hI₁ : Surjective (α := ↥I) (β := G) (comp (β := G × H) Prod.fst (⇑I.subtype : (a : ↥I) → G × H))
hI₂ : Surjective (α := ↥I) (β := H) (comp (β := G × H) Prod.snd (⇑I.subtype : (a : ↥I) → G × H))
x y : G × H
hx : x ∈ I
hy : y ∈ I
this : I.goursatFst.Normal
⊢ I.goursatSnd.Normal

Tactic:
have := normal_goursatSnd hI₂
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
hI₁ : Surjective (α := ↥I) (β := G) (comp (β := G × H) Prod.fst (⇑I.subtype : (a : ↥I) → G × H))
hI₂ : Surjective (α := ↥I) (β := H) (comp (β := G × H) Prod.snd (⇑I.subtype : (a : ↥I) → G × H))
x y : G × H
hx : x ∈ I
hy : y ∈ I
this_1 : I.goursatFst.Normal
this : I.goursatSnd.Normal
rw :
  Eq (α := G ⧸ I.goursatFst) (↑y.1 : G ⧸ I.goursatFst) (↑x.1 : G ⧸ I.goursatFst) ↔
    Eq (α := H ⧸ I.goursatSnd) (↑x.2 : H ⧸ I.goursatSnd) (↑y.2 : H ⧸ I.goursatSnd)
⊢ Eq (α := G ⧸ I.goursatFst) (↑x.1 : G ⧸ I.goursatFst) (↑y.1 : G ⧸ I.goursatFst) ↔
    Eq (α := H ⧸ I.goursatSnd) (↑x.2 : H ⧸ I.goursatSnd) (↑y.2 : H ⧸ I.goursatSnd)

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
hI₁ : Surjective (α := ↥I) (β := G) (comp (β := G × H) Prod.fst (⇑I.subtype : (a : ↥I) → G × H))
hI₂ : Surjective (α := ↥I) (β := H) (comp (β := G × H) Prod.snd (⇑I.subtype : (a : ↥I) → G × H))
x y : G × H
hx : x ∈ I
hy : y ∈ I
this_1 : I.goursatFst.Normal
this : I.goursatSnd.Normal
simp : (y.1 / x.1, 1) ∈ I ↔ (1, x.2 / y.2) ∈ I
⊢ Eq (α := G ⧸ I.goursatFst) (↑y.1 : G ⧸ I.goursatFst) (↑x.1 : G ⧸ I.goursatFst) ↔
    Eq (α := H ⧸ I.goursatSnd) (↑x.2 : H ⧸ I.goursatSnd) (↑y.2 : H ⧸ I.goursatSnd)

Tactic:
simp only [QuotientGroup.eq_iff_div_mem, mem_goursatFst, mem_goursatSnd]

Premises used: Subgroup.mem_goursatFst, QuotientGroup.eq_iff_div_mem, Subgroup.mem_goursatSnd
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
hI₁ : Surjective (α := ↥I) (β := G) (comp (β := G × H) Prod.fst (⇑I.subtype : (a : ↥I) → G × H))
hI₂ : Surjective (α := ↥I) (β := H) (comp (β := G × H) Prod.snd (⇑I.subtype : (a : ↥I) → G × H))
x y : G × H
hx : x ∈ I
hy : y ∈ I
this_1 : I.goursatFst.Normal
this : I.goursatSnd.Normal
mp : (y.1 / x.1, 1) ∈ I → (1, x.2 / y.2) ∈ I
mpr : (1, x.2 / y.2) ∈ I → (y.1 / x.1, 1) ∈ I
⊢ (y.1 / x.1, 1) ∈ I ↔ (1, x.2 / y.2) ∈ I

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
hI₁ : Surjective (α := ↥I) (β := G) (comp (β := G × H) Prod.fst (⇑I.subtype : (a : ↥I) → G × H))
hI₂ : Surjective (α := ↥I) (β := H) (comp (β := G × H) Prod.snd (⇑I.subtype : (a : ↥I) → G × H))
x y : G × H
hx : x ∈ I
hy : y ∈ I
this_1 : I.goursatFst.Normal
this : I.goursatSnd.Normal
h : (y.1 / x.1, 1) ∈ I
⊢ (1, x.2 / y.2) ∈ I

Tactic:
simpa [Prod.mul_def, Prod.div_def] using div_mem (mul_mem h hx) hy

Premises used: div_mem, Prod.mul_def, Prod.div_def, MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
hI₁ : Surjective (α := ↥I) (β := G) (comp (β := G × H) Prod.fst (⇑I.subtype : (a : ↥I) → G × H))
hI₂ : Surjective (α := ↥I) (β := H) (comp (β := G × H) Prod.snd (⇑I.subtype : (a : ↥I) → G × H))
x y : G × H
hx : x ∈ I
hy : y ∈ I
this_1 : I.goursatFst.Normal
this : I.goursatSnd.Normal
h : (1, x.2 / y.2) ∈ I
⊢ (y.1 / x.1, 1) ∈ I

Tactic:
simpa [Prod.mul_def, Prod.div_def] using div_mem (mul_mem h hy) hx

Premises used: div_mem, Prod.mul_def, Prod.div_def, MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
g : G
h : H
hg : (g, h).1 ∈ (↑I.goursatFst.toSubmonoid : Set G)
hh : (g, h).2 ∈ (↑I.goursatSnd.toSubmonoid : Set H)
⊢ (g, h) ∈ I

Tactic:
simpa using mul_mem (mem_goursatFst.1 hg) (mem_goursatSnd.1 hh)

Premises used: Subgroup.mem_goursatFst, Subgroup.mem_goursatSnd, Iff.mp, MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
hI₁ : Surjective (α := ↥I) (β := G) (comp (β := G × H) Prod.fst (⇑I.subtype : (a : ↥I) → G × H))
hI₂ : Surjective (α := ↥I) (β := H) (comp (β := G × H) Prod.snd (⇑I.subtype : (a : ↥I) → G × H))
⊢ I.goursatFst.Normal

Tactic:
have := normal_goursatFst hI₁
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
hI₁ : Surjective (α := ↥I) (β := G) (comp (β := G × H) Prod.fst (⇑I.subtype : (a : ↥I) → G × H))
hI₂ : Surjective (α := ↥I) (β := H) (comp (β := G × H) Prod.snd (⇑I.subtype : (a : ↥I) → G × H))
this : I.goursatFst.Normal
⊢ I.goursatSnd.Normal

Tactic:
have := normal_goursatSnd hI₂
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
hI₁ : Surjective (α := ↥I) (β := G) (comp (β := G × H) Prod.fst (⇑I.subtype : (a : ↥I) → G × H))
hI₂ : Surjective (α := ↥I) (β := H) (comp (β := G × H) Prod.snd (⇑I.subtype : (a : ↥I) → G × H))
this_1 : I.goursatFst.Normal
this : I.goursatSnd.Normal
⊢ have this := ⋯;
  have this_2 := ⋯;
  ∃ (e : MulEquiv.{u_1, u_2} (G ⧸ I.goursatFst) (H ⧸ I.goursatSnd)),
    ((MonoidHom.prodMap (QuotientGroup.mk' I.goursatFst) (QuotientGroup.mk' I.goursatSnd)).comp I.subtype).range =
      e.toMonoidHom.graph

Tactic:
(((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

Premises used: MonoidHom.prodMap, _private.0.Subgroup.goursat_surjective.match_1, Subgroup.subtype, Subgroup.mk_goursatFst_eq_iff_mk_goursatSnd_eq, MonoidHom.comp, Subgroup.goursatFst, Prod.fst, Subtype.mk, Iff, QuotientGroup.mk', Function.Surjective.comp, Subgroup.goursatSnd, QuotientGroup.mk'_surjective, Eq, Prod.snd, DFunLike.coe, MonoidHom.exists_mulEquiv_range_eq_graph
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
I : Subgroup (G × H)
hI₁ : Surjective (α := ↥I) (β := G) (comp (β := G × H) Prod.fst (⇑I.subtype : (a : ↥I) → G × H))
hI₂ : Surjective (α := ↥I) (β := H) (comp (β := G × H) Prod.snd (⇑I.subtype : (a : ↥I) → G × H))
this_1 : I.goursatFst.Normal
this : I.goursatSnd.Normal
⊢ have this := ⋯;
  have this_2 := ⋯;
  ∃ (e : MulEquiv.{u_1, u_2} (G ⧸ I.goursatFst) (H ⧸ I.goursatSnd)),
    ((MonoidHom.prodMap (QuotientGroup.mk' I.goursatFst) (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

Premises used: MonoidHom.prodMap, _private.0.Subgroup.goursat_surjective.match_1, Subgroup.subtype, Subgroup.mk_goursatFst_eq_iff_mk_goursatSnd_eq, MonoidHom.comp, Subgroup.goursatFst, Prod.fst, Subtype.mk, Iff, QuotientGroup.mk', Function.Surjective.comp, Subgroup.goursatSnd, QuotientGroup.mk'_surjective, Eq, Prod.snd, DFunLike.coe, MonoidHom.exists_mulEquiv_range_eq_graph
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : 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.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
simp : Eq.{u_1 + 1} (α := Subgroup ↥G') (map (MonoidHom.fst ↥G' ↥H') (P.prod Q).range) ⊤
⊢ Surjective (α := ↥I') (β := ↥G') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.fst (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))

Tactic:
simp only [← MonoidHom.coe_fst, ← MonoidHom.coe_comp, ← MonoidHom.range_eq_top,
      MonoidHom.range_comp, Subgroup.range_subtype, I']

Premises used: MonoidHom.coe_comp, MonoidHom.range_comp, MonoidHom.range_eq_top, MonoidHom.coe_fst, Subgroup.range_subtype
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : 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.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
simp : Surjective (α := ↥I) (β := ↥G') (⇑P : (a : ↥I) → ↥G')
⊢ Eq.{u_1 + 1} (α := Subgroup ↥G') (map (MonoidHom.fst ↥G' ↥H') (P.prod Q).range) ⊤

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

Premises used: MonoidHom.range_comp, MonoidHom.range_eq_top, MonoidHom.fst_comp_prod
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : 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.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
⊢ Surjective (α := ↥I) (β := ↥G') (⇑P : (a : ↥I) → ↥G')

Tactic:
(MonoidHom.fst ..).subgroupMap_surjective I

Premises used: Set.Mem, MonoidHom.subgroupMap_surjective
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : 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.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
⊢ Surjective (α := ↥I) (β := ↥G') (⇑P : (a : ↥I) → ↥G')

Tactic:
exact (MonoidHom.fst ..).subgroupMap_surjective I

Premises used: MonoidHom.subgroupMap_surjective
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : 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.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
⊢ Surjective (α := ↥I') (β := ↥G') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.fst (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))

Tactic:
have hI₁' : Surjective (Prod.fst ∘ I'.subtype) := by
    simp only [← MonoidHom.coe_fst, ← MonoidHom.coe_comp, ← MonoidHom.range_eq_top,
      MonoidHom.range_comp, Subgroup.range_subtype, I']
    simp only [← MonoidHom.range_comp, MonoidHom.fst_comp_prod, MonoidHom.range_eq_top]
    exact (MonoidHom.fst ..).subgroupMap_surjective I
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : 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.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
hI₁' :
  Surjective (α := ↥I') (β := ↥G') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.fst (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
simp : Eq.{u_2 + 1} (α := Subgroup ↥H') (map (MonoidHom.snd ↥G' ↥H') (P.prod Q).range) ⊤
⊢ Surjective (α := ↥I') (β := ↥H') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.snd (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))

Tactic:
simp only [← MonoidHom.coe_snd, ← MonoidHom.coe_comp, ← MonoidHom.range_eq_top,
      MonoidHom.range_comp, Subgroup.range_subtype, I']

Premises used: MonoidHom.coe_comp, MonoidHom.coe_snd, MonoidHom.range_comp, MonoidHom.range_eq_top, Subgroup.range_subtype
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : 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.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
hI₁' :
  Surjective (α := ↥I') (β := ↥G') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.fst (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
simp : Surjective (α := ↥I) (β := ↥H') (⇑(MonoidHom.comp (MonoidHom.snd ↥G' ↥H') (P.prod Q)) : (a : ↥I) → ↥H')
⊢ Eq.{u_2 + 1} (α := Subgroup ↥H') (map (MonoidHom.snd ↥G' ↥H') (P.prod Q).range) ⊤

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

Premises used: MonoidHom.range_comp, MonoidHom.range_eq_top
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : 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.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
hI₁' :
  Surjective (α := ↥I') (β := ↥G') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.fst (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
⊢ Surjective (α := ↥I) (β := ↥H') (⇑(MonoidHom.comp (MonoidHom.snd ↥G' ↥H') (P.prod Q)) : (a : ↥I) → ↥H')

Tactic:
(MonoidHom.snd ..).subgroupMap_surjective I

Premises used: Set.Mem, MonoidHom.subgroupMap_surjective
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : 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.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
hI₁' :
  Surjective (α := ↥I') (β := ↥G') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.fst (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
⊢ Surjective (α := ↥I) (β := ↥H') (⇑(MonoidHom.comp (MonoidHom.snd ↥G' ↥H') (P.prod Q)) : (a : ↥I) → ↥H')

Tactic:
exact (MonoidHom.snd ..).subgroupMap_surjective I

Premises used: MonoidHom.subgroupMap_surjective
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : 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.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
hI₁' :
  Surjective (α := ↥I') (β := ↥G') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.fst (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
⊢ Surjective (α := ↥I') (β := ↥H') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.snd (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))

Tactic:
have hI₂' : Surjective (Prod.snd ∘ I'.subtype) := by
    simp only [← MonoidHom.coe_snd, ← MonoidHom.coe_comp, ← MonoidHom.range_eq_top,
      MonoidHom.range_comp, Subgroup.range_subtype, I']
    simp only [← MonoidHom.range_comp, MonoidHom.range_eq_top]
    exact (MonoidHom.snd ..).subgroupMap_surjective I
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : 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.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
hI₁' :
  Surjective (α := ↥I') (β := ↥G') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.fst (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
hI₂' :
  Surjective (α := ↥I') (β := ↥H') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.snd (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
⊢ I'.goursatFst.Normal

Tactic:
have := normal_goursatFst hI₁'
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : 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.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
hI₁' :
  Surjective (α := ↥I') (β := ↥G') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.fst (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
hI₂' :
  Surjective (α := ↥I') (β := ↥H') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.snd (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
this : I'.goursatFst.Normal
⊢ I'.goursatSnd.Normal

Tactic:
have := normal_goursatSnd hI₂'
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : 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.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
hI₁' :
  Surjective (α := ↥I') (β := ↥G') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.fst (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
hI₂' :
  Surjective (α := ↥I') (β := ↥H') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.snd (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
this_1 : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
obtain :
  ∀ (e : MulEquiv.{u_1, u_2} (↥G' ⧸ I'.goursatFst) (↥H' ⧸ I'.goursatSnd))
    (he :
      MonoidHom.range
          (MonoidHom.comp (MonoidHom.prodMap (QuotientGroup.mk' I'.goursatFst) (QuotientGroup.mk' I'.goursatSnd))
            I'.subtype) =
        e.toMonoidHom.graph),
    ∃ (G' : Subgroup G) (H' : Subgroup H) (M : Subgroup ↥G') (N : Subgroup ↥H') (x : M.Normal) (x_1 : N.Normal) (e :
      MulEquiv.{u_1, u_2} (↥G' ⧸ M) (↥H' ⧸ N)),
      I =
        map (G'.subtype.prodMap H'.subtype)
          (comap (MonoidHom.prodMap (QuotientGroup.mk' M) (QuotientGroup.mk' N)) e.toMonoidHom.graph)
⊢ ∃ (G' : Subgroup G) (H' : Subgroup H) (M : Subgroup ↥G') (N : Subgroup ↥H') (x : M.Normal) (x_1 : N.Normal) (e :
    MulEquiv.{u_1, u_2} (↥G' ⧸ M) (↥H' ⧸ N)),
    I =
      map (G'.subtype.prodMap H'.subtype)
        (comap (MonoidHom.prodMap (QuotientGroup.mk' M) (QuotientGroup.mk' N)) e.toMonoidHom.graph)

Tactic:
obtain ⟨e, he⟩ := goursat_surjective hI₁' hI₂'

Premises used: Subgroup.goursat_surjective
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : 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.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
hI₁' :
  Surjective (α := ↥I') (β := ↥G') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.fst (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
hI₂' :
  Surjective (α := ↥I') (β := ↥H') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.snd (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
this_1 : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : MulEquiv.{u_1, u_2} (↥G' ⧸ I'.goursatFst) (↥H' ⧸ I'.goursatSnd)
he :
  MonoidHom.range
      (MonoidHom.comp (MonoidHom.prodMap (QuotientGroup.mk' I'.goursatFst) (QuotientGroup.mk' I'.goursatSnd))
        I'.subtype) =
    e.toMonoidHom.graph
⊢ ∃ (G' : Subgroup G) (H' : Subgroup H) (M : Subgroup ↥G') (N : Subgroup ↥H') (x : M.Normal) (x_1 : N.Normal) (e :
    MulEquiv.{u_1, u_2} (↥G' ⧸ M) (↥H' ⧸ N)),
    I =
      map (G'.subtype.prodMap H'.subtype)
        (comap (MonoidHom.prodMap (QuotientGroup.mk' M) (QuotientGroup.mk' N)) e.toMonoidHom.graph)

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

Premises used: Subgroup.map, inferInstance, Exists.intro
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : 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.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
hI₁' :
  Surjective (α := ↥I') (β := ↥G') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.fst (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
hI₂' :
  Surjective (α := ↥I') (β := ↥H') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.snd (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
this_1 : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : MulEquiv.{u_1, u_2} (↥G' ⧸ I'.goursatFst) (↥H' ⧸ I'.goursatSnd)
he :
  MonoidHom.range
      (MonoidHom.comp (MonoidHom.prodMap (QuotientGroup.mk' I'.goursatFst) (QuotientGroup.mk' I'.goursatSnd))
        I'.subtype) =
    e.toMonoidHom.graph
refine :
  I =
    map (G := Prod.{u_1, u_2} ↥(map (MonoidHom.fst G H) I) ↥(map (MonoidHom.snd G H) I))
      (MonoidHom.prodMap (Subgroup.subtype (map (MonoidHom.fst G H) I)) (Subgroup.subtype (map (MonoidHom.snd G H) I)))
      (comap (MonoidHom.prodMap (QuotientGroup.mk' I'.goursatFst) (QuotientGroup.mk' I'.goursatSnd))
        e.toMonoidHom.graph)
⊢ ∃ (G' : Subgroup G) (H' : Subgroup H) (M : Subgroup ↥G') (N : Subgroup ↥H') (x : M.Normal) (x_1 : N.Normal) (e :
    MulEquiv.{u_1, u_2} (↥G' ⧸ M) (↥H' ⧸ N)),
    I =
      map (G'.subtype.prodMap H'.subtype)
        (comap (MonoidHom.prodMap (QuotientGroup.mk' M) (QuotientGroup.mk' N)) e.toMonoidHom.graph)

Tactic:
refine ⟨I.map (MonoidHom.fst ..), I.map (MonoidHom.snd ..),
    I'.goursatFst, I'.goursatSnd, inferInstance, inferInstance, e, ?_⟩
-- Module: Mathlib.GroupTheory.Goursat
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : 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.subgroupMap (MonoidHom.fst G H) I
Q : ↥I →* ↥H' := MonoidHom.subgroupMap (MonoidHom.snd G H) I
I' : Subgroup (Prod.{u_1, u_2} ↥G' ↥H') := (P.prod Q).range
hI₁' :
  Surjective (α := ↥I') (β := ↥G') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.fst (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
hI₂' :
  Surjective (α := ↥I') (β := ↥H') (comp (β := Prod.{u_1, u_2} ↥G' ↥H') Prod.snd (⇑I'.subtype : (a : ↥I') → ↥G' × ↥H'))
this_1 : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : MulEquiv.{u_1, u_2} (↥G' ⧸ I'.goursatFst) (↥H' ⧸ I'.goursatSnd)
he :
  MonoidHom.range
      (MonoidHom.comp (MonoidHom.prodMap (QuotientGroup.mk' I'.goursatFst) (QuotientGroup.mk' I'.goursatSnd))
        I'.subtype) =
    e.toMonoidHom.graph
rw :
  I =
    map (G := Prod.{u_1, u_2} ↥(map (MonoidHom.fst G H) I) ↥(map (MonoidHom.snd G H) I))
      (MonoidHom.prodMap (Subgroup.subtype (map (MonoidHom.fst G H) I)) (Subgroup.subtype (map (MonoidHom.snd G H) I)))
      (comap (N :=
        Prod.{u_1, u_2} (↥(map (MonoidHom.fst G H) I) ⧸ I'.goursatFst) (↥(map (MonoidHom.snd G H) I) ⧸ I'.goursatSnd))
        (MonoidHom.prodMap (QuotientGroup.mk' I'.goursatFst) (QuotientGroup.mk' I'.goursatSnd))
        (MonoidHom.range
          (MonoidHom.comp (MonoidHom.prodMap (QuotientGroup.mk' I'.goursatFst) (QuotientGroup.mk' I'.goursatSnd))
            I'.subtype)))
⊢ I =
    map (G := Prod.{u_1, u_2} ↥(map (MonoidHom.fst G H) I) ↥(map (MonoidHom.snd G H) I))
      (MonoidHom.prodMap (Subgroup.subtype (map (MonoidHom.fst G H) I)) (Subgroup.subtype (map (MonoidHom.snd G H) I)))
      (comap (MonoidHom.prodMap (QuotientGroup.mk' I'.goursatFst) (QuotientGroup.mk' I'.goursatSnd))
        e.toMonoidHom.graph)

Tactic:
rw [← he]