-- Mathlib/GroupTheory/Nilpotent.lean
theorem isNilpotent_of_product_of_sylow_group
    (e : (∀ p : (Nat.card G).primeFactors, ∀ P : Sylow p G, (↑P : Subgroup G)) ≃* G) :
    IsNilpotent G

Proof state:
G : Type u_1
hG : Group G
inst✝ : Finite G
e : ((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G
ps : Finset ℕ := (Nat.card G).primeFactors
this : ∀ (p : { x // x ∈ ps }) (P : Sylow (↑p) G), IsNilpotent ↥↑P
⊢ IsNilpotent G

Tactic:
exact nilpotent_of_mulEquiv e

Result:
no goals

Proof state:
G : Type u_1
hG : Group G
inst✝ : Finite G
e : ((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G
ps : Finset ℕ := (Nat.card G).primeFactors
p : { x // x ∈ ps }
P : Sylow (↑p) G
⊢ IsNilpotent ↥↑P

Tactic:
haveI : Fact (Nat.Prime ↑p) := Fact.mk <| Nat.prime_of_mem_primeFactors p.2

Result:
G : Type u_1
hG : Group G
inst✝ : Finite G
e : ((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G
ps : Finset ℕ := (Nat.card G).primeFactors
p : { x // x ∈ ps }
P : Sylow (↑p) G
this : Fact (Nat.Prime ↑p)
⊢ IsNilpotent ↥↑P

Proof state:
G : Type u_1
hG : Group G
inst✝ : Finite G
e : ((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G
ps : Finset ℕ := (Nat.card G).primeFactors
p : { x // x ∈ ps }
P : Sylow (↑p) G
this : Fact (Nat.Prime ↑p)
⊢ IsNilpotent ↥↑P

Tactic:
exact P.isPGroup'.isNilpotent

Result:
no goals

Proof state:
G : Type u_1
hG : Group G
inst✝ : Finite G
e : ((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G
⊢ IsNilpotent G

Tactic:
let ps := (Nat.card G).primeFactors

Result:
G : Type u_1
hG : Group G
inst✝ : Finite G
e : ((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G
ps : Finset ℕ := (Nat.card G).primeFactors
⊢ IsNilpotent G

Proof state:
G : Type u_1
hG : Group G
inst✝ : Finite G
e : ((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G
ps : Finset ℕ := (Nat.card G).primeFactors
⊢ IsNilpotent G

Tactic:
have : ∀ (p : ps) (P : Sylow p G), IsNilpotent (↑P : Subgroup G) := by
  intro p P
  haveI : Fact (Nat.Prime ↑p) := Fact.mk <| Nat.prime_of_mem_primeFactors p.2
  exact P.isPGroup'.isNilpotent

Result:
G : Type u_1
hG : Group G
inst✝ : Finite G
e : ((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G
ps : Finset ℕ := (Nat.card G).primeFactors
this : ∀ (p : { x // x ∈ ps }) (P : Sylow (↑p) G), IsNilpotent ↥↑P
⊢ IsNilpotent G

Proof state:
G : Type u_1
hG : Group G
inst✝ : Finite G
e : ((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G
ps : Finset ℕ := (Nat.card G).primeFactors
⊢ ∀ (p : { x // x ∈ ps }) (P : Sylow (↑p) G), IsNilpotent ↥↑P

Tactic:
intro p P

Result:
G : Type u_1
hG : Group G
inst✝ : Finite G
e : ((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G
ps : Finset ℕ := (Nat.card G).primeFactors
p : { x // x ∈ ps }
P : Sylow (↑p) G
⊢ IsNilpotent ↥↑P

Proof state:
G : Type u_1
hG : Group G
inst✝ : Finite G
e : ((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G
⊢ IsNilpotent G

Tactic:
classical
  let ps := (Nat.card G).primeFactors
  have : ∀ (p : ps) (P : Sylow p G), IsNilpotent (↑P : Subgroup G) := by
    intro p P
    haveI : Fact (Nat.Prime ↑p) := Fact.mk <| Nat.prime_of_mem_primeFactors p.2
    exact P.isPGroup'.isNilpotent
  exact nilpotent_of_mulEquiv e

Result:
no goals