-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem le_normalizer_map (f : G →* N) : H.normalizer.map f ≤ (H.map f).normalizer := fun _ => by
  simp only [and_imp, exists_prop, mem_map, exists_imp, mem_normalizer_iff]
  rintro x hx rfl n
  constructor
  · rintro ⟨y, hy, rfl⟩
    use x * y * x⁻¹, (hx y).1 hy
    simp
  · rintro ⟨y, hyH, hy⟩
    use x⁻¹ * y * x
    rw [hx]
    simp [hy, hyH, mul_assoc]

Proof state:
case mpr.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
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 ∈ H, f x = n

Tactic:
use x⁻¹ * y * x

Result:
case h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
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

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
x✝ : N
⊢ x✝ ∈ map f H.normalizer → x✝ ∈ (map f H).normalizer

Tactic:
simp only [and_imp, exists_prop, mem_map, exists_imp, mem_normalizer_iff]

Result:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
x✝ : N
⊢ ∀ (x : G),
    (∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H) → f x = x✝ → ∀ (h : N), (∃ x ∈ H, f x = h) ↔ ∃ x ∈ H, f x = x✝ * h * x✝⁻¹

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
⊢ (∃ x ∈ H, f x = n) ↔ ∃ x_1 ∈ H, f x_1 = f x * n * (f x)⁻¹

Tactic:
constructor

Result:
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
⊢ (∃ x ∈ H, f x = n) → ∃ x_1 ∈ H, f x_1 = f x * n * (f x)⁻¹

case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
⊢ (∃ x_1 ∈ H, f x_1 = f x * n * (f x)⁻¹) → ∃ x ∈ H, f x = n

Proof state:
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
⊢ (∃ x_1 ∈ H, f x_1 = f x * n * (f x)⁻¹) → ∃ x ∈ H, f x = n

Tactic:
rintro ⟨y, hyH, hy⟩

Result:
case mpr.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
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 ∈ H, f x = n

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
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

Tactic:
simp [hy, hyH, mul_assoc]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
x✝ : N
⊢ ∀ (x : G),
    (∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H) → f x = x✝ → ∀ (h : N), (∃ x ∈ H, f x = h) ↔ ∃ x ∈ H, f x = x✝ * h * x✝⁻¹

Tactic:
rintro x hx rfl n

Result:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
⊢ (∃ x ∈ H, f x = n) ↔ ∃ x_1 ∈ H, f x_1 = f x * n * (f x)⁻¹

Proof state:
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
n : N
⊢ (∃ x ∈ H, f x = n) → ∃ x_1 ∈ H, f x_1 = f x * n * (f x)⁻¹

Tactic:
rintro ⟨y, hy, rfl⟩

Result:
case mp.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
y : G
hy : y ∈ H
⊢ ∃ x_1 ∈ H, f x_1 = f x * f y * (f x)⁻¹

Proof state:
case right
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
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)⁻¹

Tactic:
simp

Result:
no goals

Proof state:
case mp.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
x : G
hx : ∀ (h : G), h ∈ H ↔ x * h * x⁻¹ ∈ H
y : G
hy : y ∈ H
⊢ ∃ x_1 ∈ H, f x_1 = f x * f y * (f x)⁻¹

Tactic:
use x * y * x⁻¹, (hx y).1 hy

Result:
case right
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
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)⁻¹

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
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

Tactic:
rw [hx]

Result:
case h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
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