awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M_1 : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M_1
N : Subgroup G
nN : N.Normal
M : Subgroup H
inst_3 : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
refine : N ≤ MonoidHom.ker (MonoidHom.comp (mk' M) f)
⊢ MonoidHom.{u_1, u_2} (G ⧸ N) (H ⧸ M)

Tactic:
refine QuotientGroup.lift N ((mk' M).comp f) ?_

Premises used: QuotientGroup.lift, MonoidHom.comp, QuotientGroup.mk'
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M_1 : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M_1
N : Subgroup G
nN : N.Normal
M : Subgroup H
inst_3 : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
x : G
hx : x ∈ N
⊢ x ∈ MonoidHom.ker (MonoidHom.comp (mk' M) f)

Tactic:
QuotientGroup.eq.2 ?_

Premises used: Iff.mpr, Set.Mem, setOf, QuotientGroup.eq, MulAction.orbitRel, Set.preimage, Set.singleton
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M_1 : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M_1
N : Subgroup G
nN : N.Normal
M : Subgroup H
inst_3 : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
x : G
hx : x ∈ N
refine : HMul.hMul (α := H) (β := H) (((f : (a : G) → H) x)⁻¹ : H) (1 : H) ∈ M
⊢ x ∈ MonoidHom.ker (MonoidHom.comp (mk' M) f)

Tactic:
refine QuotientGroup.eq.2 ?_

Premises used: Iff.mpr, QuotientGroup.eq
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M_1 : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M_1
N : Subgroup G
nN : N.Normal
M : Subgroup H
inst_3 : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
x : G
hx : x ∈ N
rw : Membership.mem (α := H) M ((f : (a : G) → H) x : H)
⊢ HMul.hMul (α := H) (β := H) (((f : (a : G) → H) x)⁻¹ : H) (1 : H) ∈ M

Tactic:
rw [mul_one, Subgroup.inv_mem_iff]

Premises used: Subgroup.inv_mem_iff, mul_one
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M_1 : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M_1
N : Subgroup G
nN : N.Normal
M : Subgroup H
inst_3 : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
x : G
hx : x ∈ N
⊢ Membership.mem (α := H) M ((f : (a : G) → H) x : H)

Tactic:
h hx

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M_1 : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M_1
N : Subgroup G
nN : N.Normal
M : Subgroup H
inst_3 : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
x : G
hx : x ∈ N
⊢ Membership.mem (α := H) M ((f : (a : G) → H) x : H)

Tactic:
exact h hx
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
N : Subgroup G
nN : N.Normal
M : Subgroup H
inst_2 : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
x : G
⊢ Eq.{u_2 + 1} (α := H ⧸ M)
    (((map N M f h : MonoidHom.{u_1, u_2} (G ⧸ N) (H ⧸ M)) : (a : G ⧸ N) → H ⧸ M) (↑x : G ⧸ N) : H ⧸ M)
    ((↑((f : (a : G) → H) x) : H ⧸ M) : H ⧸ M)

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
N : Subgroup G
nN : N.Normal
M : Subgroup H
inst_2 : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
x : G
⊢ Eq.{u_2 + 1} (α := H ⧸ M)
    (((map N M f h : MonoidHom.{u_1, u_2} (G ⧸ N) (H ⧸ M)) : (a : G ⧸ N) → H ⧸ M) ((mk' N : (a : G) → G ⧸ N) x) : H ⧸ M)
    ((↑((f : (a : G) → H) x) : H ⧸ M) : H ⧸ M)

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
N : Subgroup G
nN : N.Normal
M : Subgroup H
inst_2 : M.Normal
f : G →* H
hf : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H ⧸ M) (mk ∘ (⇑f : (a : G) → H))
h : N ≤ Subgroup.comap f M
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := G ⧸ N) (β := H ⧸ M) (⇑(map N M f h) : (a : G ⧸ N) → H ⧸ M)

Tactic:
lift_surjective_of_surjective _ _ hf _

Premises used: QuotientGroup.lift_surjective_of_surjective
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
N : Subgroup G
nN : N.Normal
M : Subgroup H
inst_2 : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
simp_rw :
  Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (map N M f h))
    (Subgroup.map (mk' N) (MonoidHom.ker (MonoidHom.comp (mk' M) f)))
⊢ Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (map N M f h)) (Subgroup.map (mk' N) (Subgroup.comap f M))

Tactic:
simp_rw [← ker_mk' M, MonoidHom.comap_ker]

Premises used: QuotientGroup.ker_mk', MonoidHom.comap_ker
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
N : Subgroup G
nN : N.Normal
M : Subgroup H
inst_2 : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
⊢ Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (map N M f h))
    (Subgroup.map (mk' N) (MonoidHom.ker (MonoidHom.comp (mk' M) f)))

Tactic:
QuotientGroup.ker_lift _ _ _

Premises used: QuotientGroup.map, QuotientGroup.ker_lift
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
N : Subgroup G
nN : N.Normal
M : Subgroup H
inst_2 : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
⊢ Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (map N M f h))
    (Subgroup.map (mk' N) (MonoidHom.ker (MonoidHom.comp (mk' M) f)))

Tactic:
exact QuotientGroup.ker_lift _ _ _

Premises used: QuotientGroup.ker_lift
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
h : N ≤ Subgroup.comap (MonoidHom.id G) N
x : G ⧸ N
⊢ (map N N (MonoidHom.id G) h : (a : G ⧸ N) → G ⧸ N) x = x

Tactic:
induction_on x fun _x => rfl

Premises used: QuotientGroup.induction_on
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
h : N ≤ Subgroup.comap (MonoidHom.id G) N
⊢ Eq (α := G ⧸ N →* G ⧸ N) (map N N (MonoidHom.id G) h) (MonoidHom.id (G ⧸ N))

Tactic:
MonoidHom.ext (map_id_apply N h)

Premises used: MonoidHom.ext, QuotientGroup.map_id_apply
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
N : Subgroup G
nN : N.Normal
I : Type u_5
inst_2 : Group I
M : Subgroup H
O : Subgroup I
inst_3 : M.Normal
inst_4 : O.Normal
f : G →* H
g : H →* I
hf : N ≤ Subgroup.comap f M
hg : M ≤ Subgroup.comap g O
hgf : N ≤ Subgroup.comap (g.comp f) O
x : G ⧸ N
⊢ Eq.{u_5 + 1} (α := I ⧸ O)
    (((map M O g hg : MonoidHom.{u_2, u_5} (H ⧸ M) (I ⧸ O)) : (a : H ⧸ M) → I ⧸ O)
        (((map N M f hf : MonoidHom.{u_1, u_2} (G ⧸ N) (H ⧸ M)) : (a : G ⧸ N) → H ⧸ M) x) :
      I ⧸ O)
    (((map N O (g.comp f) hgf : MonoidHom.{u_1, u_5} (G ⧸ N) (I ⧸ O)) : (a : G ⧸ N) → I ⧸ O) x : I ⧸ O)

Tactic:
induction_on x fun x => ?_

Premises used: QuotientGroup.induction_on
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
N : Subgroup G
nN : N.Normal
I : Type u_5
inst_2 : Group I
M : Subgroup H
O : Subgroup I
inst_3 : M.Normal
inst_4 : O.Normal
f : G →* H
g : H →* I
hf : N ≤ Subgroup.comap f M
hg : M ≤ Subgroup.comap g O
hgf : N ≤ Subgroup.comap (g.comp f) O
x : G ⧸ N
refine :
  ∀ (x : G),
    Eq.{u_5 + 1} (α := I ⧸ O)
      (((map M O g hg : MonoidHom.{u_2, u_5} (H ⧸ M) (I ⧸ O)) : (a : H ⧸ M) → I ⧸ O)
          (((map N M f hf : MonoidHom.{u_1, u_2} (G ⧸ N) (H ⧸ M)) : (a : G ⧸ N) → H ⧸ M) (↑x : G ⧸ N)) :
        I ⧸ O)
      (((map N O (g.comp f) hgf : MonoidHom.{u_1, u_5} (G ⧸ N) (I ⧸ O)) : (a : G ⧸ N) → I ⧸ O) (↑x : G ⧸ N) : I ⧸ O)
⊢ Eq.{u_5 + 1} (α := I ⧸ O)
    (((map M O g hg : MonoidHom.{u_2, u_5} (H ⧸ M) (I ⧸ O)) : (a : H ⧸ M) → I ⧸ O)
        (((map N M f hf : MonoidHom.{u_1, u_2} (G ⧸ N) (H ⧸ M)) : (a : G ⧸ N) → H ⧸ M) x) :
      I ⧸ O)
    (((map N O (g.comp f) hgf : MonoidHom.{u_1, u_5} (G ⧸ N) (I ⧸ O)) : (a : G ⧸ N) → I ⧸ O) x : I ⧸ O)

Tactic:
refine induction_on x fun x => ?_
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
N : Subgroup G
nN : N.Normal
I : Type u_5
inst_2 : Group I
M : Subgroup H
O : Subgroup I
inst_3 : M.Normal
inst_4 : O.Normal
f : G →* H
g : H →* I
hf : N ≤ Subgroup.comap f M
hg : M ≤ Subgroup.comap g O
hgf : N ≤ Subgroup.comap (g.comp f) O
x_1 : G ⧸ N
x : G
⊢ Eq.{u_5 + 1} (α := I ⧸ O)
    (((map M O g hg : MonoidHom.{u_2, u_5} (H ⧸ M) (I ⧸ O)) : (a : H ⧸ M) → I ⧸ O)
        (((map N M f hf : MonoidHom.{u_1, u_2} (G ⧸ N) (H ⧸ M)) : (a : G ⧸ N) → H ⧸ M) (↑x : G ⧸ N)) :
      I ⧸ O)
    (((map N O (g.comp f) hgf : MonoidHom.{u_1, u_5} (G ⧸ N) (I ⧸ O)) : (a : G ⧸ N) → I ⧸ O) (↑x : G ⧸ N) : I ⧸ O)

Tactic:
simp only [map_mk, MonoidHom.comp_apply]

Premises used: QuotientGroup.map_mk, MonoidHom.comp_apply
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
N : Subgroup G
nN : N.Normal
I : Type u_5
inst_2 : Group I
M : Subgroup H
O : Subgroup I
inst_3 : M.Normal
inst_4 : O.Normal
f : G →* H
g : H →* I
hf : N ≤ Subgroup.comap f M
hg : M ≤ Subgroup.comap g O
hgf : N ≤ Subgroup.comap (g.comp f) O
⊢ Eq (α := MonoidHom.{u_1, u_5} (G ⧸ N) (I ⧸ O)) (MonoidHom.comp (map M O g hg) (map N M f hf)) (map N O (g.comp f) hgf)

Tactic:
MonoidHom.ext (map_map N M O f g hf hg hgf)

Premises used: MonoidHom.ext, QuotientGroup.map_map
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
⊢ Eq (α := Set (G ⧸ N)) (mk '' (↑N : Set G)) 1

Tactic:
congr_arg ((↑) : Subgroup Q → Set Q) <| map_mk'_self N

Premises used: setOf, congr_arg, SetLike.coe, Set.image, QuotientGroup.map_mk'_self
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
s : Set G
h : ∀ (a : G), a ∈ preimage (β := G ⧸ N) mk (mk '' s) ↔ a ∈ (↑N : Set G) * s
⊢ preimage (β := G ⧸ N) mk (mk '' s) = (↑N : Set G) * s

Tactic:
ext a
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
h : a ∈ preimage (β := G ⧸ N) mk (mk '' s) → a ∈ (↑N : Set G) * s
h₁ : a ∈ (↑N : Set G) * s → a ∈ preimage (β := G ⧸ N) mk (mk '' s)
⊢ a ∈ preimage (β := G ⧸ N) mk (mk '' s) ↔ a ∈ (↑N : Set G) * s

Tactic:
constructor
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a b : G
hb : b ∈ s
h : Eq (α := G ⧸ N) (↑b : G ⧸ N) (↑a : G ⧸ N)
⊢ a ∈ (↑N : Set G) * s

Tactic:
⟨a / b, (QuotientGroup.eq_one_iff _).1 ?_, b, hb, div_mul_cancel _ _⟩

Premises used: Set.Mem, setOf, HDiv.hDiv, Set.image2, And.intro, Exists.intro, Iff.mp, div_mul_cancel, QuotientGroup.eq_one_iff
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a b : G
hb : b ∈ s
h : Eq (α := G ⧸ N) (↑b : G ⧸ N) (↑a : G ⧸ N)
h₁ : Eq (α := G ⧸ N) (↑(a / b) : G ⧸ N) 1
⊢ a ∈ (↑N : Set G) * s

Tactic:
refine ⟨a / b, (QuotientGroup.eq_one_iff _).1 ?_, b, hb, div_mul_cancel _ _⟩
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a b : G
hb : b ∈ s
h : Eq (α := G ⧸ N) (↑b : G ⧸ N) (↑a : G ⧸ N)
⊢ Eq (α := G ⧸ N) (↑(a / b) : G ⧸ N) 1

Tactic:
simp only [h, QuotientGroup.mk_div, div_self']

Premises used: div_self', QuotientGroup.mk_div
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
ha : a ∈ (↑N : Set G)
b : G
hb : b ∈ s
⊢ (fun (x1 x2 : G) ↦ x1 * x2) a b ∈ preimage (β := G ⧸ N) mk (mk '' s)

Tactic:
⟨b, hb, ?_⟩

Premises used: Set.Mem, setOf, Set.preimage, And.intro, Exists.intro, Set.image
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
ha : a ∈ (↑N : Set G)
b : G
hb : b ∈ s
h : Eq (α := G ⧸ N) (↑b : G ⧸ N) (↑((fun (x1 x2 : G) ↦ x1 * x2) a b) : G ⧸ N)
⊢ (fun (x1 x2 : G) ↦ x1 * x2) a b ∈ preimage (β := G ⧸ N) mk (mk '' s)

Tactic:
refine ⟨b, hb, ?_⟩
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
s : Set G
a : G
ha : a ∈ (↑N : Set G)
b : G
hb : b ∈ s
⊢ Eq (α := G ⧸ N) (↑b : G ⧸ N) (↑((fun (x1 x2 : G) ↦ x1 * x2) a b) : G ⧸ N)

Tactic:
simpa only [QuotientGroup.mk_mul, right_eq_mul, QuotientGroup.eq_one_iff]

Premises used: right_eq_mul, QuotientGroup.mk_mul, QuotientGroup.eq_one_iff
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
s t : Set G
simp_rw :
  Eq (α := Set (G ⧸ N)) (mk '' s) (mk '' t) ↔ preimage (β := G ⧸ N) mk (mk '' s) = preimage (β := G ⧸ N) mk (mk '' t)
⊢ Eq (α := Set (G ⧸ N)) (mk '' s) (mk '' t) ↔ (↑N : Set G) * s = (↑N : Set G) * t

Tactic:
simp_rw [← preimage_image_coe]

Premises used: QuotientGroup.preimage_image_coe
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
s t : Set G
⊢ Eq (α := Set (G ⧸ N)) (mk '' s) (mk '' t) ↔ preimage (β := G ⧸ N) mk (mk '' s) = preimage (β := G ⧸ N) mk (mk '' t)

Tactic:
QuotientGroup.mk_surjective.preimage_injective.eq_iff.symm

Premises used: Function.Injective.eq_iff, Function.Surjective.preimage_injective, QuotientGroup.mk_surjective, Iff.symm
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
s t : Set G
⊢ Eq (α := Set (G ⧸ N)) (mk '' s) (mk '' t) ↔ preimage (β := G ⧸ N) mk (mk '' s) = preimage (β := G ⧸ N) mk (mk '' t)

Tactic:
exact QuotientGroup.mk_surjective.preimage_injective.eq_iff.symm

Premises used: Function.Injective.eq_iff, Function.Surjective.preimage_injective, QuotientGroup.mk_surjective, Iff.symm
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M
N : Subgroup G
nN : N.Normal
G' : Subgroup G
H' : Subgroup H
inst_3 : G'.Normal
inst_4 : H'.Normal
e : G ≃* H
he : Subgroup.map (↑e : G →* H) G' = H'
x : G ⧸ G'
rw : (map G' G' (MonoidHom.comp (↑e.symm : H →* G) (↑e : G →* H)) ⋯ : (a : G ⧸ G') → G ⧸ G') x = x
⊢ ((map H' G' (↑e.symm : H →* G) ⋯ : MonoidHom.{u_2, u_1} (H ⧸ H') (G ⧸ G')) : (a : H ⧸ H') → G ⧸ G')
      (((map G' H' (↑e : G →* H) ⋯ : MonoidHom.{u_1, u_2} (G ⧸ G') (H ⧸ H')) : (a : G ⧸ G') → H ⧸ H') x) =
    x

Tactic:
rw [map_map G' H' G' e e.symm (he ▸ G'.le_comap_map (e : G →* H))
        (he ▸ (G'.map_equiv_eq_comap_symm e).le)]

Premises used: LE.le.trans_eq, Eq.rec, MonoidHomClass.toMonoidHom, Eq.le, Subgroup.le_comap_map, Subgroup.comap_mono, Subgroup.comap_comap, LE.le.trans, MulEquiv.symm, QuotientGroup.map_map, Subgroup.map_equiv_eq_comap_symm
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M
N : Subgroup G
nN : N.Normal
G' : Subgroup G
H' : Subgroup H
inst_3 : G'.Normal
inst_4 : H'.Normal
e : G ≃* H
he : Subgroup.map (↑e : G →* H) G' = H'
x : G ⧸ G'
⊢ (map G' G' (MonoidHom.comp (↑e.symm : H →* G) (↑e : G →* H)) ⋯ : (a : G ⧸ G') → G ⧸ G') x = x

Tactic:
simp only [← MulEquiv.coe_monoidHom_trans, MulEquiv.self_trans_symm,
        MulEquiv.coe_monoidHom_refl, map_id_apply]

Premises used: Subgroup.comap_id, Eq.le, MulEquiv.coe_monoidHom_trans, QuotientGroup.map_id_apply, MulEquiv.self_trans_symm, MulEquiv.coe_monoidHom_refl
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M
N : Subgroup G
nN : N.Normal
G' : Subgroup G
H' : Subgroup H
inst_3 : G'.Normal
inst_4 : H'.Normal
e : G ≃* H
he : Subgroup.map (↑e : G →* H) G' = H'
x : H ⧸ H'
rw : (map H' H' (MonoidHom.comp (↑e : G →* H) (↑e.symm : H →* G)) ⋯ : (a : H ⧸ H') → H ⧸ H') x = x
⊢ ((map G' H' (↑e : G →* H) ⋯ : MonoidHom.{u_1, u_2} (G ⧸ G') (H ⧸ H')) : (a : G ⧸ G') → H ⧸ H')
      (((map H' G' (↑e.symm : H →* G) ⋯ : MonoidHom.{u_2, u_1} (H ⧸ H') (G ⧸ G')) : (a : H ⧸ H') → G ⧸ G') x) =
    x

Tactic:
rw [map_map H' G' H' e.symm e (he ▸ (G'.map_equiv_eq_comap_symm e).le)
        (he ▸ G'.le_comap_map (e : G →* H))]

Premises used: LE.le.trans_eq, Eq.rec, MonoidHomClass.toMonoidHom, Eq.le, Subgroup.le_comap_map, Subgroup.comap_mono, Subgroup.comap_comap, LE.le.trans, MulEquiv.symm, QuotientGroup.map_map, Subgroup.map_equiv_eq_comap_symm
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst : Group G
inst_1 : Group H
inst_2 : Monoid M
N : Subgroup G
nN : N.Normal
G' : Subgroup G
H' : Subgroup H
inst_3 : G'.Normal
inst_4 : H'.Normal
e : G ≃* H
he : Subgroup.map (↑e : G →* H) G' = H'
x : H ⧸ H'
⊢ (map H' H' (MonoidHom.comp (↑e : G →* H) (↑e.symm : H →* G)) ⋯ : (a : H ⧸ H') → H ⧸ H') x = x

Tactic:
simp only [← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self,
        MulEquiv.coe_monoidHom_refl, map_id_apply]

Premises used: Subgroup.comap_id, MulEquiv.symm_trans_self, Eq.le, MulEquiv.coe_monoidHom_trans, QuotientGroup.map_id_apply, MulEquiv.coe_monoidHom_refl
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
G' : Subgroup G
H' : Subgroup H
inst_2 : G'.Normal
inst_3 : H'.Normal
e : G ≃* H
he : Subgroup.map (↑e : G →* H) G' = H'
x : G
⊢ Eq.{u_2 + 1} (α := H ⧸ H')
    (((congr G' H' e he : MulEquiv.{u_1, u_2} (G ⧸ G') (H ⧸ H')) : (a : G ⧸ G') → H ⧸ H') (↑x : G ⧸ G') : H ⧸ H')
    ((↑((e : (a : G) → H) x) : H ⧸ H') : H ⧸ H')

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
G' : Subgroup G
H' : Subgroup H
inst_2 : G'.Normal
inst_3 : H'.Normal
e : G ≃* H
he : Subgroup.map (↑e : G →* H) G' = H'
x : G
⊢ Eq.{u_2 + 1} (α := H ⧸ H')
    (((congr G' H' e he : MulEquiv.{u_1, u_2} (G ⧸ G') (H ⧸ H')) : (a : G ⧸ G') → H ⧸ H')
        ((mk' G' : (a : G) → G ⧸ G') x) :
      H ⧸ H')
    ((mk' H' : (a : H) → H ⧸ H') ((e : (a : G) → H) x) : H ⧸ H')

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
G' : Subgroup G
H' : Subgroup H
inst_2 : G'.Normal
inst_3 : H'.Normal
e : G ≃* H
he : Subgroup.map (↑e : G →* H) G' = H'
x : G
⊢ Eq.{u_2 + 1} (α := H ⧸ H')
    (((congr G' H' e he : MulEquiv.{u_1, u_2} (G ⧸ G') (H ⧸ H')) : (a : G ⧸ G') → H ⧸ H') (↑x : G ⧸ G') : H ⧸ H')
    ((mk' H' : (a : H) → H ⧸ H') ((e : (a : G) → H) x) : H ⧸ H')

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
G' : Subgroup G
inst_1 : G'.Normal
he : Subgroup.map (↑(MulEquiv.refl G) : G →* G) G' = G'
h :
  ∀ (x : G ⧸ G') (x : G),
    Eq (α := G ⧸ G')
      ((congr G' G' (MulEquiv.refl G) he : (a : G ⧸ G') → G ⧸ G') (Quot.mk (⇑(leftRel G') : G → G → Prop) x) : G ⧸ G')
      ((MulEquiv.refl (G ⧸ G') : (a : G ⧸ G') → G ⧸ G') (Quot.mk (⇑(leftRel G') : G → G → Prop) x) : G ⧸ G')
⊢ Eq (α := G ⧸ G' ≃* G ⧸ G') (congr G' G' (MulEquiv.refl G) he) (MulEquiv.refl (G ⧸ G'))

Tactic:
ext ⟨x⟩
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
G' : Subgroup G
inst_1 : G'.Normal
he : Subgroup.map (↑(MulEquiv.refl G) : G →* G) G' = G'
x_1 : G ⧸ G'
x : G
⊢ Eq (α := G ⧸ G')
    ((congr G' G' (MulEquiv.refl G) he : (a : G ⧸ G') → G ⧸ G') (Quot.mk (⇑(leftRel G') : G → G → Prop) x) : G ⧸ G')
    ((MulEquiv.refl (G ⧸ G') : (a : G ⧸ G') → G ⧸ G') (Quot.mk (⇑(leftRel G') : G → G → Prop) x) : G ⧸ G')

Tactic:
rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
inst : Group G
inst_1 : Group H
G' : Subgroup G
H' : Subgroup H
inst_2 : G'.Normal
inst_3 : H'.Normal
e : G ≃* H
he : Subgroup.map (↑e : G →* H) G' = H'
⊢ Eq (α := MulEquiv.{u_2, u_1} (H ⧸ H') (G ⧸ G')) (MulEquiv.symm (congr G' H' e he)) (congr H' G' e.symm ⋯)

Tactic:
rfl

Premises used: QuotientGroup.congr, Equiv.symm, MulEquiv.symm, rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Finite
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
rw : Finite.{u_2 + 1} ((G ⧸ H) × ↥H) ↔ Finite.{u_2 + 1} ↥H ∧ Finite.{u_2 + 1} (G ⧸ H)
rw₁ : Finite.{u_2 + 1} (G ⧸ H) ∧ Finite.{u_2 + 1} ↥H ↔ Finite.{u_2 + 1} ↥H ∧ Finite.{u_2 + 1} (G ⧸ H)
rw₂ rw₃ : Finite.{u_2 + 1} ↥H ∧ Finite.{u_2 + 1} (G ⧸ H) ↔ Finite.{u_2 + 1} ↥H ∧ Finite.{u_2 + 1} (G ⧸ H)
⊢ Finite G ↔ Finite.{u_2 + 1} ↥H ∧ Finite.{u_2 + 1} (G ⧸ H)

Tactic:
rw [(groupEquivQuotientProdSubgroup (s := H)).finite_iff, Prod.finite_iff, and_comm]

Premises used: Equiv.finite_iff, Subgroup.groupEquivQuotientProdSubgroup, and_comm, Prod.finite_iff
-- Module: Mathlib.GroupTheory.QuotientGroup.Finite
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
inst_1 : Finite.{u_2 + 1} ↥H
inst_2 : Finite.{u_2 + 1} (G ⧸ H)
rw : Finite.{u_2 + 1} ↥H ∧ Finite.{u_2 + 1} (G ⧸ H)
rw₁ : Subgroup G
⊢ Finite G

Tactic:
rw [finite_iff_subgroup_quotient]

Premises used: finite_iff_subgroup_quotient
-- Module: Mathlib.GroupTheory.QuotientGroup.Finite
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
inst_1 : Finite.{u_2 + 1} ↥H
inst_2 : Finite.{u_2 + 1} (G ⧸ H)
left : Finite.{u_2 + 1} ↥H
right : Finite.{u_2 + 1} (G ⧸ H)
⊢ Finite.{u_2 + 1} ↥H ∧ Finite.{u_2 + 1} (G ⧸ H)

Tactic:
constructor
-- Module: Mathlib.GroupTheory.QuotientGroup.Finite
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
inst_1 : Finite.{u_2 + 1} ↥H
inst_2 : Finite.{u_2 + 1} (G ⧸ H)
⊢ Finite.{u_2 + 1} ↥H

Tactic:
assumption
-- Module: Mathlib.GroupTheory.QuotientGroup.Finite
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
inst_1 : Finite.{u_2 + 1} ↥H
inst_2 : Finite.{u_2 + 1} (G ⧸ H)
⊢ Finite.{u_2 + 1} (G ⧸ H)

Tactic:
assumption
-- Module: Mathlib.GroupTheory.QuotientGroup.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
a b p : G
rw :
  b ≡ a [PMOD p] ↔
    Eq (α := HasQuotient.Quotient G (B := AddSubgroup G) (AddSubgroup.zmultiples p)) (↑a : G ⧸ AddSubgroup.zmultiples p)
      (↑b : G ⧸ AddSubgroup.zmultiples p)
⊢ a ≡ b [PMOD p] ↔
    Eq (α := HasQuotient.Quotient G (B := AddSubgroup G) (AddSubgroup.zmultiples p)) (↑a : G ⧸ AddSubgroup.zmultiples p)
      (↑b : G ⧸ AddSubgroup.zmultiples p)

Tactic:
rw [modEq_comm]

Premises used: AddCommGroup.modEq_comm
-- Module: Mathlib.GroupTheory.QuotientGroup.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
a b p : G
simp_rw :
  (∃ (z : ℤ), a = b + z • p) ↔
    Eq (α := HasQuotient.Quotient G (B := AddSubgroup G) (AddSubgroup.zmultiples p)) (↑a : G ⧸ AddSubgroup.zmultiples p)
      (↑b : G ⧸ AddSubgroup.zmultiples p)
simp_rw₁ : (∃ (z : ℤ), a = b + z • p) ↔ Membership.mem (γ := AddSubgroup G) (AddSubgroup.zmultiples p) (a - b)
simp_rw₂ : (∃ (z : ℤ), a = b + z • p) ↔ ∃ (k : ℤ), k • p = a - b
simp_rw₃ : (∃ (z : ℤ), a = b + z • p) ↔ ∃ (k : ℤ), b + k • p = a
⊢ b ≡ a [PMOD p] ↔
    Eq (α := HasQuotient.Quotient G (B := AddSubgroup G) (AddSubgroup.zmultiples p)) (↑a : G ⧸ AddSubgroup.zmultiples p)
      (↑b : G ⧸ AddSubgroup.zmultiples p)

Tactic:
simp_rw [modEq_iff_eq_add_zsmul, QuotientAddGroup.eq_iff_sub_mem, AddSubgroup.mem_zmultiples_iff,
    eq_sub_iff_add_eq', eq_comm]

Premises used: eq_sub_iff_add_eq', QuotientAddGroup.eq_iff_sub_mem, AddSubgroup.mem_zmultiples_iff, eq_comm, AddCommGroup.modEq_iff_eq_add_zsmul
-- Module: Mathlib.GroupTheory.QuotientGroup.ModEq
Goal:
G : Type u_1
inst : AddCommGroup G
a b p : G
⊢ ¬a ≡ b [PMOD p] ↔
    Ne (α := HasQuotient.Quotient G (B := AddSubgroup G) (AddSubgroup.zmultiples p)) (↑a : G ⧸ AddSubgroup.zmultiples p)
      (↑b : G ⧸ AddSubgroup.zmultiples p)

Tactic:
modEq_iff_eq_mod_zmultiples.not

Premises used: Iff.not, AddCommGroup.modEq_iff_eq_mod_zmultiples
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
inst : Group G
h : FG G
⊢ ∃ (S : Finset G), S.card = rank G ∧ Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤

Tactic:
@Nat.find_spec _ (Classical.decPred _) (fg_iff'.mp h)

Premises used: Group.fg_iff', Iff.mp, Group.rank, Nat.find_spec
-- Module: Mathlib.GroupTheory.Rank
Goal:
G : Type u_1
inst : Group G
h : FG G
S : Finset G
hS : Eq (α := Subgroup G) (Subgroup.closure (↑S : Set G)) ⊤
⊢ rank G ≤ S.card

Tactic:
@Nat.find_le _ _ (Classical.decPred _) (fg_iff'.mp h) ⟨S, rfl, hS⟩

Premises used: Nat.find_le, And.intro, Exists.intro, Group.rank, rfl