awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N_1 : Subgroup G
nN : N_1.Normal
H_1 : Type v
inst_1 : Group H_1
M : Type x
inst_2 : Monoid M
φ_1 : G →* H_1
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
this_1 : (N.subgroupOf H).Normal := ⋯
this : Normal (G := ↥(H ⊔ N)) (N.subgroupOf (H ⊔ N)) := ⋯
φ : ↥H →* HasQuotient.Quotient ↥(H ⊔ N) (B := Subgroup ↥(H ⊔ N)) (N.subgroupOf (H ⊔ N)) :=
  MonoidHom.comp (mk' (N.subgroupOf (H ⊔ N))) (inclusion ⋯)
x : HasQuotient.Quotient ↥(H ⊔ N) (B := Subgroup ↥(H ⊔ N)) (N.subgroupOf (H ⊔ N))
h : G
hh : h ∈ (↑H : Set G)
n : G
hy : (fun (x1 x2 : G) ↦ x1 * x2) h n ∈ H ⊔ N
hn : n ∈ N
h₁ :
  (leftRel (N.subgroupOf (H ⊔ N)) : ↥(H ⊔ N) → ↥(H ⊔ N) → Prop)
    ((inclusion ⋯ : (a : ↥H) → ↥(H ⊔ N)) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hh))
    (Subtype.mk (p := fun (x : G) ↦ x ∈ H ⊔ N) ((fun (x1 x2 : G) ↦ x1 * x2) h n) hy)
⊢ Eq (α := HasQuotient.Quotient ↥(H ⊔ N) (B := Subgroup ↥(H ⊔ N)) (N.subgroupOf (H ⊔ N)))
    ((φ : (a : ↥H) → ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hh) :
      HasQuotient.Quotient ↥(H ⊔ N) (B := Subgroup ↥(H ⊔ N)) (N.subgroupOf (H ⊔ N)))
    (Quotient.mk'' (Subtype.mk (p := fun (x : G) ↦ x ∈ H ⊔ N) ((fun (x1 x2 : G) ↦ x1 * x2) h n) hy) :
      Quotient (α := ↥(H ⊔ N)) (leftRel (N.subgroupOf (H ⊔ N))))

Tactic:
refine Quotient.eq.mpr ?_

Premises used: Iff.mpr, Quotient.eq
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N_1 : Subgroup G
nN : N_1.Normal
H_1 : Type v
inst_1 : Group H_1
M : Type x
inst_2 : Monoid M
φ_1 : G →* H_1
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
this_1 : (N.subgroupOf H).Normal := ⋯
this : Normal (G := ↥(H ⊔ N)) (N.subgroupOf (H ⊔ N)) := ⋯
φ : ↥H →* HasQuotient.Quotient ↥(H ⊔ N) (B := Subgroup ↥(H ⊔ N)) (N.subgroupOf (H ⊔ N)) :=
  MonoidHom.comp (mk' (N.subgroupOf (H ⊔ N))) (inclusion ⋯)
x : HasQuotient.Quotient ↥(H ⊔ N) (B := Subgroup ↥(H ⊔ N)) (N.subgroupOf (H ⊔ N))
h : G
hh : h ∈ (↑H : Set G)
n : G
hy : (fun (x1 x2 : G) ↦ x1 * x2) h n ∈ H ⊔ N
hn : n ∈ N
⊢ (leftRel (N.subgroupOf (H ⊔ N)) : ↥(H ⊔ N) → ↥(H ⊔ N) → Prop)
    ((inclusion ⋯ : (a : ↥H) → ↥(H ⊔ N)) (Subtype.mk (p := fun (x : G) ↦ x ∈ H) h hh))
    (Subtype.mk (p := fun (x : G) ↦ x ∈ H ⊔ N) ((fun (x1 x2 : G) ↦ x1 * x2) h n) hy)

Tactic:
simp [leftRel_apply, inclusion, mem_subgroupOf, hn]

Premises used: Subgroup.inclusion, Subgroup.mem_subgroupOf, QuotientGroup.leftRel_apply
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N_1 : Subgroup G
nN : N_1.Normal
H_1 : Type v
inst_1 : Group H_1
M : Type x
inst_2 : Monoid M
φ_1 : G →* H_1
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
this_1 : (N.subgroupOf H).Normal := ⋯
this : Normal (G := ↥(H ⊔ N)) (N.subgroupOf (H ⊔ N)) := ⋯
φ : ↥H →* HasQuotient.Quotient ↥(H ⊔ N) (B := Subgroup ↥(H ⊔ N)) (N.subgroupOf (H ⊔ N)) :=
  MonoidHom.comp (mk' (N.subgroupOf (H ⊔ N))) (inclusion ⋯)
φ_surjective :
  Surjective (α := ↥H) (β := HasQuotient.Quotient ↥(H ⊔ N) (B := Subgroup ↥(H ⊔ N)) (N.subgroupOf (H ⊔ N)))
    (⇑φ : (a : ↥H) → ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N))
⊢ N.subgroupOf H = φ.ker

Tactic:
simp [φ, ← comap_ker]

Premises used: MonoidHom.comap_ker
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst_1 : Group H
M_1 : Type x
inst_2 : Monoid M_1
φ : G →* H
M : Subgroup G
nM : M.Normal
⊢ Subgroup.Normal (Subgroup.map (mk' N) M)

Tactic:
nM.map _ mk_surjective

Premises used: Subgroup.Normal.map, QuotientGroup.mk_surjective
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst_1 : Group H
M_1 : Type x
inst_2 : Monoid M_1
φ : G →* H
M : Subgroup G
nM : M.Normal
h : N ≤ M
x : G
hx : x ∈ (↑M : Set G)
⊢ Eq (α := G ⧸ M) ((↑((MonoidHom.id G : (a : G) → G) x) : G ⧸ M) : G ⧸ M) (1 : G ⧸ M)

Tactic:
(QuotientGroup.eq_one_iff _).mpr hx

Premises used: Iff.mpr, QuotientGroup.eq_one_iff
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst_1 : Group H
M_1 : Type x
inst_2 : Monoid M_1
φ : G →* H
M : Subgroup G
nM : M.Normal
h : N ≤ M
x : G
hx : x ∈ (↑M : Set G)
⊢ Eq (α := G ⧸ M) ((↑((MonoidHom.id G : (a : G) → G) x) : G ⧸ M) : G ⧸ M) (1 : G ⧸ M)

Tactic:
exact (QuotientGroup.eq_one_iff _).mpr hx

Premises used: Iff.mpr, QuotientGroup.eq_one_iff
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
M : Subgroup G
nM : M.Normal
h : N ≤ M
x : G ⧸ N
⊢ Eq (α := G ⧸ M)
    ((quotientQuotientEquivQuotientAux N M h : (a : (G ⧸ N) ⧸ Subgroup.map (mk' N) M) → G ⧸ M)
        (↑x : (G ⧸ N) ⧸ Subgroup.map (mk' N) M) :
      G ⧸ M)
    ((map N M (MonoidHom.id G) h : (a : G ⧸ N) → G ⧸ M) x : G ⧸ M)

Tactic:
QuotientGroup.lift_mk' _ _ x

Premises used: QuotientGroup.lift_mk'
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
M : Subgroup G
nM : M.Normal
h : N ≤ M
x : G
⊢ Eq (α := G ⧸ M)
    ((quotientQuotientEquivQuotientAux N M h : (a : (G ⧸ N) ⧸ Subgroup.map (mk' N) M) → G ⧸ M)
        (↑(↑x : G ⧸ N) : (G ⧸ N) ⧸ Subgroup.map (mk' N) M) :
      G ⧸ M)
    ((↑x : G ⧸ M) : G ⧸ M)

Tactic:
QuotientGroup.lift_mk' (M.map (mk' N)) _ x

Premises used: Quotient.liftOn', Subgroup.map, QuotientGroup.mk, QuotientGroup.lift_mk', QuotientGroup.mk', Con.liftOn
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst_1 : Group H
M_1 : Type x
inst_2 : Monoid M_1
φ : G →* H
M : Subgroup G
nM : M.Normal
h : N ≤ M
h₁ :
  ∀ (x : G),
    Eq (α := HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M))
      ((MonoidHom.comp
              (MonoidHom.comp
                (MonoidHom.comp (map M (Subgroup.map (mk' N) M) (mk' N) ⋯) (quotientQuotientEquivQuotientAux N M h) :
                  HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M) →*
                    HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M))
                (mk' (Subgroup.map (mk' N) M) :
                  G ⧸ N →* HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M)))
              (mk' N) :
            (a : G) → (G ⧸ N) ⧸ Subgroup.map (mk' N) M)
          x :
        HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M))
      ((MonoidHom.comp
              (MonoidHom.comp
                (MonoidHom.id (HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M)))
                (mk' (Subgroup.map (mk' N) M)))
              (mk' N) :
            (a : G) → (G ⧸ N) ⧸ Subgroup.map (mk' N) M)
          x :
        HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M))
⊢ Eq (α :=
    HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M) →*
      HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M))
    (MonoidHom.comp (map M (Subgroup.map (mk' N) M) (mk' N) ⋯) (quotientQuotientEquivQuotientAux N M h) :
      HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M) →*
        HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M))
    (MonoidHom.id (HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M)) :
      HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M) →*
        HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M))

Tactic:
ext
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst_1 : Group H
M_1 : Type x
inst_2 : Monoid M_1
φ : G →* H
M : Subgroup G
nM : M.Normal
h : N ≤ M
x : G
⊢ Eq (α := HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M))
    ((MonoidHom.comp
            (MonoidHom.comp
              (MonoidHom.comp (map M (Subgroup.map (mk' N) M) (mk' N) ⋯) (quotientQuotientEquivQuotientAux N M h) :
                HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M) →*
                  HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M))
              (mk' (Subgroup.map (mk' N) M) :
                G ⧸ N →* HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M)))
            (mk' N) :
          (a : G) → (G ⧸ N) ⧸ Subgroup.map (mk' N) M)
        x :
      HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M))
    ((MonoidHom.comp
            (MonoidHom.comp
              (MonoidHom.id (HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M)))
              (mk' (Subgroup.map (mk' N) M)))
            (mk' N) :
          (a : G) → (G ⧸ N) ⧸ Subgroup.map (mk' N) M)
        x :
      HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M))

Tactic:
simp
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst_1 : Group H
M_1 : Type x
inst_2 : Monoid M_1
φ : G →* H
M : Subgroup G
nM : M.Normal
h : N ≤ M
h₁ :
  ∀ (x : G),
    Eq (α := G ⧸ M)
      ((MonoidHom.comp
              (MonoidHom.comp (N := HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M))
                (quotientQuotientEquivQuotientAux N M h) (map M (Subgroup.map (mk' N) M) (mk' N) ⋯))
              (mk' M) :
            (a : G) → G ⧸ M)
          x :
        G ⧸ M)
      ((MonoidHom.comp (MonoidHom.id (G ⧸ M)) (mk' M) : (a : G) → G ⧸ M) x : G ⧸ M)
⊢ Eq (α := G ⧸ M →* G ⧸ M)
    (MonoidHom.comp (N := HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M))
      (quotientQuotientEquivQuotientAux N M h) (map M (Subgroup.map (mk' N) M) (mk' N) ⋯))
    (MonoidHom.id (G ⧸ M))

Tactic:
ext
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
H : Type v
inst_1 : Group H
M_1 : Type x
inst_2 : Monoid M_1
φ : G →* H
M : Subgroup G
nM : M.Normal
h : N ≤ M
x : G
⊢ Eq (α := G ⧸ M)
    ((MonoidHom.comp
            (MonoidHom.comp (N := HasQuotient.Quotient (G ⧸ N) (B := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) M))
              (quotientQuotientEquivQuotientAux N M h) (map M (Subgroup.map (mk' N) M) (mk' N) ⋯))
            (mk' M) :
          (a : G) → G ⧸ M)
        x :
      G ⧸ M)
    ((MonoidHom.comp (MonoidHom.id (G ⧸ M)) (mk' M) : (a : G) → G ⧸ M) x : G ⧸ M)

Tactic:
simp
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
H : Subgroup (G ⧸ N)
⊢ N ≤ Subgroup.comap (mk' N) H

Tactic:
simpa using Subgroup.comap_mono (f := mk' N) bot_le

Premises used: Subgroup.comap_mono, bot_le
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N H : Subgroup G
inst_1 : N.Normal
⊢ Subgroup.comap (mk' N) (Subgroup.map (mk' N) H) = N ⊔ H

Tactic:
simp [Subgroup.comap_map_eq, sup_comm]

Premises used: Subgroup.comap_map_eq, sup_comm
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N_1 : Subgroup G
nN : N_1.Normal
H : Type v
inst_1 : Group H
M : Type x
inst_2 : Monoid M
φ : G →* H
N : Subgroup G
hn : N.Normal
H' : Subgroup (G ⧸ N)
⊢ H' ≤ range (mk' N)

Tactic:
simp
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N_1 : Subgroup G
nN : N_1.Normal
H_1 : Type v
inst_1 : Group H_1
M : Type x
inst_2 : Monoid M
φ : G →* H_1
N : Subgroup G
hn : N.Normal
x : { H : Subgroup G // N ≤ H }
H : Subgroup G
hH : N ≤ H
⊢ (↑((fun (H' : Subgroup (G ⧸ N)) ↦ Subtype.mk (p := fun (H : Subgroup G) ↦ N ≤ H) (Subgroup.comap (mk' N) H') ⋯)
          ((fun (H : { H : Subgroup G // N ≤ H }) ↦ (Subgroup.map (mk' N) (↑H : Subgroup G) : Subgroup (G ⧸ N)))
            (Subtype.mk (p := fun (H : Subgroup G) ↦ N ≤ H) H hH))) :
      Subgroup G) =
    (↑(Subtype.mk (p := fun (H : Subgroup G) ↦ N ≤ H) H hH) : Subgroup G)

Tactic:
simpa
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
⊢ Subsingleton.{u + 1} (HasQuotient.Quotient G (B := Subgroup G) ⊤)

Tactic:
simp
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
H : Subgroup G
h : Subsingleton.{u + 1} (G ⧸ H)
x : G
h_1 : Membership.mem (γ := Subgroup G) ⊤ x
⊢ 1⁻¹ * x ∈ H

Tactic:
have this : 1⁻¹ * x ∈ H := QuotientGroup.eq.1 (Subsingleton.elim _ _)
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
H : Subgroup G
h : Subsingleton.{u + 1} (G ⧸ H)
x : G
h_1 : Membership.mem (γ := Subgroup G) ⊤ x
this : 1⁻¹ * x ∈ H
rwa : ∀ (this : 1 * x ∈ H), x ∈ H
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : x ∈ H), x ∈ H
⊢ x ∈ H

Tactic:
rwa [inv_one, one_mul] at this

Premises used: inv_one, one_mul
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
H₁ : Subgroup G
inst_1 : H₁.Normal
H₂ : Subgroup (G ⧸ H₁)
inst_2 : H₂.Normal
h :
  ∀ (x : G),
    x ∈ Subgroup.comap (mk' H₁) (Subgroup.comap (mk' H₂) (Subgroup.center ((G ⧸ H₁) ⧸ H₂))) ↔
      x ∈ Subgroup.comap (mk' (Subgroup.comap (mk' H₁) H₂)) (Subgroup.center (G ⧸ Subgroup.comap (mk' H₁) H₂))
⊢ Subgroup.comap (mk' H₁) (Subgroup.comap (mk' H₂) (Subgroup.center ((G ⧸ H₁) ⧸ H₂))) =
    Subgroup.comap (mk' (Subgroup.comap (mk' H₁) H₂)) (Subgroup.center (G ⧸ Subgroup.comap (mk' H₁) H₂))

Tactic:
ext x
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
H₁ : Subgroup G
inst_1 : H₁.Normal
H₂ : Subgroup (G ⧸ H₁)
inst_2 : H₂.Normal
x : G
⊢ x ∈ Subgroup.comap (mk' H₁) (Subgroup.comap (mk' H₂) (Subgroup.center ((G ⧸ H₁) ⧸ H₂))) ↔
    x ∈ Subgroup.comap (mk' (Subgroup.comap (mk' H₁) H₂)) (Subgroup.center (G ⧸ Subgroup.comap (mk' H₁) H₂))

Tactic:
simp only [mk'_apply, Subgroup.mem_comap, Subgroup.mem_center_iff, forall_mk, ← mk_mul,
    eq_iff_div_mem, mk_div]

Premises used: Subgroup.mem_center_iff, QuotientGroup.mk'_apply, QuotientGroup.eq_iff_div_mem, Subgroup.mem_comap, QuotientGroup.mk_mul, QuotientGroup.mk_div, QuotientGroup.forall_mk
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
H : Subgroup G
hH : H.Characteristic
K : Subgroup (G ⧸ H)
hK : K.Characteristic
⊢ (comap (mk' H) K).Characteristic

Tactic:
characteristic_iff_comap_eq.mpr fun φ ↦ congr_arg (comap (mk' H))
    (characteristic_iff_comap_eq.mp hK (congr H H φ (characteristic_iff_map_eq.mp hH φ)))

Premises used: Iff.mpr, Subgroup.characteristic_iff_comap_eq, congr_arg, QuotientGroup.mk', QuotientGroup.congr, Iff.mp, Subgroup.characteristic_iff_map_eq, Subgroup.comap
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
H_1 : Type v
inst_1 : Group H_1
M : Type x
inst_2 : Monoid M
φ : G →* H_1
A : Type u_1
inst_3 : CommGroup A
H : Subgroup G
inst_4 : H.Normal
x : ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A))
f : G →* A
hf : Membership.mem (γ := Subgroup (G →* A)) (ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) f
⊢ H ≤ f.ker

Tactic:
simpa [mem_ker, restrictHom_apply, restrict_eq_one_iff] using hf

Premises used: MonoidHom.mem_ker, MonoidHom.restrict_eq_one_iff, MonoidHom.restrictHom_apply
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
H_1 : Type v
inst_1 : Group H_1
M : Type x
inst_2 : Monoid M
φ : G →* H_1
A : Type u_1
inst_3 : CommGroup A
H : Subgroup G
inst_4 : H.Normal
x : ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A))
⊢ (fun (f : MonoidHom.{u, u_1} (G ⧸ H) A) ↦
        (Subtype.mk (p := fun (x : G →* A) ↦
            Membership.mem (γ := Subgroup (G →* A)) (ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) x)
            (f.comp (mk' H)) ⋯ :
          ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A))))
      ((fun (x : ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A))) ↦
          (match (motive := ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) → MonoidHom.{u, u_1} (G ⧸ H) A)
              x with
            | ⟨f, hf⟩ => lift H f ⋯ :
            MonoidHom.{u, u_1} (G ⧸ H) A))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
H_1 : Type v
inst_1 : Group H_1
M : Type x
inst_2 : Monoid M
φ : G →* H_1
A : Type u_1
inst_3 : CommGroup A
H : Subgroup G
inst_4 : H.Normal
x : MonoidHom.{u, u_1} (G ⧸ H) A
h :
  ∀ (x_1 : G),
    Eq.{u_1 + 1} (α := A)
      ((MonoidHom.comp
              ((fun (x : ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A))) ↦
                  (match (motive :=
                      ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) → MonoidHom.{u, u_1} (G ⧸ H) A) x with
                    | ⟨f, hf⟩ => lift H f ⋯ :
                    MonoidHom.{u, u_1} (G ⧸ H) A))
                ((fun (f : MonoidHom.{u, u_1} (G ⧸ H) A) ↦
                    (Subtype.mk (p := fun (x : G →* A) ↦
                        Membership.mem (γ := Subgroup (G →* A)) (ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A))
                          x)
                        (f.comp (mk' H)) ⋯ :
                      ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A))))
                  x))
              (mk' H) :
            (a : G) → A)
          x_1 :
        A)
      ((x.comp (mk' H) : (a : G) → A) x_1 : A)
⊢ (fun (x : ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A))) ↦
        (match (motive := ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) → MonoidHom.{u, u_1} (G ⧸ H) A)
            x with
          | ⟨f, hf⟩ => lift H f ⋯ :
          MonoidHom.{u, u_1} (G ⧸ H) A))
      ((fun (f : MonoidHom.{u, u_1} (G ⧸ H) A) ↦
          (Subtype.mk (p := fun (x : G →* A) ↦
              Membership.mem (γ := Subgroup (G →* A)) (ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) x)
              (f.comp (mk' H)) ⋯ :
            ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A))))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
H_1 : Type v
inst_1 : Group H_1
M : Type x
inst_2 : Monoid M
φ : G →* H_1
A : Type u_1
inst_3 : CommGroup A
H : Subgroup G
inst_4 : H.Normal
x : MonoidHom.{u, u_1} (G ⧸ H) A
x_1 : G
⊢ Eq.{u_1 + 1} (α := A)
    ((MonoidHom.comp
            ((fun (x : ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A))) ↦
                (match (motive :=
                    ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) → MonoidHom.{u, u_1} (G ⧸ H) A) x with
                  | ⟨f, hf⟩ => lift H f ⋯ :
                  MonoidHom.{u, u_1} (G ⧸ H) A))
              ((fun (f : MonoidHom.{u, u_1} (G ⧸ H) A) ↦
                  (Subtype.mk (p := fun (x : G →* A) ↦
                      Membership.mem (γ := Subgroup (G →* A)) (ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A))
                        x)
                      (f.comp (mk' H)) ⋯ :
                    ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A))))
                x))
            (mk' H) :
          (a : G) → A)
        x_1 :
      A)
    ((x.comp (mk' H) : (a : G) → A) x_1 : A)

Tactic:
simp
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
H_1 : Type v
inst_1 : Group H_1
M : Type x
inst_2 : Monoid M
φ : G →* H_1
A : Type u_1
inst_3 : CommGroup A
H : Subgroup G
inst_4 : H.Normal
x x_1 : ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A))
h :
  ∀ (x_2 : G),
    Eq.{u_1 + 1} (α := A)
      ((MonoidHom.comp
              (match (motive :=
                ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) → MonoidHom.{u, u_1} (G ⧸ H) A) x * x_1 with
              | ⟨f, hf⟩ => lift H f ⋯)
              (mk' H) :
            (a : G) → A)
          x_2 :
        A)
      (((HMul.hMul (α := MonoidHom.{u, u_1} (G ⧸ H) A) (β := MonoidHom.{u, u_1} (G ⧸ H) A)
                  (match (motive :=
                      ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) → MonoidHom.{u, u_1} (G ⧸ H) A) x with
                    | ⟨f, hf⟩ => lift H f ⋯ :
                    MonoidHom.{u, u_1} (G ⧸ H) A)
                  (match (motive :=
                      ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) → MonoidHom.{u, u_1} (G ⧸ H) A) x_1 with
                    | ⟨f, hf⟩ => lift H f ⋯ :
                    MonoidHom.{u, u_1} (G ⧸ H) A)).comp
              (mk' H) :
            (a : G) → A)
          x_2 :
        A)
⊢ (match (motive := ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) → MonoidHom.{u, u_1} (G ⧸ H) A)
      x * x_1 with
    | ⟨f, hf⟩ => lift H f ⋯) =
    HMul.hMul (α := MonoidHom.{u, u_1} (G ⧸ H) A) (β := MonoidHom.{u, u_1} (G ⧸ H) A)
      (match (motive := ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) → MonoidHom.{u, u_1} (G ⧸ H) A) x with
        | ⟨f, hf⟩ => lift H f ⋯ :
        MonoidHom.{u, u_1} (G ⧸ H) A)
      (match (motive := ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) → MonoidHom.{u, u_1} (G ⧸ H) A)
          x_1 with
        | ⟨f, hf⟩ => lift H f ⋯ :
        MonoidHom.{u, u_1} (G ⧸ H) A)

Tactic:
ext
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
N : Subgroup G
nN : N.Normal
H_1 : Type v
inst_1 : Group H_1
M : Type x
inst_2 : Monoid M
φ : G →* H_1
A : Type u_1
inst_3 : CommGroup A
H : Subgroup G
inst_4 : H.Normal
x x_1 : ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A))
x_2 : G
⊢ Eq.{u_1 + 1} (α := A)
    ((MonoidHom.comp
            (match (motive := ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) → MonoidHom.{u, u_1} (G ⧸ H) A)
              x * x_1 with
            | ⟨f, hf⟩ => lift H f ⋯)
            (mk' H) :
          (a : G) → A)
        x_2 :
      A)
    (((HMul.hMul (α := MonoidHom.{u, u_1} (G ⧸ H) A) (β := MonoidHom.{u, u_1} (G ⧸ H) A)
                (match (motive :=
                    ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) → MonoidHom.{u, u_1} (G ⧸ H) A) x with
                  | ⟨f, hf⟩ => lift H f ⋯ :
                  MonoidHom.{u, u_1} (G ⧸ H) A)
                (match (motive :=
                    ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A)) → MonoidHom.{u, u_1} (G ⧸ H) A) x_1 with
                  | ⟨f, hf⟩ => lift H f ⋯ :
                  MonoidHom.{u, u_1} (G ⧸ H) A)).comp
            (mk' H) :
          (a : G) → A)
        x_2 :
      A)

Tactic:
simp
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
A : Type u_1
inst_1 : CommGroup A
H : Subgroup G
inst_2 : H.Normal
f : ↥(ker (M := MonoidHom.{u, u_1} (↥H) A) (restrictHom H A))
g : G
⊢ Eq.{u_1 + 1} (α := A)
    ((((restrictHomKerEquiv A H : (a : ↥(restrictHom H A).ker) → G ⧸ H →* A) f : MonoidHom.{u, u_1} (G ⧸ H) A) :
          (a : G ⧸ H) → A)
        (↑g : G ⧸ H) :
      A)
    (((↑f : G →* A) : (a : G) → A) g : A)

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
A : Type u_1
inst_1 : CommGroup A
H : Subgroup G
inst_2 : H.Normal
f : MonoidHom.{u, u_1} (G ⧸ H) A
g : G
⊢ Eq.{u_1 + 1} (α := A)
    (((↑((MulEquiv.symm (restrictHomKerEquiv A H) : (a : G ⧸ H →* A) → ↥(restrictHom H A).ker) f) : G →* A) :
          (a : G) → A)
        g :
      A)
    ((f : (a : G ⧸ H) → A) (↑g : G ⧸ H) : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
R : Type u_1
inst : NonAssocRing R
N : AddSubgroup R
inst_1 : N.Normal
n : ℕ
a : R
rw : (↑(n • a) : R ⧸ N) = HSMul.hSMul (β := R ⧸ N) n (↑a : R ⧸ N)
rw₁ rw₂ : HSMul.hSMul (β := R ⧸ N) n (↑a : R ⧸ N) = HSMul.hSMul (β := R ⧸ N) n (↑a : R ⧸ N)
⊢ (↑((↑n : R) * a) : R ⧸ N) = HSMul.hSMul (β := R ⧸ N) n (↑a : R ⧸ N)

Tactic:
rw [← nsmul_eq_mul, mk_nsmul N a n]

Premises used: QuotientAddGroup.mk_nsmul, nsmul_eq_mul