awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
h : H
⊢ Membership.mem (α := PushoutI (G := G) φ) (γ := Subgroup (PushoutI (G := G) φ)) (MonoidHom.range (of (G := G) j))
    ((MonoidHom.comp (of (G := G) j) (φ j) : (a : H) → PushoutI φ) h : PushoutI (G := G) φ)

Tactic:
MonoidHom.mem_range.2 ⟨φ j h, rfl⟩

Premises used: Iff.mpr, MonoidHom.mem_range, Exists.intro, DFunLike.coe, rfl
-- Module: Mathlib.GroupTheory.PushoutI
Goal:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst : (i : ι) → Group (G i)
inst_1 : Group H
φ : (i : ι) → MonoidHom.{u_3, u_2} H (G i)
hφ : ∀ (i : ι), Injective.{u_3 + 1, u_2 + 1} (α := H) (β := G i) (⇑(φ i) : (a : H) → G i)
i j : ι
hij : i ≠ j
h : H
⊢ Membership.mem (α := PushoutI (G := G) φ) (γ := Subgroup (PushoutI (G := G) φ)) (MonoidHom.range (of (G := G) j))
    ((MonoidHom.comp (of (G := G) j) (φ j) : (a : H) → PushoutI φ) h : PushoutI (G := G) φ)

Tactic:
exact MonoidHom.mem_range.2 ⟨φ j h, rfl⟩

Premises used: Iff.mpr, MonoidHom.mem_range, Exists.intro, DFunLike.coe, rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
h : ∀ (x x_1 : G), x_1⁻¹ * x ∈ N
h₁ : ∀ (x : G), x ∈ N ↔ Membership.mem (γ := Subgroup G) ⊤ x
⊢ N = ⊤

Tactic:
ext
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
h : ∀ (x x_1 : G), x_1⁻¹ * x ∈ N
x : G
⊢ x ∈ N ↔ Membership.mem (γ := Subgroup G) ⊤ x

Tactic:
simpa using h _ 1

Premises used: OfNat.ofNat
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
h : N = ⊤
⊢ ∀ (x x_1 : G), x_1⁻¹ * x ∈ N

Tactic:
simp [h]
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
⊢ leftRel N = ⊤ ↔ N = ⊤

Tactic:
simpa [leftRel, MulAction.orbitRel, funext_iff, MulAction.mem_orbit_iff,
    MulAction.subgroup_smul_def, ← eq_inv_mul_iff_mul_eq]
    using ⟨fun h ↦ by ext; simpa using h _ 1, fun h ↦ by simp [h]⟩

Premises used: funext_iff, MulAction.mem_orbit_iff, QuotientGroup.leftRel, MulAction.orbitRel, eq_inv_mul_iff_mul_eq, MulAction.subgroup_smul_def
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
h : ∀ (x x_1 : G), x * x_1⁻¹ ∈ N
h₁ : ∀ (x : G), x ∈ N ↔ Membership.mem (γ := Subgroup G) ⊤ x
⊢ N = ⊤

Tactic:
ext
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
h : ∀ (x x_1 : G), x * x_1⁻¹ ∈ N
x : G
⊢ x ∈ N ↔ Membership.mem (γ := Subgroup G) ⊤ x

Tactic:
simpa using h _ 1

Premises used: OfNat.ofNat
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
h : N = ⊤
⊢ ∀ (x x_1 : G), x * x_1⁻¹ ∈ N

Tactic:
simp [h]
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
⊢ rightRel N = ⊤ ↔ N = ⊤

Tactic:
simpa [rightRel, MulAction.orbitRel, funext_iff, MulAction.mem_orbit_iff,
    MulAction.subgroup_smul_def, ← eq_mul_inv_iff_mul_eq]
    using ⟨fun h ↦ by ext; simpa using h _ 1, fun h ↦ by simp [h]⟩

Premises used: funext_iff, MulAction.mem_orbit_iff, MulAction.orbitRel, eq_mul_inv_iff_mul_eq, MulAction.subgroup_smul_def, QuotientGroup.rightRel
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
⊢ Subsingleton.{u_1 + 1} (G ⧸ N) ↔ N = ⊤

Tactic:
simp [HasQuotient.Quotient]

Premises used: HasQuotient.Quotient
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
⊢ Nontrivial.{u_1} (G ⧸ N) ↔ N ≠ ⊤

Tactic:
simp [← not_subsingleton_iff_nontrivial]

Premises used: not_subsingleton_iff_nontrivial
-- 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
a b c d : G
hab : (leftRel N : G → G → Prop) a b
hcd : (leftRel N : G → G → Prop) c d
rw : ∀ (hab : a⁻¹ * b ∈ N) (hcd : c⁻¹ * d ∈ N), (fun (x y : G) ↦ x⁻¹ * y ∈ N) (a * c) (b * d)
⊢ (leftRel N : G → G → Prop) (a * c) (b * d)

Tactic:
rw [leftRel_eq] at hab hcd ⊢

Premises used: QuotientGroup.leftRel_eq
-- 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
a b c d : G
hab : a⁻¹ * b ∈ N
hcd : c⁻¹ * d ∈ N
⊢ c⁻¹ * (a⁻¹ * b) * c⁻¹⁻¹ * (c⁻¹ * d) ∈ N

Tactic:
N.mul_mem (nN.conj_mem _ hab _) hcd

Premises used: Subgroup.mul_mem, Subgroup.Normal.conj_mem
-- 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
a b c d : G
hab : a⁻¹ * b ∈ N
hcd : c⁻¹ * d ∈ N
⊢ c⁻¹ * (a⁻¹ * b) * c⁻¹⁻¹ * (c⁻¹ * d) = (a * c)⁻¹ * (b * d)

Tactic:
simp only [mul_inv_rev, mul_assoc, inv_mul_cancel_left]

Premises used: inv_mul_cancel_left, mul_assoc, mul_inv_rev
-- 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
a b c d : G
hab : a⁻¹ * b ∈ N
hcd : c⁻¹ * d ∈ N
N₁ : c⁻¹ * (a⁻¹ * b) * c⁻¹⁻¹ * (c⁻¹ * d) = (a * c)⁻¹ * (b * d)
⊢ (a * c)⁻¹ * (b * d) ∈ N

Tactic:
calc
      c⁻¹ * (a⁻¹ * b) * c⁻¹⁻¹ * (c⁻¹ * d) ∈ N := N.mul_mem (nN.conj_mem _ hab _) hcd
      _ = (a * c)⁻¹ * (b * d) := by
        simp only [mul_inv_rev, mul_assoc, inv_mul_cancel_left]

Premises used: HMul.hMul, Inv.inv, Subgroup.mul_mem, Subgroup.Normal.conj_mem
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
M : Type u_4
inst : Group G
inst_1 : Monoid M
f : G →* M
H : ∀ (x y : G), (QuotientGroup.con f.ker : (a : G) → G → Prop) x y ↔ (Con.ker f : (a : G) → G → Prop) x y
⊢ QuotientGroup.con f.ker = Con.ker f

Tactic:
ext
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
M : Type u_4
inst : Group G
inst_1 : Monoid M
f : G →* M
x y : G
H : ({ toSetoid := leftRel f.ker, mul' := ⋯ } : (a : G) → G → Prop) x y ↔ (Con.ker f : (a : G) → G → Prop) x y
H₁ : (leftRel f.ker : G → G → Prop) x y ↔ (Con.ker f : (a : G) → G → Prop) x y
H₂ : (leftRel f.ker : G → G → Prop) y x ↔ (Con.ker f : (a : G) → G → Prop) x y
H₃ : y⁻¹ * x ∈ f.ker ↔ (Con.ker f : (a : G) → G → Prop) x y
H₄ : y⁻¹ * x ∈ f.ker ↔ Eq.{u_4 + 1} (α := M) ((f : (a : G) → M) x : M) ((f : (a : G) → M) y : M)
H₅ H₆ : y⁻¹ * x ∈ f.ker ↔ y⁻¹ * x ∈ f.ker
⊢ (QuotientGroup.con f.ker : (a : G) → G → Prop) x y ↔ (Con.ker f : (a : G) → G → Prop) x y

Tactic:
rw [QuotientGroup.con, Con.rel_mk, Setoid.comm', leftRel_apply, Con.ker_rel, MonoidHom.eq_iff]

Premises used: Con.ker_rel, Con.rel_mk, QuotientGroup.con, MonoidHom.eq_iff, Setoid.comm', QuotientGroup.leftRel_apply
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
⊢ Eq (α := (a : G) → G ⧸ N) (⇑(mk' N) : (a : G) → G ⧸ N) mk

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
x : G
⊢ Eq (α := G ⧸ N) ((mk' N : (a : G) → G ⧸ N) x : G ⧸ N) ((↑x : G ⧸ N) : G ⧸ N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
⊢ Surjective (α := G) (β := G ⧸ N) (⇑(mk' N) : (a : G) → G ⧸ N)

Tactic:
@mk_surjective _ _ N

Premises used: QuotientGroup.mk_surjective
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
x y : G
⊢ x⁻¹ * y ∈ N ↔ ∃ z ∈ N, x * z = y

Tactic:
simp only [← _root_.eq_inv_mul_iff_mul_eq, exists_eq_right]

Premises used: exists_eq_right, eq_inv_mul_iff_mul_eq
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
M : Type u_4
inst : Group G
inst_1 : Monoid M
N : Subgroup G
nN : N.Normal
f g : MonoidHom.{u_1, u_4} (G ⧸ N) M
h : f.comp (mk' N) = g.comp (mk' N)
⊢ f = g

Tactic:
MonoidHom.ext fun x => QuotientGroup.induction_on x <| (DFunLike.congr_fun h :)

Premises used: MonoidHom.ext, QuotientGroup.induction_on
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
x : G
⊢ Eq (α := G ⧸ N) (↑x : G ⧸ N) 1 ↔ x ∈ N

Tactic:
QuotientGroup.eq.trans ?_

Premises used: QuotientGroup.eq, MulAction.orbitRel, Iff.trans
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
x : G
refine : x⁻¹ * 1 ∈ N ↔ x ∈ N
⊢ Eq (α := G ⧸ N) (↑x : G ⧸ N) 1 ↔ x ∈ N

Tactic:
refine QuotientGroup.eq.trans ?_

Premises used: QuotientGroup.eq, Iff.trans
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
x : G
rw : x⁻¹ ∈ N ↔ x ∈ N
rw₁ rw₂ : x ∈ N ↔ x ∈ N
⊢ x⁻¹ * 1 ∈ N ↔ x ∈ N

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
inst : Group G
N : Subgroup G
nN : N.Normal
h :
  ∀ (x : ↥N),
    Eq (α := G ⧸ N) ((MonoidHom.comp (mk' N) N.subtype : (a : ↥N) → G ⧸ N) x : G ⧸ N) ((1 : (a : ↥N) → G ⧸ N) x : G ⧸ N)
⊢ Eq (α := ↥N →* G ⧸ N) (MonoidHom.comp (mk' N) N.subtype) 1

Tactic:
ext
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
x : ↥N
⊢ Eq (α := G ⧸ N) ((MonoidHom.comp (mk' N) N.subtype : (a : ↥N) → G ⧸ N) x : G ⧸ N) ((1 : (a : ↥N) → G ⧸ N) x : G ⧸ N)

Tactic:
simp
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
⊢ Eq (α := Subgroup (G ⧸ N)) (MonoidHom.range (mk' N)) ⊤

Tactic:
MonoidHom.range_eq_top.mpr (mk'_surjective N)

Premises used: Iff.mpr, MonoidHom.range_eq_top, QuotientGroup.mk'_surjective
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Group G
inst_1 : Group H
inst_2 : MulOneClass I
f : G →* H
inst_3 : f.range.Normal
g : H →* I
h : Eq (α := ↥g.ker →* H ⧸ f.range) (MonoidHom.comp (mk' f.range) g.ker.subtype) 1
x : H
hx : x ∈ g.ker
⊢ Eq (α := H ⧸ f.range) (↑x : H ⧸ f.range) 1

Tactic:
DFunLike.congr_fun h ⟨x, hx⟩

Premises used: DFunLike.congr_fun
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
H : Type u_2
I : Type u_3
inst : Group G
inst_1 : Group H
inst_2 : MulOneClass I
f : G →* H
inst_3 : f.range.Normal
g : H →* I
h : Eq (α := ↥g.ker →* H ⧸ f.range) (MonoidHom.comp (mk' f.range) g.ker.subtype) 1
x : H
hx : x ∈ g.ker
⊢ Eq (α := H ⧸ f.range) (↑x : H ⧸ f.range) 1

Tactic:
exact DFunLike.congr_fun h ⟨x, hx⟩

Premises used: DFunLike.congr_fun
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
⊢ MonoidHom.ker (mk' N) = N

Tactic:
Subgroup.ext eq_one_iff

Premises used: QuotientGroup.eq_one_iff, Subgroup.ext
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
x y : G
⊢ Eq (α := G ⧸ N) (↑x : G ⧸ N) (↑y : G ⧸ N) ↔ x / y ∈ N

Tactic:
eq_comm.trans (QuotientGroup.eq.trans ?_)

Premises used: QuotientGroup.eq, eq_comm, Iff.trans
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
x y : G
refine : y⁻¹ * x ∈ N ↔ x / y ∈ N
⊢ Eq (α := G ⧸ N) (↑x : G ⧸ N) (↑y : G ⧸ N) ↔ x / y ∈ N

Tactic:
refine eq_comm.trans (QuotientGroup.eq.trans ?_)

Premises used: QuotientGroup.eq, eq_comm, Iff.trans
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
x y : G
rw : x * y⁻¹ ∈ N ↔ x / y ∈ N
rw₁ rw₂ : x * y⁻¹ ∈ N ↔ x * y⁻¹ ∈ N
⊢ y⁻¹ * x ∈ N ↔ x / y ∈ N

Tactic:
rw [nN.mem_comm_iff, div_eq_mul_inv]

Premises used: Subgroup.Normal.mem_comm_iff, div_eq_mul_inv
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
⊢ Eq.{u_1 + 1} (α := G ⧸ N) (↑1 : G ⧸ N) 1

Tactic:
rfl

Premises used: MulAction.orbitRel, rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
a b : G
⊢ (↑(a * b) : G ⧸ N) = HMul.hMul (α := G ⧸ N) (↑a : G ⧸ N) (↑b : G ⧸ N)

Tactic:
rfl

Premises used: Quotient.map₂, rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
a : G
⊢ Eq (α := G ⧸ N) (↑a⁻¹ : G ⧸ N) (↑a : G ⧸ N)⁻¹

Tactic:
rfl

Premises used: Quot.map, Quotient.map', rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
a b : G
⊢ (↑(a / b) : G ⧸ N) = HDiv.hDiv (α := G ⧸ N) (↑a : G ⧸ N) (↑b : G ⧸ N)

Tactic:
rfl

Premises used: Quotient.map₂, rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
a : G
n : ℕ
⊢ (↑(a ^ n) : G ⧸ N) = HPow.hPow (α := G ⧸ N) (↑a : G ⧸ N) n

Tactic:
rfl

Premises used: Quot.map, Quotient.map', rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
a : G
n : ℤ
⊢ (↑(a ^ n) : G ⧸ N) = HPow.hPow (α := G ⧸ N) (↑a : G ⧸ N) n

Tactic:
rfl

Premises used: Quot.map, Quotient.map', rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
nN : N.Normal
⊢ Eq (α := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) N) ⊥

Tactic:
aesop
-- 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
c : Con G
a b : G
hx : Membership.mem (γ := Set G) {x : G | (c : (a : G) → G → Prop) x 1} a
hy : Membership.mem (γ := Set G) {x : G | (c : (a : G) → G → Prop) x 1} b
⊢ Membership.mem (γ := Set G) {x : G | (c : (a : G) → G → Prop) x 1} (a * b)

Tactic:
simpa using c.mul hx hy

Premises used: Con.mul
-- 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
c : Con G
x : G
h : Membership.mem (γ := Set G) {x : G | (c : (a : G) → G → Prop) x 1} x
⊢ Membership.mem (γ := Set G) {x : G | (c : (a : G) → G → Prop) x 1} x⁻¹

Tactic:
simpa using c.inv h

Premises used: Con.inv
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
c : Con G
x : G
⊢ x ∈ c.subgroup ↔ (c : (a : G) → G → Prop) x 1

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- 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
c : Con G
x : G
hx : x ∈ c.subgroup
g : G
⊢ g * x * g⁻¹ ∈ c.subgroup

Tactic:
simpa using (c.mul (c.mul (c.refl g) hx) (c.refl g⁻¹))

Premises used: Con.mul, Con.refl, Inv.inv
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
h : ∀ (x : G), x ∈ (QuotientGroup.con H).subgroup ↔ x ∈ H
⊢ (QuotientGroup.con H).subgroup = H

Tactic:
ext
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
inst_1 : H.Normal
x : G
⊢ x ∈ (QuotientGroup.con H).subgroup ↔ x ∈ H

Tactic:
simp [QuotientGroup.con, leftRel_apply]

Premises used: QuotientGroup.con, QuotientGroup.leftRel_apply
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
c : Con G
H : ∀ (x y : G), (QuotientGroup.con c.subgroup : (a : G) → G → Prop) x y ↔ (c : (a : G) → G → Prop) x y
⊢ QuotientGroup.con c.subgroup = c

Tactic:
ext x y
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
c : Con G
x y : G
H : (c : (a : G) → G → Prop) (x⁻¹ * y) 1 ↔ (c : (a : G) → G → Prop) x y
⊢ (QuotientGroup.con c.subgroup : (a : G) → G → Prop) x y ↔ (c : (a : G) → G → Prop) x y

Tactic:
rw [QuotientGroup.con, Con.rel_mk, leftRel_apply, Con.mem_subgroup_iff]

Premises used: Con.mem_subgroup_iff, Con.rel_mk, QuotientGroup.con, QuotientGroup.leftRel_apply
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
c : Con G
x y : G
h : (c : (a : G) → G → Prop) (x⁻¹ * y) 1
⊢ (c : (a : G) → G → Prop) x y

Tactic:
simpa using c.mul (c.refl x) (c.symm h)

Premises used: Con.mul, Con.refl, Con.symm
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
c : Con G
x y : G
h : (c : (a : G) → G → Prop) x y
⊢ (c : (a : G) → G → Prop) (x⁻¹ * y) 1

Tactic:
simpa using c.mul (c.refl x⁻¹) (c.symm h)

Premises used: Con.mul, Con.refl, Con.symm, Inv.inv
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
c : Con G
x y : G
⊢ (c : (a : G) → G → Prop) (x⁻¹ * y) 1 ↔ (c : (a : G) → G → Prop) x y

Tactic:
exact ⟨fun h ↦ by simpa using c.mul (c.refl x) (c.symm h),
    fun h ↦ by simpa using c.mul (c.refl x⁻¹) (c.symm h)⟩
-- 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
simp :
  ∀ {a b : { N : Subgroup G // N.Normal }},
    (∀ {x y : G}, x⁻¹ * y ∈ (↑a : Subgroup G) → x⁻¹ * y ∈ (↑b : Subgroup G)) ↔ a ≤ b
⊢ ∀ {a b : { N : Subgroup G // N.Normal }},
    LE.le (α := Con G)
        (({ toFun := fun (N : { N : Subgroup G // N.Normal }) ↦ QuotientGroup.con (↑N : Subgroup G),
                invFun := fun (c : Con G) ↦ Subtype.mk (p := fun (N : Subgroup G) ↦ N.Normal) c.subgroup ⋯,
                left_inv := ⋯, right_inv := ⋯ } :
              (a : { N : Subgroup G // N.Normal }) → Con G)
            a :
          Con G)
        (({ toFun := fun (N : { N : Subgroup G // N.Normal }) ↦ QuotientGroup.con (↑N : Subgroup G),
                invFun := fun (c : Con G) ↦ Subtype.mk (p := fun (N : Subgroup G) ↦ N.Normal) c.subgroup ⋯,
                left_inv := ⋯, right_inv := ⋯ } :
              (a : { N : Subgroup G // N.Normal }) → Con G)
            b :
          Con G) ↔
      a ≤ b

Tactic:
simp only [QuotientGroup.con, Equiv.coe_fn_mk, Con.le_def, Con.rel_mk, leftRel_apply]

Premises used: Con.rel_mk, QuotientGroup.con, Con.le_def, Equiv.coe_fn_mk, QuotientGroup.leftRel_apply
-- 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
a b : { N : Subgroup G // N.Normal }
⊢ (∀ {x y : G}, x⁻¹ * y ∈ (↑a : Subgroup G) → x⁻¹ * y ∈ (↑b : Subgroup G)) ↔ a ≤ b

Tactic:
⟨fun h x _ ↦ ?_, fun hle _ _ h ↦ hle h⟩

Premises used: Iff.intro
-- 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
refine :
  ∀ {a b : { N : Subgroup G // N.Normal }} (h : ∀ {x y : G}, x⁻¹ * y ∈ (↑a : Subgroup G) → x⁻¹ * y ∈ (↑b : Subgroup G)),
    ∀ x ∈ (↑a : Subgroup G), x ∈ (↑b : Subgroup G)
⊢ ∀ {a b : { N : Subgroup G // N.Normal }},
    (∀ {x y : G}, x⁻¹ * y ∈ (↑a : Subgroup G) → x⁻¹ * y ∈ (↑b : Subgroup G)) ↔ a ≤ b

Tactic:
refine ⟨fun h x _ ↦ ?_, fun hle _ _ h ↦ hle h⟩
-- 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
a b : { N : Subgroup G // N.Normal }
h : ∀ {x y : G}, x⁻¹ * y ∈ (↑a : Subgroup G) → x⁻¹ * y ∈ (↑b : Subgroup G)
x : G
h_1 : x ∈ (↑a : Subgroup G)
⊢ 1⁻¹ * x ∈ (↑a : Subgroup G) → 1⁻¹ * x ∈ (↑b : Subgroup G)

Tactic:
specialize @h 1 x
-- 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
a b : { N : Subgroup G // N.Normal }
x : G
h_1 : x ∈ (↑a : Subgroup G)
h : 1⁻¹ * x ∈ (↑a : Subgroup G) → 1⁻¹ * x ∈ (↑b : Subgroup G)
⊢ x ∈ (↑b : Subgroup G)

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N M : Subgroup G
inst_1 : N.Normal
inst_2 : M.Normal
⊢ QuotientGroup.con N ≤ QuotientGroup.con M ↔ N ≤ M

Tactic:
(Subgroup.orderIsoCon.map_rel_iff (a := ⟨N, inferInstance⟩) (b := ⟨M, inferInstance⟩))

Premises used: Set.Mem, RelIso.map_rel_iff, Subgroup.orderIsoCon
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
inst : Group G
N M : Subgroup G
hN : N.Normal
hM : M.Normal
h : N ≤ M
⊢ QuotientGroup.con N ≤ QuotientGroup.con M

Tactic:
con_le_iff.mpr h

Premises used: Iff.mpr, QuotientGroup.con_le_iff
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
M : Type u_4
inst : Group G
inst_1 : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* M
HN : N ≤ φ.ker
g : G
⊢ Eq.{u_4 + 1} (α := M) ((lift N φ HN : (a : G ⧸ N) → M) (↑g : G ⧸ N) : M) ((φ : (a : G) → M) g : M)

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
M : Type u_4
inst : Group G
inst_1 : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* M
HN : N ≤ φ.ker
⊢ MonoidHom.comp (lift N φ HN) (mk' N) = φ

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
M : Type u_4
inst : Group G
inst_1 : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* M
HN : N ≤ φ.ker
g : G
⊢ Eq.{u_4 + 1} (α := M) ((lift N φ HN : (a : G ⧸ N) → M) (Quot.mk (⇑(leftRel N) : G → G → Prop) g) : M)
    ((φ : (a : G) → M) g : M)

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, rfl
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
M : Type u_4
inst : Group G
inst_1 : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* M
hφ : Surjective.{u_1 + 1, u_4 + 1} (α := G) (β := M) (⇑φ : (a : G) → M)
HN : N ≤ φ.ker
⊢ Surjective.{u_1 + 1, u_4 + 1} (α := G ⧸ N) (β := M) (⇑(lift N φ HN) : (a : G ⧸ N) → M)

Tactic:
Quotient.lift_surjective _ _ hφ

Premises used: Quotient.liftOn', MulAction.orbitRel, Quotient.lift_surjective, Con.Quotient, Quotient, Con.liftOn
-- Module: Mathlib.GroupTheory.QuotientGroup.Defs
Goal:
G : Type u_1
M : Type u_4
inst : Group G
inst_1 : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* M
HN : N ≤ φ.ker
rw :
  Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (lift N φ HN))
    (Subgroup.map (mk' N) (MonoidHom.comp (lift N φ HN) (mk' N)).ker)
rw₁ :
  Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (lift N φ HN))
    (Subgroup.map (mk' N) (Subgroup.comap (mk' N) (MonoidHom.ker (lift N φ HN))))
rw₂ rw₃ : Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (lift N φ HN)) (MonoidHom.ker (lift N φ HN))
⊢ Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (lift N φ HN)) (Subgroup.map (mk' N) φ.ker)

Tactic:
rw [← congrArg MonoidHom.ker (lift_comp_mk' N φ HN), ← MonoidHom.comap_ker,
    Subgroup.map_comap_eq_self_of_surjective (mk'_surjective N)]

Premises used: congrArg, QuotientGroup.lift_comp_mk', MonoidHom.ker, Subgroup.map_comap_eq_self_of_surjective, QuotientGroup.mk'_surjective, MonoidHom.comap_ker
-- 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 →* H
hφ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
HN : N = φ.ker
rw : Eq (α := Subgroup (G ⧸ N)) (MonoidHom.ker (lift N φ ⋯)) ⊥
rw₁ : Eq (α := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) φ.ker) ⊥
rw₂ : Eq (α := Subgroup (G ⧸ N)) (Subgroup.map (mk' N) N) ⊥
rw₃ rw₄ : Eq.{u_1 + 1} (α := Subgroup (G ⧸ N)) ⊥ ⊥
⊢ Injective.{u_1 + 1, u_2 + 1} (α := G ⧸ N) (β := H) (⇑(lift N φ ⋯) : (a : G ⧸ N) → H)

Tactic:
rw [← MonoidHom.ker_eq_bot_iff, ker_lift, ← HN, QuotientGroup.map_mk'_self]

Premises used: QuotientGroup.ker_lift, MonoidHom.ker_eq_bot_iff, QuotientGroup.map_mk'_self
-- 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
φ : G →* H
hφ : Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑φ : (a : G) → H)
HN : N = φ.ker
g : G
⊢ Eq.{u_2 + 1} (α := H) ((liftEquiv N hφ HN : (a : G ⧸ N) → H) (↑g : G ⧸ N) : H) ((φ : (a : G) → H) g : H)

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, rfl