awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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)
⊢ (leftRel φ.ker : G → G → Prop) a b
have rw₃ : HMul.hMul (α := ↥φ.range) (β := ↥φ.range) ((φ.rangeRestrict : (a : G) → ↥φ.range) a⁻¹ : ↥φ.range)
    ((φ.rangeRestrict : (a : G) → ↥φ.range) b : ↥φ.range) =
  1
Tactic: rw [leftRel_apply, ← ker_rangeRestrict, mem_ker, φ.rangeRestrict.map_mul, ← h,
        φ.rangeRestrict.map_inv, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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
⊢ (leftRel φ.ker : G → G → Prop) a b
have rw₄ : HMul.hMul (α := ↥φ.range) (β := ↥φ.range) ((φ.rangeRestrict : (a : G) → ↥φ.range) a⁻¹ : ↥φ.range)
    ((φ.rangeRestrict : (a : G) → ↥φ.range) a : ↥φ.range) =
  1
Tactic: rw [leftRel_apply, ← ker_rangeRestrict, mem_ker, φ.rangeRestrict.map_mul, ← h,
        φ.rangeRestrict.map_inv, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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
⊢ (leftRel φ.ker : G → G → Prop) a b
have rw₅ : HMul.hMul (α := ↥φ.range) (β := ↥φ.range) (((φ.rangeRestrict : (a : G) → ↥φ.range) a)⁻¹ : ↥φ.range)
    ((φ.rangeRestrict : (a : G) → ↥φ.range) a : ↥φ.range) =
  1
Tactic: rw [leftRel_apply, ← ker_rangeRestrict, mem_ker, φ.rangeRestrict.map_mul, ← h,
        φ.rangeRestrict.map_inv, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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
⊢ (leftRel φ.ker : G → G → Prop) a b
have rw₆ : Eq.{v + 1} (α := ↥φ.range) 1 1
Tactic: rw [leftRel_apply, ← ker_rangeRestrict, mem_ker, φ.rangeRestrict.map_mul, ← h,
        φ.rangeRestrict.map_inv, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
Goal:
G : Type u
inst : Group G
H : Type v
inst_1 : Group H
φ : G →* H
g : G
⊢ ∃ (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)
have 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) sorry : ↥φ.range)
Tactic: use mk g
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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
⊢ Eq.{v + 1} (α := H) ((kerLift φ : (a : G ⧸ φ.ker) → H) ((mk ∘ ψ) ((kerLift φ : (a : G ⧸ φ.ker) → H) x)) : H)
    ((kerLift φ : (a : G ⧸ φ.ker) → H) x : H)
have 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)
Tactic: rw [Function.comp_apply, kerLift_mk, hφ]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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)
⊢ Eq.{v + 1} (α := H) ((kerLift φ : (a : G ⧸ φ.ker) → H) ((mk ∘ ψ) ((kerLift φ : (a : G ⧸ φ.ker) → H) x)) : H)
    ((kerLift φ : (a : G ⧸ φ.ker) → H) x : H)
have rw₁ : Eq.{v + 1} (α := H) ((φ : (a : G) → H) (ψ ((kerLift φ : (a : G ⧸ φ.ker) → H) x)) : H)
  ((kerLift φ : (a : G ⧸ φ.ker) → H) x : H)
Tactic: rw [Function.comp_apply, kerLift_mk, hφ]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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)
⊢ Eq.{v + 1} (α := H) ((kerLift φ : (a : G ⧸ φ.ker) → H) ((mk ∘ ψ) ((kerLift φ : (a : G ⧸ φ.ker) → H) x)) : H)
    ((kerLift φ : (a : G ⧸ φ.ker) → H) x : H)
have rw₂ : Eq.{v + 1} (α := H) ((kerLift φ : (a : G ⧸ φ.ker) → H) x : H) ((kerLift φ : (a : G ⧸ φ.ker) → H) x : H)
Tactic: rw [Function.comp_apply, kerLift_mk, hφ]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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
⊢ Eq (α := ↥A ⧸ A'.subgroupOf A →* ↥A ⧸ A'.subgroupOf A)
    (MonoidHom.comp (quotientMapSubgroupOfOfLe ⋯ ⋯) (quotientMapSubgroupOfOfLe ⋯ ⋯))
    (MonoidHom.id (↥A ⧸ A'.subgroupOf A))
have h₁ : ∀ (x : G) (hx : x ∈ A),
  Eq (α := ↥A ⧸ A'.subgroupOf A)
    ((MonoidHom.comp (MonoidHom.comp (quotientMapSubgroupOfOfLe sorry sorry) (quotientMapSubgroupOfOfLe sorry sorry))
            (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: ext ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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
⊢ Eq (α := ↥B ⧸ B'.subgroupOf B →* ↥B ⧸ B'.subgroupOf B)
    (MonoidHom.comp (quotientMapSubgroupOfOfLe ⋯ ⋯) (quotientMapSubgroupOfOfLe ⋯ ⋯))
    (MonoidHom.id (↥B ⧸ B'.subgroupOf B))
have h₁ : ∀ (x : G) (hx : x ∈ B),
  Eq (α := ↥B ⧸ B'.subgroupOf B)
    ((MonoidHom.comp (MonoidHom.comp (quotientMapSubgroupOfOfLe sorry sorry) (quotientMapSubgroupOfOfLe sorry sorry))
            (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: ext ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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)))
    (MulEquiv.refl (HasQuotient.Quotient A (B := Subgroup A) (range (G := A) (zpowGroupHom n))))
    (equivQuotientZPowOfEquiv (MulEquiv.refl A) n)
have 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)))
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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)
        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)))
have 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)))
Tactic: rw [← Quotient.out_eq' x]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
Goal:
A B C : Type u
inst : CommGroup A
inst_1 : CommGroup B
inst_2 : CommGroup C
e : A ≃* B
d : B ≃* C
n : ℤ
⊢ (equivQuotientZPowOfEquiv e n).trans (equivQuotientZPowOfEquiv d n) = equivQuotientZPowOfEquiv (e.trans d) n
have 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)))
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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)
        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)))
have 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)))
Tactic: rw [← Quotient.out_eq' x]
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (hypothesis)
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
⊢ ∃ (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) :
        Quotient (α := ↥(H ⊔ N)) (leftRel (N.subgroupOf (H ⊔ N))))
have hy₁ : y ∈ (↑(H ⊔ N) : Set G)
Tactic: rw [← SetLike.mem_coe] at hy
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (hypothesis)
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)
⊢ ∃ (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))))
have hy₁ : y ∈ (↑H : Set G) * (↑N : Set G)
Tactic: rw [coe_mul_of_left_le_normalizer_right H N hLE] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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)
⊢ ∃ (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))))
have 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))))
Tactic: rcases hy with ⟨h, hh, n, hn, rfl⟩
Cleared hypotheses: y, hy_1, hy
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (hypothesis)
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
⊢ ∃ (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))))
have hn₁ : n ∈ N
Tactic: simp only [SetLike.mem_coe] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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
⊢ ∃ (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))))
have 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))))
Tactic: use ⟨h, hh⟩
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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))))
have h₁ : (leftRel (N.subgroupOf (H ⊔ N)) : ↥(H ⊔ N) → ↥(H ⊔ N) → Prop)
  ((inclusion sorry : (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: refine Quotient.eq.mpr ?_
-- Lean 4 proof step from Mathlib.GroupTheory.QuotientGroup.Basic (goal)
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
⊢ 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))
have 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) sorry) (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: ext