no goals
G : Type u_1
H : Type ?u.52507
A : Type ?u.52510
a a₁ a₂ b c : G
inst✝ : Group G
s : Set G
⊢ 1 ∈ normalizer s
simp [normalizer]
no goals
G : Type u_1
H : Type ?u.52507
A : Type ?u.52510
a✝ a₁ a₂ b✝ c : G
inst✝ : Group G
s : Set G
a b : G
ha : ∀ (n : G), n ∈ s ↔ a * n * a⁻¹ ∈ s
hb : ∀ (n : G), n ∈ s ↔ b * n * b⁻¹ ∈ s
n : G
⊢ n ∈ s ↔ a * b * n * (a * b)⁻¹ ∈ s
rw [mul_inv_rev, ← mul_assoc, mul_assoc a, mul_assoc a, ← ha, ← hb]
G : Type u_1
H : Type ?u.52507
A : Type ?u.52510
a✝ a₁ a₂ b c : G
inst✝ : Group G
s : Set G
a : G
ha : ∀ (n : G), n ∈ s ↔ a * n * a⁻¹ ∈ s
n : G
⊢ n ∈ s ↔ a * (a⁻¹ * n * a⁻¹⁻¹) * a⁻¹ ∈ s
G : Type u_1
H : Type ?u.52507
A : Type ?u.52510
a✝ a₁ a₂ b c : G
inst✝ : Group G
s : Set G
a : G
ha : ∀ (n : G), n ∈ s ↔ a * n * a⁻¹ ∈ s
n : G
⊢ n ∈ s ↔ a⁻¹ * n * a⁻¹⁻¹ ∈ s
rw [ha (a⁻¹ * n * a⁻¹⁻¹)]
no goals
G : Type u_1
H : Type ?u.52507
A : Type ?u.52510
a✝ a₁ a₂ b c : G
inst✝ : Group G
s : Set G
a : G
ha : ∀ (n : G), n ∈ s ↔ a * n * a⁻¹ ∈ s
n : G
⊢ n ∈ s ↔ a * (a⁻¹ * n * a⁻¹⁻¹) * a⁻¹ ∈ s
simp [mul_assoc]