case intro.intro
G : Type u_1
G' : Type ?u.436568
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.436577
inst✝ : AddGroup A
s : Set G
x c : G
H : x ∈ conjugatesOfSet s
a : G
h₁ : a ∈ s
h₂ : IsConj a x
⊢ c * x * c⁻¹ ∈ conjugatesOfSet s
G : Type u_1
G' : Type ?u.436568
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.436577
inst✝ : AddGroup A
s : Set G
x c : G
H : x ∈ conjugatesOfSet s
⊢ c * x * c⁻¹ ∈ conjugatesOfSet s
rcases mem_conjugatesOfSet_iff.1 H with ⟨a, h₁, h₂⟩
no goals
case intro.intro
G : Type u_1
G' : Type ?u.436568
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.436577
inst✝ : AddGroup A
s : Set G
x c : G
H : x ∈ conjugatesOfSet s
a : G
h₁ : a ∈ s
h₂ : IsConj a x
⊢ c * x * c⁻¹ ∈ conjugatesOfSet s
exact mem_conjugatesOfSet_iff.2 ⟨a, h₁, h₂.trans (isConj_iff.2 ⟨c, rfl⟩)⟩