awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (goal)
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'))
have simp : Eq.{u_2 + 1} (α := Subgroup ↥H') (map (MonoidHom.snd ↥G' ↥H') (P.prod Q).range) ⊤
Tactic: simp only [← MonoidHom.coe_snd, ← MonoidHom.coe_comp, ← MonoidHom.range_eq_top,
      MonoidHom.range_comp, Subgroup.range_subtype, I']
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (goal)
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'))
⊢ Eq.{u_2 + 1} (α := Subgroup ↥H') (map (MonoidHom.snd ↥G' ↥H') (P.prod Q).range) ⊤
have simp : Surjective (α := ↥I) (β := ↥H') (⇑(MonoidHom.comp (MonoidHom.snd ↥G' ↥H') (P.prod Q)) : (a : ↥I) → ↥H')
Tactic: simp only [← MonoidHom.range_comp, MonoidHom.range_eq_top]
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (hypothesis)
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'))
⊢ ∃ (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)
have hI₂' : 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
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (hypothesis)
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'))
⊢ ∃ (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)
have this : I'.goursatFst.Normal
Tactic: have := normal_goursatFst hI₁'
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (hypothesis)
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
⊢ ∃ (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)
have this₁ : I'.goursatSnd.Normal
Tactic: have := normal_goursatSnd hI₂'
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (goal)
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
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨e, he⟩ := goursat_surjective hI₁' hI₂'
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (goal)
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)
have 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)
Tactic: refine ⟨I.map (MonoidHom.fst ..), I.map (MonoidHom.snd ..),
    I'.goursatFst, I'.goursatSnd, inferInstance, inferInstance, e, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (goal)
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
⊢ 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)
have 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)))
Tactic: rw [← he]
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (goal)
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
⊢ 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)))
have simp : 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) ⧸ (P.prod Q).range.goursatFst)
        (↥(map (MonoidHom.snd G H) I) ⧸ (P.prod Q).range.goursatSnd))
      (MonoidHom.prodMap (QuotientGroup.mk' (P.prod Q).range.goursatFst)
        (QuotientGroup.mk' (P.prod Q).range.goursatSnd))
      (map
        (MonoidHom.prodMap (QuotientGroup.mk' (P.prod Q).range.goursatFst)
          (QuotientGroup.mk' (P.prod Q).range.goursatSnd))
        (P.prod Q).range))
Tactic: simp only [MonoidHom.range_comp, Subgroup.range_subtype, I']
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (goal)
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
⊢ 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) ⧸ (P.prod Q).range.goursatFst)
          (↥(map (MonoidHom.snd G H) I) ⧸ (P.prod Q).range.goursatSnd))
        (MonoidHom.prodMap (QuotientGroup.mk' (P.prod Q).range.goursatFst)
          (QuotientGroup.mk' (P.prod Q).range.goursatSnd))
        (map
          (MonoidHom.prodMap (QuotientGroup.mk' (P.prod Q).range.goursatFst)
            (QuotientGroup.mk' (P.prod Q).range.goursatSnd))
          (P.prod Q).range))
have rw : I =
  map (MonoidHom.prodMap (Subgroup.subtype (map (MonoidHom.fst G H) I)) (Subgroup.subtype (map (MonoidHom.snd G H) I)))
    (P.prod Q).range
Tactic: rw [comap_map_eq_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (goal)
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
      (MonoidHom.prodMap (Subgroup.subtype (map (MonoidHom.fst G H) I)) (Subgroup.subtype (map (MonoidHom.snd G H) I)))
      (P.prod Q).range
⊢ 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) ⧸ (P.prod Q).range.goursatFst)
          (↥(map (MonoidHom.snd G H) I) ⧸ (P.prod Q).range.goursatSnd))
        (MonoidHom.prodMap (QuotientGroup.mk' (P.prod Q).range.goursatFst)
          (QuotientGroup.mk' (P.prod Q).range.goursatSnd))
        (map
          (MonoidHom.prodMap (QuotientGroup.mk' (P.prod Q).range.goursatFst)
            (QuotientGroup.mk' (P.prod Q).range.goursatSnd))
          (P.prod Q).range))
have rw₁ : MonoidHom.ker
    (MonoidHom.prodMap (QuotientGroup.mk' (P.prod Q).range.goursatFst)
      (QuotientGroup.mk' (P.prod Q).range.goursatSnd)) ≤
  (P.prod Q).range
Tactic: rw [comap_map_eq_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (goal)
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
⊢ I =
    map
      (MonoidHom.prodMap (Subgroup.subtype (map (MonoidHom.fst G H) I)) (Subgroup.subtype (map (MonoidHom.snd G H) I)))
      (P.prod Q).range
have h : ∀ (g : G) (h : H),
  (g, h) ∈ I ↔
    Membership.mem (γ := Subgroup (G × H))
      (map
        (MonoidHom.prodMap (Subgroup.subtype (map (MonoidHom.fst G H) I))
          (Subgroup.subtype (map (MonoidHom.snd G H) I)))
        (P.prod Q).range)
      (g, h)
Tactic: ext ⟨g, h⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (goal)
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 : G
h : H
⊢ (g, h) ∈ I ↔
    Membership.mem (γ := Subgroup (G × H))
      (map
        (MonoidHom.prodMap (Subgroup.subtype (map (MonoidHom.fst G H) I))
          (Subgroup.subtype (map (MonoidHom.snd G H) I)))
        (P.prod Q).range)
      (g, h)
have h₁ : (g, h) ∈ I →
  Membership.mem (γ := Subgroup (G × H))
    (map
      (MonoidHom.prodMap (Subgroup.subtype (map (MonoidHom.fst G H) I)) (Subgroup.subtype (map (MonoidHom.snd G H) I)))
      (P.prod Q).range)
    (g, h)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (goal)
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 : G
h : H
h₁ :
  (g, h) ∈ I →
    Membership.mem (γ := Subgroup (G × H))
      (map
        (MonoidHom.prodMap (Subgroup.subtype (map (MonoidHom.fst G H) I))
          (Subgroup.subtype (map (MonoidHom.snd G H) I)))
        (P.prod Q).range)
      (g, h)
⊢ (g, h) ∈ I ↔
    Membership.mem (γ := Subgroup (G × H))
      (map
        (MonoidHom.prodMap (Subgroup.subtype (map (MonoidHom.fst G H) I))
          (Subgroup.subtype (map (MonoidHom.snd G H) I)))
        (P.prod Q).range)
      (g, h)
have h₂ : Membership.mem (γ := Subgroup (G × H))
    (map
      (MonoidHom.prodMap (Subgroup.subtype (map (MonoidHom.fst G H) I)) (Subgroup.subtype (map (MonoidHom.snd G H) I)))
      (P.prod Q).range)
    (g, h) →
  (g, h) ∈ I
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Goursat (goal)
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 : G
h : H
⊢ Membership.mem (γ := Subgroup (G × H))
      (map
        (MonoidHom.prodMap (Subgroup.subtype (map (MonoidHom.fst G H) I))
          (Subgroup.subtype (map (MonoidHom.snd G H) I)))
        (P.prod Q).range)
      (g, h) →
    (g, h) ∈ I
have h₁ : ∀ (x : H) (h_1 : (g, x) ∈ I) (x_1 : G) (h_2 : (x_1, h) ∈ I) (x_2 : G) (x_3 : H) (x_4 : (x_2, x_3) ∈ I),
  Eq.{u_1 + 1} (α := ↥(map (MonoidHom.fst G H) I))
      ((P : (a : ↥I) → ↥(map (MonoidHom.fst G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (x_2, x_3) sorry) :
        ↥(map (MonoidHom.fst G H) I))
      (Subtype.mk (p := fun (a : G) ↦ Membership.mem (γ := Subgroup G) (map (MonoidHom.fst G H) I) a) g sorry :
        ↥(map (MonoidHom.fst G H) I)) →
    Eq.{u_2 + 1} (α := ↥(map (MonoidHom.snd G H) I))
        ((Q : (a : ↥I) → ↥(map (MonoidHom.snd G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (x_2, x_3) sorry) :
          ↥(map (MonoidHom.snd G H) I))
        (Subtype.mk (p := fun (a : H) ↦ Membership.mem (γ := Subgroup H) (map (MonoidHom.snd G H) I) a) h sorry :
          ↥(map (MonoidHom.snd G H) I)) →
      (g, h) ∈ I
Tactic: simp 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, forall_exists_index, and_imp]