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)
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
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))
⊢ 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:
simp only [MonoidHom.range_comp, Subgroup.range_subtype, I']

Premises used: MonoidHom.range_comp, 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'))
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
rw₁ :
  MonoidHom.ker
      (MonoidHom.prodMap (QuotientGroup.mk' (P.prod Q).range.goursatFst)
        (QuotientGroup.mk' (P.prod Q).range.goursatSnd)) ≤
    (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))

Tactic:
rw [comap_map_eq_self]

Premises used: Subgroup.comap_map_eq_self
-- 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
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)
⊢ 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:
ext ⟨g, h⟩
-- 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 : 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)
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
⊢ (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
-- 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 : G
h : H
hgh : (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:
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⟩⟩

Premises used: exists_eq_right_right, MonoidHom.coe_snd, Subgroup.coe_subtype, Subtype.exists, exists_eq_right, MonoidHom.coe_prodMap, exists_and_right, MonoidHom.mem_range, MonoidHom.prod_apply, Prod.mk.injEq, Prod.map_apply, Subgroup.mem_map, MonoidHom.coe_fst, Prod.exists
-- 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 : G
h : H
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) ⋯) :
          ↥(map (MonoidHom.fst G H) I))
        (Subtype.mk (p := fun (a : G) ↦ Membership.mem (γ := Subgroup G) (map (MonoidHom.fst G H) I) a) g ⋯ :
          ↥(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) ⋯) :
            ↥(map (MonoidHom.snd G H) I))
          (Subtype.mk (p := fun (a : H) ↦ Membership.mem (γ := Subgroup H) (map (MonoidHom.snd G H) I) a) h ⋯ :
            ↥(map (MonoidHom.snd G H) I)) →
        (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

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]

Premises used: exists_eq_right_right, and_imp, MonoidHom.coe_snd, Subgroup.coe_subtype, Subtype.exists, forall_exists_index, exists_eq_right, MonoidHom.coe_prodMap, exists_and_right, MonoidHom.mem_range, MonoidHom.prod_apply, Prod.mk.injEq, Prod.map_apply, Subgroup.mem_map, MonoidHom.coe_fst, Prod.exists
-- 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 : 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 :
  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) (g₂, h₂) ⋯) :
      ↥(map (MonoidHom.fst G H) I))
    (Subtype.mk (p := fun (a : G) ↦ Membership.mem (γ := Subgroup G) (map (MonoidHom.fst G H) I) a) g ⋯ :
      ↥(map (MonoidHom.fst G H) I))
hQ :
  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) (g₂, h₂) ⋯) :
      ↥(map (MonoidHom.snd G H) I))
    (Subtype.mk (p := fun (a : H) ↦ Membership.mem (γ := Subgroup H) (map (MonoidHom.snd G H) I) a) h ⋯ :
      ↥(map (MonoidHom.snd G H) I))
⊢ (↑((P : (a : ↥I) → ↥(map (MonoidHom.fst G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (g₂, h₂) ⋯)) : G) = g

Tactic:
simp only [Subtype.ext_iff] at hP hQ

Premises used: Subtype.ext_iff
-- 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 : 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 :
  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) (g₂, h₂) ⋯) :
      ↥(map (MonoidHom.fst G H) I))
    (Subtype.mk (p := fun (a : G) ↦ Membership.mem (γ := Subgroup G) (map (MonoidHom.fst G H) I) a) g ⋯ :
      ↥(map (MonoidHom.fst G H) I))
hQ :
  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) (g₂, h₂) ⋯) :
      ↥(map (MonoidHom.snd G H) I))
    (Subtype.mk (p := fun (a : H) ↦ Membership.mem (γ := Subgroup H) (map (MonoidHom.snd G H) I) a) h ⋯ :
      ↥(map (MonoidHom.snd G H) I))
hP₁ : (↑((P : (a : ↥I) → ↥(map (MonoidHom.fst G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (g₂, h₂) ⋯)) : G) = g
⊢ (↑((Q : (a : ↥I) → ↥(map (MonoidHom.snd G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (g₂, h₂) ⋯)) : H) = h

Tactic:
simp only [Subtype.ext_iff] at hP hQ

Premises used: Subtype.ext_iff
-- 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 : 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 : (a : ↥I) → ↥(map (MonoidHom.fst G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (g₂, h₂) ⋯)) : G) = g
hQ : (↑((Q : (a : ↥I) → ↥(map (MonoidHom.snd G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (g₂, h₂) ⋯)) : H) = h
h₃ :
  ((↑((P : (a : ↥I) → ↥(map (MonoidHom.fst G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (g₂, h₂) ⋯)) : G), h) ∈ I
h₄ h₅ h₆ h₇ :
  ((↑((P : (a : ↥I) → ↥(map (MonoidHom.fst G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (g₂, h₂) ⋯)) : G),
      (↑((Q : (a : ↥I) → ↥(map (MonoidHom.snd G H) I)) (Subtype.mk (p := fun (a : G × H) ↦ a ∈ I) (g₂, h₂) ⋯)) : H)) ∈
    I
⊢ (g, h) ∈ I

Tactic:
rwa [← hP, ← hQ]
-- 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
⊢ (P.prod Q).range.goursatFst.prod (P.prod Q).range.goursatSnd ≤ (P.prod Q).range

Tactic:
goursatFst_prod_goursatSnd_le (P.prod Q).range

Premises used: MonoidHom.range, MonoidHom.prod, Subgroup.goursatFst_prod_goursatSnd_le
-- 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
h :
  MonoidHom.ker
      (MonoidHom.prodMap (QuotientGroup.mk' (P.prod Q).range.goursatFst)
        (QuotientGroup.mk' (P.prod Q).range.goursatSnd)) =
    (P.prod Q).range.goursatFst.prod (P.prod Q).range.goursatSnd
⊢ MonoidHom.ker
      (MonoidHom.prodMap (QuotientGroup.mk' (P.prod Q).range.goursatFst)
        (QuotientGroup.mk' (P.prod Q).range.goursatSnd)) ≤
    (P.prod Q).range

Tactic:
convert! goursatFst_prod_goursatSnd_le (P.prod Q).range

Premises used: MonoidHom.range, MonoidHom.prod, Subgroup.goursatFst_prod_goursatSnd_le
-- 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
h :
  ∀ (g : ↥(map (MonoidHom.fst G H) I)) (h : ↥(map (MonoidHom.snd G H) I)),
    (g, h) ∈
        MonoidHom.ker
          (MonoidHom.prodMap (QuotientGroup.mk' (P.prod Q).range.goursatFst)
            (QuotientGroup.mk' (P.prod Q).range.goursatSnd)) ↔
      (g, h) ∈ (P.prod Q).range.goursatFst.prod (P.prod Q).range.goursatSnd
⊢ MonoidHom.ker
      (MonoidHom.prodMap (QuotientGroup.mk' (P.prod Q).range.goursatFst)
        (QuotientGroup.mk' (P.prod Q).range.goursatSnd)) =
    (P.prod Q).range.goursatFst.prod (P.prod Q).range.goursatSnd

Tactic:
ext ⟨g, h⟩
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
M : Type u
inst : Monoid M
α : Type v
inst_1 : MulAction M α
β : Type u_1
inst_2 : MulAction M β
x y : α × β
h : x ∈ orbit M y
rcases : ∀ (g : M), ((fun (m : M) ↦ m • y) g).1 ∈ orbit M y.1
⊢ x.1 ∈ orbit M y.1

Tactic:
rcases h with ⟨g, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
M : Type u
inst : Monoid M
α : Type v
inst_1 : MulAction M α
β : Type u_1
inst_2 : MulAction M β
y : α × β
g : M
⊢ ((fun (m : M) ↦ m • y) g).1 ∈ orbit M y.1

Tactic:
mem_orbit _ _

Premises used: Set.Mem, MulAction.mem_orbit
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
M : Type u
inst : Monoid M
α : Type v
inst_1 : MulAction M α
β : Type u_1
inst_2 : MulAction M β
y : α × β
g : M
⊢ ((fun (m : M) ↦ m • y) g).1 ∈ orbit M y.1

Tactic:
exact mem_orbit _ _

Premises used: MulAction.mem_orbit
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
M : Type u
inst : Monoid M
α : Type v
inst_1 : MulAction M α
β : Type u_1
inst_2 : MulAction M β
x y : α × β
h : x ∈ orbit M y
rcases : ∀ (g : M), ((fun (m : M) ↦ m • y) g).2 ∈ orbit M y.2
⊢ x.2 ∈ orbit M y.2

Tactic:
rcases h with ⟨g, rfl⟩

Premises used: rfl
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
M : Type u
inst : Monoid M
α : Type v
inst_1 : MulAction M α
β : Type u_1
inst_2 : MulAction M β
y : α × β
g : M
⊢ ((fun (m : M) ↦ m • y) g).2 ∈ orbit M y.2

Tactic:
mem_orbit _ _

Premises used: Set.Mem, MulAction.mem_orbit
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
M : Type u
inst : Monoid M
α : Type v
inst_1 : MulAction M α
β : Type u_1
inst_2 : MulAction M β
y : α × β
g : M
⊢ ((fun (m : M) ↦ m • y) g).2 ∈ orbit M y.2

Tactic:
exact mem_orbit _ _

Premises used: MulAction.mem_orbit
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
M : Type u
inst : Monoid M
α : Type v
inst_1 : MulAction M α
inst_2 : Finite M
a : α
⊢ (orbit M a).Finite

Tactic:
Set.finite_range _

Premises used: Set.finite_range, MulAction.orbit
-- Module: Mathlib.GroupTheory.GroupAction.Basic
Goal:
M : Type u
inst : Monoid M
α : Type v
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
a : α
⊢ orbit M a = Set.univ

Tactic:
(surjective_smul M a).range_eq

Premises used: MulAction.surjective_smul, Function.Surjective.range_eq, MulAction.orbit