G : Type u_1
inst✝² : Group G
A : Type ?u.42200
inst✝¹ : AddGroup A
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ (n : G), n ∈ S → x * n * x⁻¹ ∈ S
this : (a : Prop) → Decidable a
⊢ x ∈ setNormalizer S
G : Type u_1
inst✝² : Group G
A : Type ?u.42200
inst✝¹ : AddGroup A
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ (n : G), n ∈ S → x * n * x⁻¹ ∈ S
⊢ x ∈ setNormalizer S
haveI := Classical.propDecidable
case intro
G : Type u_1
inst✝² : Group G
A : Type ?u.42200
inst✝¹ : AddGroup A
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ (n : G), n ∈ S → x * n * x⁻¹ ∈ S
this : (a : Prop) → Decidable a
val✝ : Fintype ↑S
⊢ x ∈ setNormalizer S
G : Type u_1
inst✝² : Group G
A : Type ?u.42200
inst✝¹ : AddGroup A
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ (n : G), n ∈ S → x * n * x⁻¹ ∈ S
this : (a : Prop) → Decidable a
⊢ x ∈ setNormalizer S
cases nonempty_fintype S
case intro
G : Type u_1
inst✝² : Group G
A : Type ?u.42200
inst✝¹ : AddGroup A
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ (n : G), n ∈ S → x * n * x⁻¹ ∈ S
this✝ : (a : Prop) → Decidable a
val✝ : Fintype ↑S
this : Fintype ↑((fun n => x * n * x⁻¹) '' S)
⊢ x ∈ setNormalizer S
case intro
G : Type u_1
inst✝² : Group G
A : Type ?u.42200
inst✝¹ : AddGroup A
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ (n : G), n ∈ S → x * n * x⁻¹ ∈ S
this : (a : Prop) → Decidable a
val✝ : Fintype ↑S
⊢ x ∈ setNormalizer S
haveI := Set.fintypeImage S fun n => x * n * x⁻¹
no goals
case intro
G : Type u_1
inst✝² : Group G
A : Type ?u.42200
inst✝¹ : AddGroup A
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ (n : G), n ∈ S → x * n * x⁻¹ ∈ S
this✝ : (a : Prop) → Decidable a
val✝ : Fintype ↑S
this : Fintype ↑((fun n => x * n * x⁻¹) '' S)
⊢ x ∈ setNormalizer S
exact fun n =>
  ⟨h n, fun h₁ =>
    have heq : (fun n => x * n * x⁻¹) '' S = S :=
      Set.eq_of_subset_of_card_le (fun n ⟨y, hy⟩ => hy.2 ▸ h y hy.1)
        (by rw [Set.card_image_of_injective S conj_injective])
    have : x * n * x⁻¹ ∈ (fun n => x * n * x⁻¹) '' S := heq.symm ▸ h₁
    let ⟨y, hy⟩ := this
    conj_injective hy.2 ▸ hy.1⟩
no goals
G : Type u_1
inst✝² : Group G
A : Type ?u.42200
inst✝¹ : AddGroup A
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ (n : G), n ∈ S → x * n * x⁻¹ ∈ S
this✝ : (a : Prop) → Decidable a
val✝ : Fintype ↑S
this : Fintype ↑((fun n => x * n * x⁻¹) '' S)
n : G
h₁ : x * n * x⁻¹ ∈ S
⊢ Fintype.card ↑S ≤ Fintype.card ↑((fun n => x * n * x⁻¹) '' S)
rw [Set.card_image_of_injective S conj_injective]