case basic
G : Type u_1
H : Type ?u.145368
A : Type ?u.145371
a✝ a₁ a₂ b c : G
s✝ : Set G
inst✝ : Group G
s t : Set G
ht : IsNormalSubgroup t
h : s ⊆ t
a x : G
hx : x ∈ conjugatesOfSet s
⊢ x ∈ t

case one
G : Type u_1
H : Type ?u.145368
A : Type ?u.145371
a✝ a₁ a₂ b c : G
s✝ : Set G
inst✝ : Group G
s t : Set G
ht : IsNormalSubgroup t
h : s ⊆ t
a : G
⊢ 1 ∈ t

case inv
G : Type u_1
H : Type ?u.145368
A : Type ?u.145371
a✝¹ a₁ a₂ b c : G
s✝ : Set G
inst✝ : Group G
s t : Set G
ht : IsNormalSubgroup t
h : s ⊆ t
a x : G
a✝ : InClosure (conjugatesOfSet s) x
ihx : x ∈ t
⊢ x⁻¹ ∈ t

case mul
G : Type u_1
H : Type ?u.145368
A : Type ?u.145371
a✝² a₁ a₂ b c : G
s✝ : Set G
inst✝ : Group G
s t : Set G
ht : IsNormalSubgroup t
h : s ⊆ t
a x y : G
a✝¹ : InClosure (conjugatesOfSet s) x
a✝ : InClosure (conjugatesOfSet s) y
ihx : x ∈ t
ihy : y ∈ t
⊢ x * y ∈ t
G : Type u_1
H : Type ?u.145368
A : Type ?u.145371
a✝ a₁ a₂ b c : G
s✝ : Set G
inst✝ : Group G
s t : Set G
ht : IsNormalSubgroup t
h : s ⊆ t
a : G
w : a ∈ normalClosure s
⊢ a ∈ t
induction' w with x hx x _ ihx x y _ _ ihx ihy
no goals
case basic
G : Type u_1
H : Type ?u.145368
A : Type ?u.145371
a✝ a₁ a₂ b c : G
s✝ : Set G
inst✝ : Group G
s t : Set G
ht : IsNormalSubgroup t
h : s ⊆ t
a x : G
hx : x ∈ conjugatesOfSet s
⊢ x ∈ t
exact conjugatesOfSet_subset' ht h <| hx
no goals
case one
G : Type u_1
H : Type ?u.145368
A : Type ?u.145371
a✝ a₁ a₂ b c : G
s✝ : Set G
inst✝ : Group G
s t : Set G
ht : IsNormalSubgroup t
h : s ⊆ t
a : G
⊢ 1 ∈ t
exact ht.toIsSubgroup.toIsSubmonoid.one_mem
no goals
case inv
G : Type u_1
H : Type ?u.145368
A : Type ?u.145371
a✝¹ a₁ a₂ b c : G
s✝ : Set G
inst✝ : Group G
s t : Set G
ht : IsNormalSubgroup t
h : s ⊆ t
a x : G
a✝ : InClosure (conjugatesOfSet s) x
ihx : x ∈ t
⊢ x⁻¹ ∈ t
exact ht.toIsSubgroup.inv_mem ihx
no goals
case mul
G : Type u_1
H : Type ?u.145368
A : Type ?u.145371
a✝² a₁ a₂ b c : G
s✝ : Set G
inst✝ : Group G
s t : Set G
ht : IsNormalSubgroup t
h : s ⊆ t
a x y : G
a✝¹ : InClosure (conjugatesOfSet s) x
a✝ : InClosure (conjugatesOfSet s) y
ihx : x ∈ t
ihy : y ∈ t
⊢ x * y ∈ t
exact ht.toIsSubgroup.toIsSubmonoid.mul_mem ihx ihy