awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
f : Perm α
h : ∀ (x : α), Membership.mem (α := α) s ((f : (a : α) → α) x : α) ↔ x ∈ s
a : ↥s
⊢ a ∈ (f.subtypePerm (p := Membership.mem s) h).support ↔
    Membership.mem (γ := Finset ↥s) {x : ↥s | (f : (a : α) → α) (↑x : α) ≠ (↑x : α)} a

Tactic:
simp [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h : σ ≠ 1
rw : 1 < card.{u_1} (α := α) {x : α | ¬(σ : (a : α) → α) x = x}
⊢ card.{u_1} (α := α) {x : α | (σ : (a : α) → α) x = x} < Fintype.card α - 1

Tactic:
rw [Nat.lt_sub_iff_add_lt, ← Nat.lt_sub_iff_add_lt', ← Finset.card_compl, Finset.compl_filter]

Premises used: Nat.lt_sub_iff_add_lt, Finset.card_compl, Nat.lt_sub_iff_add_lt', Finset.compl_filter
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h : σ ≠ 1
⊢ 1 < card.{u_1} (α := α) {x : α | ¬(σ : (a : α) → α) x = x}

Tactic:
one_lt_card_support_of_ne_one h

Premises used: Equiv.Perm.support, Equiv.Perm.one_lt_card_support_of_ne_one
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
h : σ ≠ 1
⊢ 1 < card.{u_1} (α := α) {x : α | ¬(σ : (a : α) → α) x = x}

Tactic:
exact one_lt_card_support_of_ne_one h

Premises used: Equiv.Perm.one_lt_card_support_of_ne_one
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
h : ∀ (a : α), a ∈ (σ * τ * σ⁻¹).support ↔ a ∈ map (Equiv.toEmbedding σ) τ.support
⊢ (σ * τ * σ⁻¹).support = map (Equiv.toEmbedding σ) τ.support

Tactic:
ext
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
a : α
⊢ a ∈ (σ * τ * σ⁻¹).support ↔ a ∈ map (Equiv.toEmbedding σ) τ.support

Tactic:
simp only [mem_map_equiv, Perm.coe_mul, Function.comp_apply, Ne, Perm.mem_support,
    Equiv.eq_symm_apply, inv_def]

Premises used: Equiv.Perm.coe_mul, Equiv.Perm.mem_support, Ne, Finset.mem_map_equiv, Equiv.Perm.inv_def, Function.comp_apply, Equiv.eq_symm_apply
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
σ τ : Perm α
⊢ #(σ * τ * σ⁻¹).support = #τ.support

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.ViaEmbedding
Goal:
α : Type u_1
β : Type u_2
e : Perm α
ι : α ↪ β
x : α
⊢ Eq (α := β) ((e.viaEmbedding ι : (a : β) → β) ((ι : (a : α) → β) x : β) : β)
    ((ι : (a : α) → β) ((e : (a : α) → α) x : α) : β)

Tactic:
extendDomain_apply_image e (ofInjective ι.1 ι.2) x

Premises used: Set.Mem, Equiv.Perm.extendDomain_apply_image, Function.Embedding.inj', Equiv.ofInjective, Function.Embedding.toFun
-- Module: Mathlib.GroupTheory.Perm.ViaEmbedding
Goal:
α : Type u_1
β : Type u_2
e : Perm α
ι : α ↪ β
x : β
hx : ¬Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑ι : (a : α) → β)) x
⊢ (e.viaEmbedding ι : (a : β) → β) x = x

Tactic:
extendDomain_apply_not_subtype e (ofInjective ι.1 ι.2) hx

Premises used: Function.Embedding.inj', Equiv.Perm.extendDomain_apply_not_subtype, Equiv.ofInjective, Function.Embedding.toFun
-- Module: Mathlib.GroupTheory.Perm.ViaEmbedding
Goal:
α : Type u_1
β : Type u_2
e : Perm α
ι : α ↪ β
⊢ (viaEmbeddingHom ι : (a : Perm α) → Perm β) e = e.viaEmbedding ι

Tactic:
rfl

Premises used: Equiv.Perm.extendDomain, Equiv.Perm.viaEmbedding, Equiv.Perm.subtypeCongr, rfl
-- Module: Mathlib.GroupTheory.Perm.ViaEmbedding
Goal:
α : Type u_1
β : Type u_2
ι : α ↪ β
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := Perm α) (β := Perm β) (⇑(viaEmbeddingHom ι) : (a : Perm α) → Perm β)

Tactic:
extendDomainHom_injective (ofInjective ι.1 ι.2)

Premises used: Function.Embedding.inj', Equiv.ofInjective, Function.Embedding.toFun, Equiv.Perm.extendDomainHom_injective
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
rels : Set (FreeGroup α)
⊢ Function.Surjective (α := FreeGroup α) (β := PresentedGroup rels)
    (⇑(mk rels) : (a : FreeGroup α) → PresentedGroup rels)

Tactic:
QuotientGroup.mk_surjective

Premises used: PresentedGroup, QuotientGroup.mk_surjective
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
rels : Set (FreeGroup α)
x : FreeGroup α
⊢ Eq (α := PresentedGroup rels) ((mk rels : (a : FreeGroup α) → PresentedGroup rels) x : PresentedGroup rels)
      (1 : PresentedGroup rels) ↔
    Membership.mem (γ := Subgroup (FreeGroup α)) (Subgroup.normalClosure rels) x

Tactic:
QuotientGroup.eq_one_iff _

Premises used: PresentedGroup, QuotientGroup.eq_one_iff
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
rels : Set (FreeGroup α)
x : FreeGroup α
hx : x ∈ rels
⊢ Eq (α := PresentedGroup rels) ((mk rels : (a : FreeGroup α) → PresentedGroup rels) x : PresentedGroup rels)
    (1 : PresentedGroup rels)

Tactic:
mk_eq_one_iff.mpr <| Subgroup.subset_normalClosure hx

Premises used: Iff.mpr, PresentedGroup.mk_eq_one_iff, Subgroup.subset_normalClosure
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
rels : Set (FreeGroup α)
x y : FreeGroup α
hx : x * y⁻¹ ∈ rels
⊢ Eq (α := PresentedGroup rels) ((mk rels : (a : FreeGroup α) → PresentedGroup rels) x : PresentedGroup rels)
    ((mk rels : (a : FreeGroup α) → PresentedGroup rels) y : PresentedGroup rels)

Tactic:
eq_of_mul_inv_eq_one <| one_of_mem hx

Premises used: eq_of_mul_inv_eq_one, PresentedGroup.one_of_mem
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
rels : Set (FreeGroup α)
x y : FreeGroup α
hx : x⁻¹ * y ∈ rels
⊢ Eq (α := PresentedGroup rels) ((mk rels : (a : FreeGroup α) → PresentedGroup rels) x : PresentedGroup rels)
    ((mk rels : (a : FreeGroup α) → PresentedGroup rels) y : PresentedGroup rels)

Tactic:
eq_of_inv_mul_eq_one <| one_of_mem hx

Premises used: eq_of_inv_mul_eq_one, PresentedGroup.one_of_mem
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
rels : Set (FreeGroup α)
⊢ Eq (α := (x : α) → PresentedGroup rels) (of (rels := rels))
    ((⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) :
        (a : FreeGroup α) → FreeGroup α ⧸ Subgroup.normalClosure rels) ∘
      FreeGroup.of)

Tactic:
have : (PresentedGroup.of : α → PresentedGroup rels) = QuotientGroup.mk' _ ∘ FreeGroup.of := rfl
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
rels : Set (FreeGroup α)
this :
  Eq (α := (x : α) → PresentedGroup rels) (of (rels := rels))
    ((⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) :
        (a : FreeGroup α) → FreeGroup α ⧸ Subgroup.normalClosure rels) ∘
      FreeGroup.of)
rw : Eq (α := Subgroup (PresentedGroup rels)) (MonoidHom.range (QuotientGroup.mk' (Subgroup.normalClosure rels))) ⊤
⊢ Eq.{u_1 + 1} (α := Subgroup (PresentedGroup rels)) (Subgroup.closure (Set.range (of (rels := rels)))) ⊤

Tactic:
rw [this, Set.range_comp, ← MonoidHom.map_closure (QuotientGroup.mk' _),
    FreeGroup.closure_range_of, ← MonoidHom.range_eq_map]

Premises used: Set.range_comp, FreeGroup.closure_range_of, MonoidHom.range_eq_map, MonoidHom.map_closure, QuotientGroup.mk'
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
rels : Set (FreeGroup α)
this :
  Eq (α := (x : α) → PresentedGroup rels) (of (rels := rels))
    ((⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) :
        (a : FreeGroup α) → FreeGroup α ⧸ Subgroup.normalClosure rels) ∘
      FreeGroup.of)
⊢ Eq (α := Subgroup (PresentedGroup rels)) (MonoidHom.range (QuotientGroup.mk' (Subgroup.normalClosure rels))) ⊤

Tactic:
MonoidHom.range_eq_top.2 (QuotientGroup.mk'_surjective _)

Premises used: PresentedGroup, Iff.mpr, MonoidHom.range_eq_top, QuotientGroup.mk'_surjective
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
rels : Set (FreeGroup α)
this :
  Eq (α := (x : α) → PresentedGroup rels) (of (rels := rels))
    ((⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) :
        (a : FreeGroup α) → FreeGroup α ⧸ Subgroup.normalClosure rels) ∘
      FreeGroup.of)
⊢ Eq (α := Subgroup (PresentedGroup rels)) (MonoidHom.range (QuotientGroup.mk' (Subgroup.normalClosure rels))) ⊤

Tactic:
exact MonoidHom.range_eq_top.2 (QuotientGroup.mk'_surjective _)

Premises used: Iff.mpr, MonoidHom.range_eq_top, QuotientGroup.mk'_surjective
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
rels : Set (FreeGroup α)
C : PresentedGroup rels → Prop
x : PresentedGroup rels
H : ∀ (z : FreeGroup α), C ((mk rels : (a : FreeGroup α) → PresentedGroup rels) z)
⊢ C x

Tactic:
Quotient.inductionOn' x H

Premises used: Quotient.inductionOn'
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of (rels := rels) j ∈ H
x : PresentedGroup rels
mk :
  ∀ (z : FreeGroup α),
    Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) z ∈ H
⊢ x ∈ H

Tactic:
obtain ⟨z⟩ := x
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of (rels := rels) j ∈ H
x : PresentedGroup rels
z : FreeGroup α
mk : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) 1 ∈ H
mk₁ :
  ∀ (x : α),
    Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop)
        (FreeGroup.of x) ∈
      H
mk₂ :
  ∀ (x : α),
    Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop)
          (FreeGroup.of x) ∈
        H →
      Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop)
          (FreeGroup.of x)⁻¹ ∈
        H
mk₃ :
  ∀ (x y : FreeGroup α),
    Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) x ∈ H →
      Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) y ∈ H →
        Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) (x * y) ∈ H
⊢ Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) z ∈ H

Tactic:
induction z
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of (rels := rels) j ∈ H
x : PresentedGroup rels
⊢ Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) 1 ∈ H

Tactic:
one_mem H

Premises used: Set.Mem, OneMemClass.one_mem
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of (rels := rels) j ∈ H
x : PresentedGroup rels
⊢ Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) 1 ∈ H

Tactic:
exact one_mem H

Premises used: OneMemClass.one_mem
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of (rels := rels) j ∈ H
x : PresentedGroup rels
x_1 : α
⊢ Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop)
      (FreeGroup.of x_1) ∈
    H

Tactic:
h _

Premises used: PresentedGroup.of, Set.Mem
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of (rels := rels) j ∈ H
x : PresentedGroup rels
x_1 : α
⊢ Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop)
      (FreeGroup.of x_1) ∈
    H

Tactic:
exact h _
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of (rels := rels) j ∈ H
x : PresentedGroup rels
x_1 : α
h_1 :
  Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop)
      (FreeGroup.of x_1) ∈
    H
⊢ Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop)
      (FreeGroup.of x_1) ∈
    H

Tactic:
assumption
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of (rels := rels) j ∈ H
x : PresentedGroup rels
x_1 : α
h_1 :
  Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop)
      (FreeGroup.of x_1) ∈
    H
⊢ Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop)
      (FreeGroup.of x_1)⁻¹ ∈
    H

Tactic:
exact (Subgroup.inv_mem_iff H).mpr (by assumption)

Premises used: Iff.mpr, Subgroup.inv_mem_iff
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of (rels := rels) j ∈ H
x : PresentedGroup rels
x_1 y : FreeGroup α
h1 : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) x_1 ∈ H
h2 : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) y ∈ H
mk : (↑(x_1 * y) : FreeGroup α ⧸ Subgroup.normalClosure rels) ∈ H.carrier
⊢ Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) (x_1 * y) ∈ H

Tactic:
change QuotientGroup.mk _ ∈ H.carrier

Premises used: QuotientGroup.mk, Submonoid.toSubsemigroup, Subsemigroup.carrier, Subgroup.toSubmonoid
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of (rels := rels) j ∈ H
x : PresentedGroup rels
x_1 y : FreeGroup α
h1 : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) x_1 ∈ H
h2 : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) y ∈ H
mk :
  HMul.hMul (α := HasQuotient.Quotient (FreeGroup α) (B := Subgroup (FreeGroup α)) (Subgroup.normalClosure rels))
      (↑x_1 : FreeGroup α ⧸ Subgroup.normalClosure rels) (↑y : FreeGroup α ⧸ Subgroup.normalClosure rels) ∈
    H.carrier
⊢ (↑(x_1 * y) : FreeGroup α ⧸ Subgroup.normalClosure rels) ∈ H.carrier

Tactic:
rw [QuotientGroup.mk_mul]

Premises used: QuotientGroup.mk_mul
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of (rels := rels) j ∈ H
x : PresentedGroup rels
x_1 y : FreeGroup α
h1 : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) x_1 ∈ H
h2 : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) y ∈ H
⊢ HMul.hMul (α := HasQuotient.Quotient (FreeGroup α) (B := Subgroup (FreeGroup α)) (Subgroup.normalClosure rels))
      (↑x_1 : FreeGroup α ⧸ Subgroup.normalClosure rels) (↑y : FreeGroup α ⧸ Subgroup.normalClosure rels) ∈
    H.carrier

Tactic:
Subgroup.mul_mem _ h1 h2

Premises used: Set.Mem, Subgroup.mul_mem
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of (rels := rels) j ∈ H
x : PresentedGroup rels
x_1 y : FreeGroup α
h1 : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) x_1 ∈ H
h2 : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels)) : FreeGroup α → FreeGroup α → Prop) y ∈ H
⊢ HMul.hMul (α := HasQuotient.Quotient (FreeGroup α) (B := Subgroup (FreeGroup α)) (Subgroup.normalClosure rels))
      (↑x_1 : FreeGroup α ⧸ Subgroup.normalClosure rels) (↑y : FreeGroup α ⧸ Subgroup.normalClosure rels) ∈
    H.carrier

Tactic:
exact Subgroup.mul_mem _ h1 h2

Premises used: Subgroup.mul_mem
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
G : Type u_3
inst : Group G
f : α → G
rels : Set (FreeGroup α)
h :
  ∀ r ∈ rels,
    Eq.{u_3 + 1} (α := G)
      ((((FreeGroup.lift : (a : α → G) → FreeGroup α →* G) f : MonoidHom.{u_1, u_3} (FreeGroup α) G) :
            (a : FreeGroup α) → G)
          r :
        G)
      (1 : G)
⊢ LE.le (α := Subgroup (FreeGroup α)) (Subgroup.normalClosure rels)
    (MonoidHom.ker.{u_1, u_3} (M := G) ((FreeGroup.lift : (a : α → G) → FreeGroup α →* G) f))

Tactic:
Subgroup.normalClosure_le_normal fun x w ↦ MonoidHom.mem_ker.2 (h x w)

Premises used: Iff.mpr, MonoidHom.mem_ker, Subgroup.normalClosure_le_normal
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
G : Type u_3
inst : Group G
f : α → G
rels : Set (FreeGroup α)
h :
  ∀ r ∈ rels,
    Eq.{u_3 + 1} (α := G)
      ((((FreeGroup.lift : (a : α → G) → FreeGroup α →* G) f : MonoidHom.{u_1, u_3} (FreeGroup α) G) :
            (a : FreeGroup α) → G)
          r :
        G)
      (1 : G)
⊢ ∀ (x : FreeGroup α),
    Membership.mem (γ := Subgroup (FreeGroup α)) (Subgroup.normalClosure rels) x →
      Eq.{u_3 + 1} (α := G)
        ((((FreeGroup.lift : (a : α → G) → FreeGroup α →* G) f : MonoidHom.{u_1, u_3} (FreeGroup α) G) :
              (a : FreeGroup α) → G)
            x :
          G)
        (1 : G)

Tactic:
fun _ w ↦ MonoidHom.mem_ker.1 <| closure_rels_subset_ker h w

Premises used: PresentedGroup.closure_rels_subset_ker, MonoidHom.mem_ker, Iff.mp
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
G : Type u_3
inst : Group G
f : α → G
rels : Set (FreeGroup α)
h :
  ∀ r ∈ rels,
    Eq.{u_3 + 1} (α := G)
      ((((FreeGroup.lift : (a : α → G) → FreeGroup α →* G) f : MonoidHom.{u_1, u_3} (FreeGroup α) G) :
            (a : FreeGroup α) → G)
          r :
        G)
      (1 : G)
x : α
⊢ (toGroup (rels := rels) h : (a : PresentedGroup rels) → G) (PresentedGroup.of (rels := rels) x) = f x

Tactic:
FreeGroup.lift_apply_of

Premises used: Quotient.liftOn', FreeGroup.lift_apply_of, FreeGroup.Lift.aux, Con.liftOn, List.foldr, List.prod
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
G : Type u_3
inst : Group G
f : α → G
rels : Set (FreeGroup α)
h :
  ∀ r ∈ rels,
    Eq.{u_3 + 1} (α := G)
      ((((FreeGroup.lift : (a : α → G) → FreeGroup α →* G) f : MonoidHom.{u_1, u_3} (FreeGroup α) G) :
            (a : FreeGroup α) → G)
          r :
        G)
      (1 : G)
g : MonoidHom.{u_1, u_3} (PresentedGroup rels) G
hg : ∀ (x : α), (g : (a : PresentedGroup rels) → G) (PresentedGroup.of (rels := rels) x) = f x
x : PresentedGroup rels
⊢ Eq.{u_3 + 1} (α := G) ((g : (a : PresentedGroup rels) → G) x : G)
    ((toGroup (rels := rels) h : (a : PresentedGroup rels) → G) x : G)

Tactic:
QuotientGroup.induction_on x ?_

Premises used: QuotientGroup.induction_on
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
G : Type u_3
inst : Group G
f : α → G
rels : Set (FreeGroup α)
h :
  ∀ r ∈ rels,
    Eq.{u_3 + 1} (α := G)
      ((((FreeGroup.lift : (a : α → G) → FreeGroup α →* G) f : MonoidHom.{u_1, u_3} (FreeGroup α) G) :
            (a : FreeGroup α) → G)
          r :
        G)
      (1 : G)
g : MonoidHom.{u_1, u_3} (PresentedGroup rels) G
hg : ∀ (x : α), (g : (a : PresentedGroup rels) → G) (PresentedGroup.of (rels := rels) x) = f x
x : PresentedGroup rels
refine :
  ∀ (z : FreeGroup α),
    Eq.{u_3 + 1} (α := G) ((g : (a : PresentedGroup rels) → G) (↑z : FreeGroup α ⧸ Subgroup.normalClosure rels) : G)
      ((toGroup (rels := rels) h : (a : PresentedGroup rels) → G) (↑z : FreeGroup α ⧸ Subgroup.normalClosure rels) : G)
⊢ Eq.{u_3 + 1} (α := G) ((g : (a : PresentedGroup rels) → G) x : G)
    ((toGroup (rels := rels) h : (a : PresentedGroup rels) → G) x : G)

Tactic:
refine QuotientGroup.induction_on x ?_
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
G : Type u_3
inst : Group G
f : α → G
rels : Set (FreeGroup α)
h :
  ∀ r ∈ rels,
    Eq.{u_3 + 1} (α := G)
      ((((FreeGroup.lift : (a : α → G) → FreeGroup α →* G) f : MonoidHom.{u_1, u_3} (FreeGroup α) G) :
            (a : FreeGroup α) → G)
          r :
        G)
      (1 : G)
g : MonoidHom.{u_1, u_3} (PresentedGroup rels) G
hg : ∀ (x : α), (g : (a : PresentedGroup rels) → G) (PresentedGroup.of (rels := rels) x) = f x
x : PresentedGroup rels
⊢ ∀ (z : FreeGroup α),
    Eq.{u_3 + 1} (α := G) ((g : (a : PresentedGroup rels) → G) (↑z : FreeGroup α ⧸ Subgroup.normalClosure rels) : G)
      ((toGroup (rels := rels) h : (a : PresentedGroup rels) → G) (↑z : FreeGroup α ⧸ Subgroup.normalClosure rels) : G)

Tactic:
fun _ ↦ FreeGroup.lift_unique (g.comp (QuotientGroup.mk' _)) hg

Premises used: Quotient.liftOn', Subgroup.normalClosure, FreeGroup.lift_unique, MonoidHom.comp, QuotientGroup.mk', Con.liftOn
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
G : Type u_3
inst : Group G
f : α → G
rels : Set (FreeGroup α)
h :
  ∀ r ∈ rels,
    Eq.{u_3 + 1} (α := G)
      ((((FreeGroup.lift : (a : α → G) → FreeGroup α →* G) f : MonoidHom.{u_1, u_3} (FreeGroup α) G) :
            (a : FreeGroup α) → G)
          r :
        G)
      (1 : G)
g : MonoidHom.{u_1, u_3} (PresentedGroup rels) G
hg : ∀ (x : α), (g : (a : PresentedGroup rels) → G) (PresentedGroup.of (rels := rels) x) = f x
x : PresentedGroup rels
⊢ ∀ (z : FreeGroup α),
    Eq.{u_3 + 1} (α := G) ((g : (a : PresentedGroup rels) → G) (↑z : FreeGroup α ⧸ Subgroup.normalClosure rels) : G)
      ((toGroup (rels := rels) h : (a : PresentedGroup rels) → G) (↑z : FreeGroup α ⧸ Subgroup.normalClosure rels) : G)

Tactic:
exact fun _ ↦ FreeGroup.lift_unique (g.comp (QuotientGroup.mk' _)) hg

Premises used: Subgroup.normalClosure, FreeGroup.lift_unique, MonoidHom.comp, QuotientGroup.mk'
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
G : Type u_3
inst : Group G
rels : Set (FreeGroup α)
φ ψ : MonoidHom.{u_1, u_3} (PresentedGroup rels) G
hx :
  ∀ (x : α),
    Eq.{u_3 + 1} (α := G) ((φ : (a : PresentedGroup rels) → G) (of (rels := rels) x) : G)
      ((ψ : (a : PresentedGroup rels) → G) (of (rels := rels) x) : G)
h :
  ∀ (a : α),
    Eq.{u_3 + 1} (α := G)
      ((φ.comp (QuotientGroup.mk' (Subgroup.normalClosure rels)) : (a : FreeGroup α) → G) (FreeGroup.of a) : G)
      ((ψ.comp (QuotientGroup.mk' (Subgroup.normalClosure rels)) : (a : FreeGroup α) → G) (FreeGroup.of a) : G)
⊢ φ = ψ

Tactic:
ext
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
G : Type u_3
inst : Group G
rels : Set (FreeGroup α)
φ ψ : MonoidHom.{u_1, u_3} (PresentedGroup rels) G
hx :
  ∀ (x : α),
    Eq.{u_3 + 1} (α := G) ((φ : (a : PresentedGroup rels) → G) (of (rels := rels) x) : G)
      ((ψ : (a : PresentedGroup rels) → G) (of (rels := rels) x) : G)
a : α
⊢ Eq.{u_3 + 1} (α := G)
    ((φ.comp (QuotientGroup.mk' (Subgroup.normalClosure rels)) : (a : FreeGroup α) → G) (FreeGroup.of a) : G)
    ((ψ.comp (QuotientGroup.mk' (Subgroup.normalClosure rels)) : (a : FreeGroup α) → G) (FreeGroup.of a) : G)

Tactic:
apply hx
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
β : Type u_2
x : α
rels : Set (FreeGroup α)
e : α ≃ β
⊢ Eq.{u_2 + 1} (α :=
    PresentedGroup (α := β) ((⇑(FreeGroup.freeGroupCongr e) : (a : FreeGroup α) → FreeGroup β) '' rels))
    ((equivPresentedGroup rels e :
          (a : PresentedGroup rels) →
            PresentedGroup ((⇑(FreeGroup.freeGroupCongr e) : (a : FreeGroup α) → FreeGroup β) '' rels))
        (of (rels := rels) x) :
      PresentedGroup (α := β) ((⇑(FreeGroup.freeGroupCongr e) : (a : FreeGroup α) → FreeGroup β) '' rels))
    (of (rels := (⇑(FreeGroup.freeGroupCongr e) : (a : FreeGroup α) → FreeGroup β) '' rels) ((e : (a : α) → β) x) :
      PresentedGroup (α := β) ((⇑(FreeGroup.freeGroupCongr e) : (a : FreeGroup α) → FreeGroup β) '' rels))

Tactic:
rfl

Premises used: FreeGroup.of, Quotient.liftOn', PresentedGroup.of, List.map, Con.liftOn, FreeGroup.mk, Quot.map, rfl
-- Module: Mathlib.GroupTheory.PresentedGroup
Goal:
α : Type u_1
β : Type u_2
x : β
rels : Set (FreeGroup α)
e : α ≃ β
⊢ Eq.{u_1 + 1} (α := PresentedGroup rels)
    (((equivPresentedGroup rels e).symm :
          (a : PresentedGroup ((⇑(FreeGroup.freeGroupCongr e) : (a : FreeGroup α) → FreeGroup β) '' rels)) →
            PresentedGroup rels)
        (of (rels := (⇑(FreeGroup.freeGroupCongr e) : (a : FreeGroup α) → FreeGroup β) '' rels) x) :
      PresentedGroup rels)
    (of (rels := rels) ((e.symm : (a : β) → α) x) : PresentedGroup rels)

Tactic:
rfl

Premises used: FreeGroup.of, Quotient.liftOn', PresentedGroup.of, List.map, Con.liftOn, FreeGroup.mk, Quot.map, rfl