G : Type u_1
G' : Type ?u.395731
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.395740
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_2
inst✝ : Group N
f : G →* N
x✝ : N
⊢ ∀ (x : G),
    (∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H) →
      ↑f x = x✝ → ∀ (h : N), (∃ x, x ∈ H ∧ ↑f x = h) ↔ ∃ x, x ∈ H ∧ ↑f x = x✝ * h * x✝⁻¹
G : Type u_1
G' : Type ?u.395731
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.395740
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_2
inst✝ : Group N
f : G →* N
x✝ : N
⊢ x✝ ∈ map f (normalizer H) → x✝ ∈ normalizer (map f H)
simp only [and_imp, exists_prop, mem_map, exists_imp, mem_normalizer_iff]
G : Type u_1
G' : Type ?u.395731
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.395740
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_2
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
⊢ (∃ x, x ∈ H ∧ ↑f x = n) ↔ ∃ x_1, x_1 ∈ H ∧ ↑f x_1 = ↑f x * n * (↑f x)⁻¹
G : Type u_1
G' : Type ?u.395731
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.395740
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_2
inst✝ : Group N
f : G →* N
x✝ : N
⊢ ∀ (x : G),
    (∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H) →
      ↑f x = x✝ → ∀ (h : N), (∃ x, x ∈ H ∧ ↑f x = h) ↔ ∃ x, x ∈ H ∧ ↑f x = x✝ * h * x✝⁻¹
rintro x hx rfl n
case mp
G : Type u_1
G' : Type ?u.395731
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.395740
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_2
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
⊢ (∃ x, x ∈ H ∧ ↑f x = n) → ∃ x_1, x_1 ∈ H ∧ ↑f x_1 = ↑f x * n * (↑f x)⁻¹

case mpr
G : Type u_1
G' : Type ?u.395731
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.395740
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_2
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
⊢ (∃ x_1, x_1 ∈ H ∧ ↑f x_1 = ↑f x * n * (↑f x)⁻¹) → ∃ x, x ∈ H ∧ ↑f x = n
G : Type u_1
G' : Type ?u.395731
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.395740
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_2
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
⊢ (∃ x, x ∈ H ∧ ↑f x = n) ↔ ∃ x_1, x_1 ∈ H ∧ ↑f x_1 = ↑f x * n * (↑f x)⁻¹
constructor
case mp.intro.intro
G : Type u_1
G' : Type ?u.395731
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.395740
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_2
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
y : G
hy : y ∈ H
⊢ ∃ x_1, x_1 ∈ H ∧ ↑f x_1 = ↑f x * ↑f y * (↑f x)⁻¹
case mp
G : Type u_1
G' : Type ?u.395731
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.395740
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_2
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
⊢ (∃ x, x ∈ H ∧ ↑f x = n) → ∃ x_1, x_1 ∈ H ∧ ↑f x_1 = ↑f x * n * (↑f x)⁻¹
rintro ⟨y, hy, rfl⟩
case mp.intro.intro
G : Type u_1
G' : Type ?u.395731
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.395740
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_2
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
y : G
hy : y ∈ H
⊢ ↑f (x * y * x⁻¹) = ↑f x * ↑f y * (↑f x)⁻¹
case mp.intro.intro
G : Type u_1
G' : Type ?u.395731
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.395740
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_2
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
y : G
hy : y ∈ H
⊢ ∃ x_1, x_1 ∈ H ∧ ↑f x_1 = ↑f x * ↑f y * (↑f x)⁻¹
use x * y * x⁻¹, (hx y).1 hy
no goals
case mp.intro.intro
G : Type u_1
G' : Type ?u.395731
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.395740
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_2
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
y : G
hy : y ∈ H
⊢ ↑f (x * y * x⁻¹) = ↑f x * ↑f y * (↑f x)⁻¹
simp
case mpr.intro.intro
G : Type u_1
G' : Type ?u.395731
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.395740
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_2
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
y : G
hyH : y ∈ H
hy : ↑f y = ↑f x * n * (↑f x)⁻¹
⊢ ∃ x, x ∈ H ∧ ↑f x = n
case mpr
G : Type u_1
G' : Type ?u.395731
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.395740
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_2
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
⊢ (∃ x_1, x_1 ∈ H ∧ ↑f x_1 = ↑f x * n * (↑f x)⁻¹) → ∃ x, x ∈ H ∧ ↑f x = n
rintro ⟨y, hyH, hy⟩
case mpr.intro.intro
G : Type u_1
G' : Type ?u.395731
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.395740
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_2
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
y : G
hyH : y ∈ H
hy : ↑f y = ↑f x * n * (↑f x)⁻¹
⊢ x⁻¹ * y * x ∈ H ∧ ↑f (x⁻¹ * y * x) = n
case mpr.intro.intro
G : Type u_1
G' : Type ?u.395731
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.395740
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_2
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
y : G
hyH : y ∈ H
hy : ↑f y = ↑f x * n * (↑f x)⁻¹
⊢ ∃ x, x ∈ H ∧ ↑f x = n
use x⁻¹ * y * x
case mpr.intro.intro
G : Type u_1
G' : Type ?u.395731
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.395740
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_2
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
y : G
hyH : y ∈ H
hy : ↑f y = ↑f x * n * (↑f x)⁻¹
⊢ x * (x⁻¹ * y * x) * x⁻¹ ∈ H ∧ ↑f (x⁻¹ * y * x) = n
case mpr.intro.intro
G : Type u_1
G' : Type ?u.395731
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.395740
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_2
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
y : G
hyH : y ∈ H
hy : ↑f y = ↑f x * n * (↑f x)⁻¹
⊢ x⁻¹ * y * x ∈ H ∧ ↑f (x⁻¹ * y * x) = n
rw [hx]
no goals
case mpr.intro.intro
G : Type u_1
G' : Type ?u.395731
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.395740
inst✝¹ : AddGroup A
H K : Subgroup G
N : Type u_2
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
y : G
hyH : y ∈ H
hy : ↑f y = ↑f x * n * (↑f x)⁻¹
⊢ x * (x⁻¹ * y * x) * x⁻¹ ∈ H ∧ ↑f (x⁻¹ * y * x) = n
simp [hy, hyH, mul_assoc]