case h
G : Type u_1
G' : Type ?u.627985
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.627994
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ : G →* N
H : Subgroup G
f : G ≃* N
x : N
⊢ x ∈ map (MulEquiv.toMonoidHom f) (normalizer H) ↔ x ∈ normalizer (map (MulEquiv.toMonoidHom f) H)
G : Type u_1
G' : Type ?u.627985
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.627994
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ : G →* N
H : Subgroup G
f : G ≃* N
⊢ map (MulEquiv.toMonoidHom f) (normalizer H) = normalizer (map (MulEquiv.toMonoidHom f) H)
ext x
case h
G : Type u_1
G' : Type ?u.627985
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.627994
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ : G →* N
H : Subgroup G
f : G ≃* N
x : N
⊢ (∀ (h : G), h ∈ H ↔ ↑(MulEquiv.symm f) x * h * (↑(MulEquiv.symm f) x)⁻¹ ∈ H) ↔
    ∀ (h : N), ↑(MulEquiv.symm f) h ∈ H ↔ ↑(MulEquiv.symm f) (x * h * x⁻¹) ∈ H
case h
G : Type u_1
G' : Type ?u.627985
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.627994
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ : G →* N
H : Subgroup G
f : G ≃* N
x : N
⊢ x ∈ map (MulEquiv.toMonoidHom f) (normalizer H) ↔ x ∈ normalizer (map (MulEquiv.toMonoidHom f) H)
simp only [mem_normalizer_iff, mem_map_equiv]
case h
G : Type u_1
G' : Type ?u.627985
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.627994
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ : G →* N
H : Subgroup G
f : G ≃* N
x : N
⊢ ∀ {x_1 : G},
    (x_1 ∈ H ↔ ↑(MulEquiv.symm f) x * x_1 * (↑(MulEquiv.symm f) x)⁻¹ ∈ H) ↔
      (↑(MulEquiv.symm f) (↑f.toEquiv x_1) ∈ H ↔ ↑(MulEquiv.symm f) (x * ↑f.toEquiv x_1 * x⁻¹) ∈ H)
case h
G : Type u_1
G' : Type ?u.627985
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.627994
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ : G →* N
H : Subgroup G
f : G ≃* N
x : N
⊢ (∀ (h : G), h ∈ H ↔ ↑(MulEquiv.symm f) x * h * (↑(MulEquiv.symm f) x)⁻¹ ∈ H) ↔
    ∀ (h : N), ↑(MulEquiv.symm f) h ∈ H ↔ ↑(MulEquiv.symm f) (x * h * x⁻¹) ∈ H
rw [f.toEquiv.forall_congr]
case h
G : Type u_1
G' : Type ?u.627985
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.627994
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ : G →* N
H : Subgroup G
f : G ≃* N
x : N
x✝ : G
⊢ (x✝ ∈ H ↔ ↑(MulEquiv.symm f) x * x✝ * (↑(MulEquiv.symm f) x)⁻¹ ∈ H) ↔
    (↑(MulEquiv.symm f) (↑f.toEquiv x✝) ∈ H ↔ ↑(MulEquiv.symm f) (x * ↑f.toEquiv x✝ * x⁻¹) ∈ H)
case h
G : Type u_1
G' : Type ?u.627985
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.627994
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ : G →* N
H : Subgroup G
f : G ≃* N
x : N
⊢ ∀ {x_1 : G},
    (x_1 ∈ H ↔ ↑(MulEquiv.symm f) x * x_1 * (↑(MulEquiv.symm f) x)⁻¹ ∈ H) ↔
      (↑(MulEquiv.symm f) (↑f.toEquiv x_1) ∈ H ↔ ↑(MulEquiv.symm f) (x * ↑f.toEquiv x_1 * x⁻¹) ∈ H)
intro
case h
G : Type u_1
G' : Type ?u.627985
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.627994
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ : G →* N
H : Subgroup G
f : G ≃* N
x : N
x✝ : G
⊢ (x✝ ∈ H ↔ ↑(MulEquiv.symm f) x * x✝ * (↑(MulEquiv.symm f) x)⁻¹ ∈ H) ↔
    (x✝ ∈ H ↔ ↑(MulEquiv.symm f) (x * ↑f.toEquiv x✝ * x⁻¹) ∈ H)
case h
G : Type u_1
G' : Type ?u.627985
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.627994
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ : G →* N
H : Subgroup G
f : G ≃* N
x : N
x✝ : G
⊢ (x✝ ∈ H ↔ ↑(MulEquiv.symm f) x * x✝ * (↑(MulEquiv.symm f) x)⁻¹ ∈ H) ↔
    (↑(MulEquiv.symm f) (↑f.toEquiv x✝) ∈ H ↔ ↑(MulEquiv.symm f) (x * ↑f.toEquiv x✝ * x⁻¹) ∈ H)
erw [f.toEquiv.symm_apply_apply]
case h
G : Type u_1
G' : Type ?u.627985
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.627994
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ : G →* N
H : Subgroup G
f : G ≃* N
x : N
x✝ : G
⊢ (x✝ ∈ H ↔ ↑(MulEquiv.symm f) x * x✝ * (↑(MulEquiv.symm f) x)⁻¹ ∈ H) ↔
    (x✝ ∈ H ↔ ↑(MulEquiv.symm f) x * ↑(MulEquiv.symm f) (↑f.toEquiv x✝) * (↑(MulEquiv.symm f) x)⁻¹ ∈ H)
case h
G : Type u_1
G' : Type ?u.627985
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.627994
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ : G →* N
H : Subgroup G
f : G ≃* N
x : N
x✝ : G
⊢ (x✝ ∈ H ↔ ↑(MulEquiv.symm f) x * x✝ * (↑(MulEquiv.symm f) x)⁻¹ ∈ H) ↔
    (x✝ ∈ H ↔ ↑(MulEquiv.symm f) (x * ↑f.toEquiv x✝ * x⁻¹) ∈ H)
simp only [map_mul, map_inv]
no goals
case h
G : Type u_1
G' : Type ?u.627985
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.627994
inst✝¹ : AddGroup A
N : Type u_2
inst✝ : Group N
f✝ : G →* N
H : Subgroup G
f : G ≃* N
x : N
x✝ : G
⊢ (x✝ ∈ H ↔ ↑(MulEquiv.symm f) x * x✝ * (↑(MulEquiv.symm f) x)⁻¹ ∈ H) ↔
    (x✝ ∈ H ↔ ↑(MulEquiv.symm f) x * ↑(MulEquiv.symm f) (↑f.toEquiv x✝) * (↑(MulEquiv.symm f) x)⁻¹ ∈ H)
erw [f.toEquiv.symm_apply_apply]