p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p { x // x ∈ N }
g : G
x✝ : g ∈ ⊤
⊢ g ∈ normalizer (map (Subgroup.subtype N) ↑P) ⊔ N
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p { x // x ∈ N }
⊢ normalizer (map (Subgroup.subtype N) ↑P) ⊔ N = ⊤
refine' top_le_iff.mp fun g _ => _
case intro
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p { x // x ∈ N }
g : G
x✝ : g ∈ ⊤
n : { x // x ∈ N }
hn : n • ↑MulAut.conjNormal g • P = P
⊢ g ∈ normalizer (map (Subgroup.subtype N) ↑P) ⊔ N
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p { x // x ∈ N }
g : G
x✝ : g ∈ ⊤
⊢ g ∈ normalizer (map (Subgroup.subtype N) ↑P) ⊔ N
obtain ⟨n, hn⟩ := exists_smul_eq N ((MulAut.conjNormal g : MulAut N) • P) P
case intro
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p { x // x ∈ N }
g : G
x✝ : g ∈ ⊤
n : { x // x ∈ N }
hn : n • ↑MulAut.conjNormal g • P = P
⊢ (↑n)⁻¹ * (↑n * g) ∈ N ⊔ normalizer (map (Subgroup.subtype N) ↑P)
case intro
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p { x // x ∈ N }
g : G
x✝ : g ∈ ⊤
n : { x // x ∈ N }
hn : n • ↑MulAut.conjNormal g • P = P
⊢ g ∈ normalizer (map (Subgroup.subtype N) ↑P) ⊔ N
rw [← inv_mul_cancel_left (↑n) g, sup_comm]
case intro
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p { x // x ∈ N }
g : G
x✝ : g ∈ ⊤
n : { x // x ∈ N }
hn : n • ↑MulAut.conjNormal g • P = P
⊢ ↑n * g ∈ normalizer (map (Subgroup.subtype N) ↑P)
case intro
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p { x // x ∈ N }
g : G
x✝ : g ∈ ⊤
n : { x // x ∈ N }
hn : n • ↑MulAut.conjNormal g • P = P
⊢ (↑n)⁻¹ * (↑n * g) ∈ N ⊔ normalizer (map (Subgroup.subtype N) ↑P)
apply mul_mem_sup (N.inv_mem n.2)
case intro
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p { x // x ∈ N }
g : G
x✝ : g ∈ ⊤
n : { x // x ∈ N }
hn✝ : (↑MulAut.conj n * ↑MulAut.conjNormal g) • P = P
hn :
  map
      (↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut { x // x ∈ N }) n) { x // x ∈ N })
        (↑MulAut.conjNormal (↑n * g)))
      ↑P =
    ↑P
⊢ ↑n * g ∈ normalizer (map (Subgroup.subtype N) ↑P)
case intro
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p { x // x ∈ N }
g : G
x✝ : g ∈ ⊤
n : { x // x ∈ N }
hn : n • ↑MulAut.conjNormal g • P = P
⊢ ↑n * g ∈ normalizer (map (Subgroup.subtype N) ↑P)
rw [Sylow.smul_def, ← mul_smul, ← MulAut.conjNormal_val, ← MulAut.conjNormal.map_mul,
  Sylow.ext_iff, Sylow.pointwise_smul_def, Subgroup.pointwise_smul_def] at hn
case intro
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p { x // x ∈ N }
g : G
x✝ : g ∈ ⊤
n : { x // x ∈ N }
hn✝ : (↑MulAut.conj n * ↑MulAut.conjNormal g) • P = P
hn :
  map
      (↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut { x // x ∈ N }) n) { x // x ∈ N })
        (↑MulAut.conjNormal (↑n * g)))
      ↑P =
    ↑P
x : G
⊢ ↑(MulEquiv.toMonoidHom (↑MulAut.conj (↑n * g))) x ∈
      map (MulEquiv.toMonoidHom (↑MulAut.conj (↑n * g))) (map (Subgroup.subtype N) ↑P) ↔
    ↑n * g * x * (↑n * g)⁻¹ ∈ map (Subgroup.subtype N) ↑P
case intro
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p { x // x ∈ N }
g : G
x✝ : g ∈ ⊤
n : { x // x ∈ N }
hn✝ : (↑MulAut.conj n * ↑MulAut.conjNormal g) • P = P
hn :
  map
      (↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut { x // x ∈ N }) n) { x // x ∈ N })
        (↑MulAut.conjNormal (↑n * g)))
      ↑P =
    ↑P
⊢ ↑n * g ∈ normalizer (map (Subgroup.subtype N) ↑P)
refine' fun x =>
  (mem_map_iff_mem
          (show Function.Injective (MulAut.conj (↑n * g)).toMonoidHom from
            (MulAut.conj (↑n * g)).injective)).symm.trans
    _
case intro
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p { x // x ∈ N }
g : G
x✝ : g ∈ ⊤
n : { x // x ∈ N }
hn✝ : (↑MulAut.conj n * ↑MulAut.conjNormal g) • P = P
hn :
  map
      (↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut { x // x ∈ N }) n) { x // x ∈ N })
        (↑MulAut.conjNormal (↑n * g)))
      ↑P =
    ↑P
x : G
⊢ ↑(MulEquiv.toMonoidHom (↑MulAut.conj (↑n * g))) x ∈
      map (MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑n * g))) (Subgroup.subtype N)) ↑P ↔
    ↑n * g * x * (↑n * g)⁻¹ ∈
      map
        (MonoidHom.comp (Subgroup.subtype N)
          (↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut { x // x ∈ N }) n) { x // x ∈ N })
            (↑MulAut.conjNormal (↑n * g))))
        ↑P
case intro
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p { x // x ∈ N }
g : G
x✝ : g ∈ ⊤
n : { x // x ∈ N }
hn✝ : (↑MulAut.conj n * ↑MulAut.conjNormal g) • P = P
hn :
  map
      (↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut { x // x ∈ N }) n) { x // x ∈ N })
        (↑MulAut.conjNormal (↑n * g)))
      ↑P =
    ↑P
x : G
⊢ ↑(MulEquiv.toMonoidHom (↑MulAut.conj (↑n * g))) x ∈
      map (MulEquiv.toMonoidHom (↑MulAut.conj (↑n * g))) (map (Subgroup.subtype N) ↑P) ↔
    ↑n * g * x * (↑n * g)⁻¹ ∈ map (Subgroup.subtype N) ↑P
rw [map_map, ← congr_arg (map N.subtype) hn, map_map]
no goals
case intro
p✝ : ℕ
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : Normal N
inst✝ : Finite (Sylow p { x // x ∈ N })
P : Sylow p { x // x ∈ N }
g : G
x✝ : g ∈ ⊤
n : { x // x ∈ N }
hn✝ : (↑MulAut.conj n * ↑MulAut.conjNormal g) • P = P
hn :
  map
      (↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut { x // x ∈ N }) n) { x // x ∈ N })
        (↑MulAut.conjNormal (↑n * g)))
      ↑P =
    ↑P
x : G
⊢ ↑(MulEquiv.toMonoidHom (↑MulAut.conj (↑n * g))) x ∈
      map (MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑n * g))) (Subgroup.subtype N)) ↑P ↔
    ↑n * g * x * (↑n * g)⁻¹ ∈
      map
        (MonoidHom.comp (Subgroup.subtype N)
          (↑(MulDistribMulAction.toMonoidEnd ((fun x => MulAut { x // x ∈ N }) n) { x // x ∈ N })
            (↑MulAut.conjNormal (↑n * g))))
        ↑P
rfl