awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
H : Type v
inst_1 : Group H
φ : G →* H
a_1 b_1 : G ⧸ φ.ker
a b : G
h :
  Eq.{v + 1} (α := ↥φ.range) ((φ.rangeRestrict : (a : G) → ↥φ.range) a : ↥φ.range)
    ((φ.rangeRestrict : (a : G) → ↥φ.range) b : ↥φ.range)
rw : a⁻¹ * b ∈ φ.ker
rw₁ : a⁻¹ * b ∈ φ.rangeRestrict.ker
rw₂ : Eq.{v + 1} (α := ↥φ.range) ((φ.rangeRestrict : (a : G) → ↥φ.range) (a⁻¹ * b) : ↥φ.range) (1 : ↥φ.range)
rw₃ :
  HMul.hMul (α := ↥φ.range) (β := ↥φ.range) ((φ.rangeRestrict : (a : G) → ↥φ.range) a⁻¹ : ↥φ.range)
      ((φ.rangeRestrict : (a : G) → ↥φ.range) b : ↥φ.range) =
    1
rw₄ :
  HMul.hMul (α := ↥φ.range) (β := ↥φ.range) ((φ.rangeRestrict : (a : G) → ↥φ.range) a⁻¹ : ↥φ.range)
      ((φ.rangeRestrict : (a : G) → ↥φ.range) a : ↥φ.range) =
    1
rw₅ :
  HMul.hMul (α := ↥φ.range) (β := ↥φ.range) (((φ.rangeRestrict : (a : G) → ↥φ.range) a)⁻¹ : ↥φ.range)
      ((φ.rangeRestrict : (a : G) → ↥φ.range) a : ↥φ.range) =
    1
rw₆ rw₇ : Eq.{v + 1} (α := ↥φ.range) 1 1
⊢ (leftRel φ.ker : G → G → Prop) a b

Tactic:
rw [leftRel_apply, ← ker_rangeRestrict, mem_ker, φ.rangeRestrict.map_mul, ← h,
        φ.rangeRestrict.map_inv, inv_mul_cancel]

Premises used: inv_mul_cancel, MonoidHom.rangeRestrict, MonoidHom.ker_rangeRestrict, MonoidHom.mem_ker, MonoidHom.map_inv, MonoidHom.map_mul, QuotientGroup.leftRel_apply
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
H : Type v
inst_1 : Group H
φ : G →* H
g : G
h :
  Eq.{v + 1} (α := ↥φ.range) ((rangeKerLift φ : (a : G ⧸ φ.ker) → ↥φ.range) (↑g : G ⧸ φ.ker) : ↥φ.range)
    (Subtype.mk (p := fun (x : H) ↦ x ∈ φ.range) ((φ : (a : G) → H) g) ⋯ : ↥φ.range)
⊢ ∃ (a : G ⧸ φ.ker),
    Eq.{v + 1} (α := ↥φ.range) ((rangeKerLift φ : (a : G ⧸ φ.ker) → ↥φ.range) a : ↥φ.range)
      (Subtype.mk (p := fun (x : H) ↦ x ∈ φ.range) ((φ : (a : G) → H) g) ⋯ : ↥φ.range)

Tactic:
use mk g

Premises used: QuotientGroup.mk
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
H : Type v
inst_1 : Group H
φ : G →* H
g : G
⊢ Eq.{v + 1} (α := ↥φ.range) ((rangeKerLift φ : (a : G ⧸ φ.ker) → ↥φ.range) (↑g : G ⧸ φ.ker) : ↥φ.range)
    (Subtype.mk (p := fun (x : H) ↦ x ∈ φ.range) ((φ : (a : G) → H) g) ⋯ : ↥φ.range)

Tactic:
rfl
-- 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 : Type x
inst_2 : Monoid M
φ : G →* H
ψ : H → G
hφ : RightInverse ψ (⇑φ : (a : G) → H)
x : G ⧸ φ.ker
rw :
  Eq.{v + 1} (α := H) ((kerLift φ : (a : G ⧸ φ.ker) → H) (↑(ψ ((kerLift φ : (a : G ⧸ φ.ker) → H) x)) : G ⧸ φ.ker) : H)
    ((kerLift φ : (a : G ⧸ φ.ker) → H) x : H)
rw₁ :
  Eq.{v + 1} (α := H) ((φ : (a : G) → H) (ψ ((kerLift φ : (a : G ⧸ φ.ker) → H) x)) : H)
    ((kerLift φ : (a : G ⧸ φ.ker) → H) x : H)
rw₂ rw₃ : Eq.{v + 1} (α := H) ((kerLift φ : (a : G ⧸ φ.ker) → H) x : H) ((kerLift φ : (a : G ⧸ φ.ker) → H) x : H)
⊢ Eq.{v + 1} (α := H) ((kerLift φ : (a : G ⧸ φ.ker) → H) ((mk ∘ ψ) ((kerLift φ : (a : G ⧸ φ.ker) → H) x)) : H)
    ((kerLift φ : (a : G ⧸ φ.ker) → H) x : H)

Tactic:
rw [Function.comp_apply, kerLift_mk, hφ]

Premises used: QuotientGroup.kerLift_mk, Function.comp_apply
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
M N : Subgroup G
inst_1 : M.Normal
inst_2 : N.Normal
h : M = N
x : G
⊢ Eq (α := G ⧸ N) ((quotientMulEquivOfEq h : (a : G ⧸ M) → G ⧸ N) (↑x : G ⧸ M) : G ⧸ N) ((↑x : G ⧸ N) : G ⧸ N)

Tactic:
rfl

Premises used: Quot.map, Quotient.map', rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
G : Type u
inst : Group G
A' A B' B : Subgroup G
_hAN : (A'.subgroupOf A).Normal
_hBN : (B'.subgroupOf B).Normal
h' : A' ≤ B'
h : A ≤ B
x : ↥A
⊢ Eq (α := ↥B ⧸ B'.subgroupOf B)
    ((quotientMapSubgroupOfOfLe h' h : (a : ↥A ⧸ A'.subgroupOf A) → ↥B ⧸ B'.subgroupOf B) (↑x : ↥A ⧸ A'.subgroupOf A) :
      ↥B ⧸ B'.subgroupOf B)
    ((↑((Subgroup.inclusion h : (a : ↥A) → ↥B) x) : ↥B ⧸ B'.subgroupOf B) : ↥B ⧸ B'.subgroupOf B)

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, rfl
-- 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 : Type x
inst_2 : Monoid M
φ : G →* H
A' A B' B : Subgroup G
hAN : (A'.subgroupOf A).Normal
hBN : (B'.subgroupOf B).Normal
h' : A' = B'
h : A = B
h₁ :
  ∀ (x : G) (hx : x ∈ A),
    Eq (α := ↥A ⧸ A'.subgroupOf A)
      ((MonoidHom.comp (MonoidHom.comp (quotientMapSubgroupOfOfLe ⋯ ⋯) (quotientMapSubgroupOfOfLe ⋯ ⋯))
              (mk' (A'.subgroupOf A)) :
            (a : ↥A) → ↥A ⧸ A'.subgroupOf A)
          (Subtype.mk (p := fun (x : G) ↦ x ∈ A) x hx) :
        ↥A ⧸ A'.subgroupOf A)
      ((MonoidHom.comp (MonoidHom.id (↥A ⧸ A'.subgroupOf A)) (mk' (A'.subgroupOf A)) : (a : ↥A) → ↥A ⧸ A'.subgroupOf A)
          (Subtype.mk (p := fun (x : G) ↦ x ∈ A) x hx) :
        ↥A ⧸ A'.subgroupOf A)
⊢ Eq (α := ↥A ⧸ A'.subgroupOf A →* ↥A ⧸ A'.subgroupOf A)
    (MonoidHom.comp (quotientMapSubgroupOfOfLe ⋯ ⋯) (quotientMapSubgroupOfOfLe ⋯ ⋯))
    (MonoidHom.id (↥A ⧸ A'.subgroupOf A))

Tactic:
ext ⟨x, hx⟩
-- 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 : Type x
inst_2 : Monoid M
φ : G →* H
A' A B' B : Subgroup G
hAN : (A'.subgroupOf A).Normal
hBN : (B'.subgroupOf B).Normal
h' : A' = B'
h : A = B
x : G
hx : x ∈ A
⊢ Eq (α := ↥A ⧸ A'.subgroupOf A)
    ((MonoidHom.comp (MonoidHom.comp (quotientMapSubgroupOfOfLe ⋯ ⋯) (quotientMapSubgroupOfOfLe ⋯ ⋯))
            (mk' (A'.subgroupOf A)) :
          (a : ↥A) → ↥A ⧸ A'.subgroupOf A)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ A) x hx) :
      ↥A ⧸ A'.subgroupOf A)
    ((MonoidHom.comp (MonoidHom.id (↥A ⧸ A'.subgroupOf A)) (mk' (A'.subgroupOf A)) : (a : ↥A) → ↥A ⧸ A'.subgroupOf A)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ A) x hx) :
      ↥A ⧸ A'.subgroupOf A)

Tactic:
rfl
-- 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 : Type x
inst_2 : Monoid M
φ : G →* H
A' A B' B : Subgroup G
hAN : (A'.subgroupOf A).Normal
hBN : (B'.subgroupOf B).Normal
h' : A' = B'
h : A = B
h₁ :
  ∀ (x : G) (hx : x ∈ B),
    Eq (α := ↥B ⧸ B'.subgroupOf B)
      ((MonoidHom.comp (MonoidHom.comp (quotientMapSubgroupOfOfLe ⋯ ⋯) (quotientMapSubgroupOfOfLe ⋯ ⋯))
              (mk' (B'.subgroupOf B)) :
            (a : ↥B) → ↥B ⧸ B'.subgroupOf B)
          (Subtype.mk (p := fun (x : G) ↦ x ∈ B) x hx) :
        ↥B ⧸ B'.subgroupOf B)
      ((MonoidHom.comp (MonoidHom.id (↥B ⧸ B'.subgroupOf B)) (mk' (B'.subgroupOf B)) : (a : ↥B) → ↥B ⧸ B'.subgroupOf B)
          (Subtype.mk (p := fun (x : G) ↦ x ∈ B) x hx) :
        ↥B ⧸ B'.subgroupOf B)
⊢ Eq (α := ↥B ⧸ B'.subgroupOf B →* ↥B ⧸ B'.subgroupOf B)
    (MonoidHom.comp (quotientMapSubgroupOfOfLe ⋯ ⋯) (quotientMapSubgroupOfOfLe ⋯ ⋯))
    (MonoidHom.id (↥B ⧸ B'.subgroupOf B))

Tactic:
ext ⟨x, hx⟩
-- 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 : Type x
inst_2 : Monoid M
φ : G →* H
A' A B' B : Subgroup G
hAN : (A'.subgroupOf A).Normal
hBN : (B'.subgroupOf B).Normal
h' : A' = B'
h : A = B
x : G
hx : x ∈ B
⊢ Eq (α := ↥B ⧸ B'.subgroupOf B)
    ((MonoidHom.comp (MonoidHom.comp (quotientMapSubgroupOfOfLe ⋯ ⋯) (quotientMapSubgroupOfOfLe ⋯ ⋯))
            (mk' (B'.subgroupOf B)) :
          (a : ↥B) → ↥B ⧸ B'.subgroupOf B)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ B) x hx) :
      ↥B ⧸ B'.subgroupOf B)
    ((MonoidHom.comp (MonoidHom.id (↥B ⧸ B'.subgroupOf B)) (mk' (B'.subgroupOf B)) : (a : ↥B) → ↥B ⧸ B'.subgroupOf B)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ B) x hx) :
      ↥B ⧸ B'.subgroupOf B)

Tactic:
rfl
-- 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 : Type x
inst_2 : Monoid M
φ : G →* H
A B C : Type u
inst_3 : CommGroup A
inst_4 : CommGroup B
inst_5 : CommGroup C
f : A →* B
g_1 : B →* A
e : A ≃* B
d : B ≃* C
n : ℤ
g : A
h_1 : Membership.mem (γ := Subgroup A) (range (G := A) (zpowGroupHom n)) g
h : A
hg : h ^ n = g
⊢ Eq (α := B) (((zpowGroupHom n : B →* B) : (a : B) → B) ((f : (a : A) → B) h : B) : B) ((f : (a : A) → B) g : B)

Tactic:
simp only [← hg, map_zpow, zpowGroupHom_apply]

Premises used: map_zpow, zpowGroupHom_apply
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
A : Type u
inst : CommGroup A
n : ℤ
⊢ Eq (α :=
    HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n)) →*
      HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n)))
    (homQuotientZPowOfHom (MonoidHom.id A) n)
    (MonoidHom.id (HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n))))

Tactic:
monoidHom_ext _ rfl

Premises used: QuotientGroup.monoidHom_ext, rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
A B : Type u
inst : CommGroup A
inst_1 : CommGroup B
f : A →* B
g : B →* A
n : ℤ
⊢ homQuotientZPowOfHom (f.comp g) n = (homQuotientZPowOfHom f n).comp (homQuotientZPowOfHom g n)

Tactic:
monoidHom_ext _ rfl

Premises used: QuotientGroup.monoidHom_ext, rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
A B : Type u
inst : CommGroup A
inst_1 : CommGroup B
f : A →* B
g : B →* A
n : ℤ
i : RightInverse (α := A) (β := B) (⇑g : (a : B) → A) (⇑f : (a : A) → B)
⊢ (homQuotientZPowOfHom f n).comp (homQuotientZPowOfHom g n) =
    MonoidHom.id (HasQuotient.Quotient B (B := Subgroup B) (range (G := B) (zpowGroupHom n)))

Tactic:
monoidHom_ext _ <| MonoidHom.ext fun x => congrArg _ <| i x

Premises used: congrArg, MonoidHom.ext, QuotientGroup.monoidHom_ext, Setoid.r, Quot.mk
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
A : Type u
inst : CommGroup A
n : ℤ
h :
  ∀ (x : HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n))),
    Eq (α := HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n)))
      ((MulEquiv.refl (HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n))) :
            (a : A ⧸ (zpowGroupHom n).range) → A ⧸ (zpowGroupHom n).range)
          x :
        HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n)))
      ((equivQuotientZPowOfEquiv (MulEquiv.refl A) n : (a : A ⧸ (zpowGroupHom n).range) → A ⧸ (zpowGroupHom n).range)
          x :
        HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n)))
⊢ Eq (α :=
    HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n)) ≃*
      HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n)))
    (MulEquiv.refl (HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n))))
    (equivQuotientZPowOfEquiv (MulEquiv.refl A) n)

Tactic:
ext x
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
A : Type u
inst : CommGroup A
n : ℤ
x : HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n))
h :
  Eq (α := HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n)))
    ((MulEquiv.refl (HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n))) :
          (a : A ⧸ (zpowGroupHom n).range) → A ⧸ (zpowGroupHom n).range)
        (Quotient.mk'' (Quotient.out x)) :
      HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n)))
    ((equivQuotientZPowOfEquiv (MulEquiv.refl A) n : (a : A ⧸ (zpowGroupHom n).range) → A ⧸ (zpowGroupHom n).range)
        (Quotient.mk'' (Quotient.out x)) :
      HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n)))
⊢ Eq (α := HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n)))
    ((MulEquiv.refl (HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n))) :
          (a : A ⧸ (zpowGroupHom n).range) → A ⧸ (zpowGroupHom n).range)
        x :
      HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n)))
    ((equivQuotientZPowOfEquiv (MulEquiv.refl A) n : (a : A ⧸ (zpowGroupHom n).range) → A ⧸ (zpowGroupHom n).range) x :
      HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n)))

Tactic:
rw [← Quotient.out_eq' x]

Premises used: Quotient.out_eq'
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
A : Type u
inst : CommGroup A
n : ℤ
x : HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n))
⊢ Eq (α := HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n)))
    ((MulEquiv.refl (HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n))) :
          (a : A ⧸ (zpowGroupHom n).range) → A ⧸ (zpowGroupHom n).range)
        (Quotient.mk'' (Quotient.out x)) :
      HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n)))
    ((equivQuotientZPowOfEquiv (MulEquiv.refl A) n : (a : A ⧸ (zpowGroupHom n).range) → A ⧸ (zpowGroupHom n).range)
        (Quotient.mk'' (Quotient.out x)) :
      HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n)))

Tactic:
rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
A B : Type u
inst : CommGroup A
inst_1 : CommGroup B
e : A ≃* B
n : ℤ
⊢ (equivQuotientZPowOfEquiv e n).symm = equivQuotientZPowOfEquiv e.symm n

Tactic:
rfl

Premises used: MonoidHom.toMulEquiv, Equiv.symm, QuotientGroup.equivQuotientZPowOfEquiv, MulEquiv.symm, rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
A B C : Type u
inst : CommGroup A
inst_1 : CommGroup B
inst_2 : CommGroup C
e : A ≃* B
d : B ≃* C
n : ℤ
h :
  ∀ (x : HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n))),
    Eq (α := HasQuotient.Quotient C (B := Subgroup C) (range (G := C) (zpowGroupHom n)))
      (((equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n) :
            (a : A ⧸ (zpowGroupHom n).range) → C ⧸ (zpowGroupHom n).range)
          x :
        HasQuotient.Quotient C (B := Subgroup C) (range (G := C) (zpowGroupHom n)))
      ((equivQuotientZPowOfEquiv (e.trans d) n : (a : A ⧸ (zpowGroupHom n).range) → C ⧸ (zpowGroupHom n).range) x :
        HasQuotient.Quotient C (B := Subgroup C) (range (G := C) (zpowGroupHom n)))
⊢ (equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n) = equivQuotientZPowOfEquiv (e.trans d) n

Tactic:
ext x
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
A B C : Type u
inst : CommGroup A
inst_1 : CommGroup B
inst_2 : CommGroup C
e : A ≃* B
d : B ≃* C
n : ℤ
x : HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n))
h :
  Eq (α := HasQuotient.Quotient C (B := Subgroup C) (range (G := C) (zpowGroupHom n)))
    (((equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n) :
          (a : A ⧸ (zpowGroupHom n).range) → C ⧸ (zpowGroupHom n).range)
        (Quotient.mk'' (Quotient.out x)) :
      HasQuotient.Quotient C (B := Subgroup C) (range (G := C) (zpowGroupHom n)))
    ((equivQuotientZPowOfEquiv (e.trans d) n : (a : A ⧸ (zpowGroupHom n).range) → C ⧸ (zpowGroupHom n).range)
        (Quotient.mk'' (Quotient.out x)) :
      HasQuotient.Quotient C (B := Subgroup C) (range (G := C) (zpowGroupHom n)))
⊢ Eq (α := HasQuotient.Quotient C (B := Subgroup C) (range (G := C) (zpowGroupHom n)))
    (((equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n) :
          (a : A ⧸ (zpowGroupHom n).range) → C ⧸ (zpowGroupHom n).range)
        x :
      HasQuotient.Quotient C (B := Subgroup C) (range (G := C) (zpowGroupHom n)))
    ((equivQuotientZPowOfEquiv (e.trans d) n : (a : A ⧸ (zpowGroupHom n).range) → C ⧸ (zpowGroupHom n).range) x :
      HasQuotient.Quotient C (B := Subgroup C) (range (G := C) (zpowGroupHom n)))

Tactic:
rw [← Quotient.out_eq' x]

Premises used: Quotient.out_eq'
-- Module: Mathlib.GroupTheory.QuotientGroup.Basic
Goal:
A B C : Type u
inst : CommGroup A
inst_1 : CommGroup B
inst_2 : CommGroup C
e : A ≃* B
d : B ≃* C
n : ℤ
x : HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n))
⊢ Eq (α := HasQuotient.Quotient C (B := Subgroup C) (range (G := C) (zpowGroupHom n)))
    (((equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n) :
          (a : A ⧸ (zpowGroupHom n).range) → C ⧸ (zpowGroupHom n).range)
        (Quotient.mk'' (Quotient.out x)) :
      HasQuotient.Quotient C (B := Subgroup C) (range (G := C) (zpowGroupHom n)))
    ((equivQuotientZPowOfEquiv (e.trans d) n : (a : A ⧸ (zpowGroupHom n).range) → C ⧸ (zpowGroupHom n).range)
        (Quotient.mk'' (Quotient.out x)) :
      HasQuotient.Quotient C (B := Subgroup C) (range (G := C) (zpowGroupHom n)))

Tactic:
rfl
-- 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))
y : G
hy : y ∈ H ⊔ N
⊢ y ∈ (↑(H ⊔ N) : Set G)

Tactic:
rw [← SetLike.mem_coe] at hy

Premises used: SetLike.mem_coe
-- 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))
y : G
hy_1 : y ∈ H ⊔ N
hy : y ∈ (↑(H ⊔ N) : Set G)
⊢ y ∈ (↑H : Set G) * (↑N : Set G)

Tactic:
rw [coe_mul_of_left_le_normalizer_right H N hLE] at hy

Premises used: Subgroup.coe_mul_of_left_le_normalizer_right
-- 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))
y : G
hy_1 : y ∈ H ⊔ N
hy : y ∈ (↑H : Set G) * (↑N : Set G)
rcases :
  ∀ (h : G) (hh : h ∈ (↑H : Set G)) (n : G) (hn : n ∈ (↑N : Set G)) (hy : (fun (x1 x2 : G) ↦ x1 * x2) h n ∈ H ⊔ N),
    ∃ (a : ↥H),
      Eq (α := HasQuotient.Quotient ↥(H ⊔ N) (B := Subgroup ↥(H ⊔ N)) (N.subgroupOf (H ⊔ N)))
        ((φ : (a : ↥H) → ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)) a :
          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))))
⊢ ∃ (a : ↥H),
    Eq (α := HasQuotient.Quotient ↥(H ⊔ N) (B := Subgroup ↥(H ⊔ N)) (N.subgroupOf (H ⊔ N)))
      ((φ : (a : ↥H) → ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)) a :
        HasQuotient.Quotient ↥(H ⊔ N) (B := Subgroup ↥(H ⊔ N)) (N.subgroupOf (H ⊔ N)))
      (Quotient.mk'' (Subtype.mk (p := fun (x : G) ↦ x ∈ H ⊔ N) y hy_1) :
        Quotient (α := ↥(H ⊔ N)) (leftRel (N.subgroupOf (H ⊔ N))))

Tactic:
rcases hy with ⟨h, hh, n, hn, rfl⟩

Premises used: rfl
-- 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
hn : n ∈ (↑N : Set G)
hy : (fun (x1 x2 : G) ↦ x1 * x2) h n ∈ H ⊔ N
⊢ n ∈ N

Tactic:
simp only [SetLike.mem_coe] at hn

Premises used: SetLike.mem_coe
-- 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₁ :
  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))))
⊢ ∃ (a : ↥H),
    Eq (α := HasQuotient.Quotient ↥(H ⊔ N) (B := Subgroup ↥(H ⊔ N)) (N.subgroupOf (H ⊔ N)))
      ((φ : (a : ↥H) → ↥(H ⊔ N) ⧸ N.subgroupOf (H ⊔ N)) a :
        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:
use ⟨h, hh⟩
-- 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
⊢ 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:
Quotient.eq.mpr ?_

Premises used: Iff.mpr, Quotient.eq