G : Type u_1
G' : Type ?u.435622
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.435631
inst✝ : AddGroup A
s : Set G
N : Subgroup G
tn : Subgroup.Normal N
a✝ : G
h : a✝ ∈ N
a : G
hc : a ∈ conjugatesOf a✝
⊢ a ∈ ↑N
G : Type u_1
G' : Type ?u.435622
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.435631
inst✝ : AddGroup A
s : Set G
N : Subgroup G
tn : Subgroup.Normal N
a : G
h : a ∈ N
⊢ conjugatesOf a ⊆ ↑N
rintro a hc
case intro
G : Type u_1
G' : Type ?u.435622
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.435631
inst✝ : AddGroup A
s : Set G
N : Subgroup G
tn : Subgroup.Normal N
a : G
h : a ∈ N
c : G
hc : c * a * c⁻¹ ∈ conjugatesOf a
⊢ c * a * c⁻¹ ∈ ↑N
G : Type u_1
G' : Type ?u.435622
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.435631
inst✝ : AddGroup A
s : Set G
N : Subgroup G
tn : Subgroup.Normal N
a✝ : G
h : a✝ ∈ N
a : G
hc : a ∈ conjugatesOf a✝
⊢ a ∈ ↑N
obtain ⟨c, rfl⟩ := isConj_iff.1 hc
no goals
case intro
G : Type u_1
G' : Type ?u.435622
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.435631
inst✝ : AddGroup A
s : Set G
N : Subgroup G
tn : Subgroup.Normal N
a : G
h : a ∈ N
c : G
hc : c * a * c⁻¹ ∈ conjugatesOf a
⊢ c * a * c⁻¹ ∈ ↑N
exact tn.conj_mem a h c