-- Mathlib/GroupTheory/PresentedGroup.lean
theorem generated_by (rels : Set (FreeGroup α)) (H : Subgroup (PresentedGroup rels))
    (h : ∀ j : α, PresentedGroup.of j ∈ H) (x : PresentedGroup rels) : x ∈ H

Proof state:
case H.Cm
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x✝ y✝ : FreeGroup α
a✝¹ : (mk rels) x✝ ∈ H
a✝ : (mk rels) y✝ ∈ H
⊢ (mk rels) (x✝ * y✝) ∈ H

Tactic:
rename_i h1 h2

Result:
case H.Cm
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x✝ y✝ : FreeGroup α
h1 : (mk rels) x✝ ∈ H
h2 : (mk rels) y✝ ∈ H
⊢ (mk rels) (x✝ * y✝) ∈ H

Proof state:
case H.Cp
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x✝ : α
⊢ (mk rels) (pure x✝) ∈ H

Tactic:
exact h _

Result:
no goals

Proof state:
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x✝ : α
a✝ : (mk rels) (pure x✝) ∈ H
⊢ ?m.4389 ∈ H

Tactic:
assumption

Result:
no goals

Proof state:
case H.Ci
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x✝ : α
a✝ : (mk rels) (pure x✝) ∈ H
⊢ (mk rels) (pure x✝)⁻¹ ∈ H

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

Result:
no goals

Proof state:
case H.Cm
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x✝ y✝ : FreeGroup α
h1 : (mk rels) x✝ ∈ H
h2 : (mk rels) y✝ ∈ H
⊢ ↑x✝ * ↑y✝ ∈ H.carrier

Tactic:
exact Subgroup.mul_mem _ h1 h2

Result:
no goals

Proof state:
case H
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
z : FreeGroup α
⊢ (mk rels) z ∈ H

Tactic:
induction z

Result:
case H.C1
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
⊢ (mk rels) 1 ∈ H

case H.Cp
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x✝ : α
⊢ (mk rels) (pure x✝) ∈ H

case H.Ci
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x✝ : α
a✝ : (mk rels) (pure x✝) ∈ H
⊢ (mk rels) (pure x✝)⁻¹ ∈ H

case H.Cm
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x✝ y✝ : FreeGroup α
a✝¹ : (mk rels) x✝ ∈ H
a✝ : (mk rels) y✝ ∈ H
⊢ (mk rels) (x✝ * y✝) ∈ H

Proof state:
case H.Cm
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x✝ y✝ : FreeGroup α
h1 : (mk rels) x✝ ∈ H
h2 : (mk rels) y✝ ∈ H
⊢ ↑(x✝ * y✝) ∈ H.carrier

Tactic:
rw [QuotientGroup.mk_mul]

Result:
case H.Cm
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x✝ y✝ : FreeGroup α
h1 : (mk rels) x✝ ∈ H
h2 : (mk rels) y✝ ∈ H
⊢ ↑x✝ * ↑y✝ ∈ H.carrier

Proof state:
case H.C1
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
⊢ (mk rels) 1 ∈ H

Tactic:
exact one_mem H

Result:
no goals

Proof state:
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x : PresentedGroup rels
⊢ x ∈ H

Tactic:
induction' x with z

Result:
case H
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
z : FreeGroup α
⊢ (mk rels) z ∈ H

Proof state:
case H.Cm
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x✝ y✝ : FreeGroup α
h1 : (mk rels) x✝ ∈ H
h2 : (mk rels) y✝ ∈ H
⊢ (mk rels) (x✝ * y✝) ∈ H

Tactic:
change QuotientGroup.mk _ ∈ H.carrier

Result:
case H.Cm
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x✝ y✝ : FreeGroup α
h1 : (mk rels) x✝ ∈ H
h2 : (mk rels) y✝ ∈ H
⊢ ↑(x✝ * y✝) ∈ H.carrier