-- Mathlib/GroupTheory/IndexNormal.lean
theorem normal_of_index_eq_minFac_card (hHp : H.index = (Nat.card G).minFac) :
    H.Normal

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : H.normalCore.relindex H = 1
⊢ H.Normal

Tactic:
convert H.normalCore_normal

Result:
case h.e'_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : H.normalCore.relindex H = 1
⊢ H = H.normalCore

Proof state:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
⊢ H.normalCore.index = H.index

Tactic:
apply dvd_antisymm _ (index_dvd_of_le H.normalCore_le)

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
⊢ H.normalCore.index ∣ H.index

Proof state:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
⊢ H.normalCore.relindex H = 1

Tactic:
rw [← mul_left_inj' index_ne_zero, one_mul, relindex_mul_index H.normalCore_le]

Result:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
⊢ H.normalCore.index = H.index

Proof state:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
⊢ H.normalCore.relindex H = 1

Tactic:
have : Finite G := finite_of_card_ne_zero hG0

Result:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
⊢ H.normalCore.relindex H = 1

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
hr1 : H.normalCore.index ≠ 1
⊢ H.index - 1 < H.normalCore.index.minFac

Tactic:
exact lt_of_lt_of_le (Nat.sub_one_lt hp.ne_zero) <|
  hHp ▸ minFac_le_of_dvd (Nat.minFac_prime hr1).two_le
    (dvd_trans (minFac_dvd H.normalCore.index) (H.normalCore.index_dvd_card))

Result:
no goals

Proof state:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
⊢ H.Normal

Tactic:
suffices H.normalCore.relindex H = 1 by
  convert H.normalCore_normal
  exact le_antisymm (relindex_eq_one.mp this) (normalCore_le H)

Result:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
⊢ H.normalCore.relindex H = 1

Proof state:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
⊢ H.normalCore.relindex H = 1

Tactic:
have index_ne_zero : H.index ≠ 0 := index_ne_zero_of_finite

Result:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
⊢ H.normalCore.relindex H = 1

Proof state:
case h.e'_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : H.normalCore.relindex H = 1
⊢ H = H.normalCore

Tactic:
exact le_antisymm (relindex_eq_one.mp this) (normalCore_le H)

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
⊢ Nat.card ↥(toPermHom G (G ⧸ H)).range ∣ Nat.card (Equiv.Perm (G ⧸ H))

Tactic:
exact card_subgroup_dvd_card (toPermHom G (G ⧸ H)).range

Result:
no goals

Proof state:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = 2
hG0 : Nat.card G = 0
⊢ H.Normal

Tactic:
exact normal_of_index_eq_two hHp

Result:
no goals

Proof state:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
⊢ H.Normal

Tactic:
by_cases hG1 : Nat.card G = 1

Result:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : Nat.card G = 1
⊢ H.Normal

case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
⊢ H.Normal

Proof state:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : Nat.card G = 0
⊢ H.Normal

Tactic:
rw [hG0, minFac_zero] at hHp

Result:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = 2
hG0 : Nat.card G = 0
⊢ H.Normal

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
⊢ H.Normal

Tactic:
by_cases hG0 : Nat.card G = 0

Result:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : Nat.card G = 0
⊢ H.Normal

case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
⊢ H.Normal

Proof state:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : Nat.card G = 1
⊢ H.Normal

Tactic:
rw [hG1, minFac_one] at hHp

Result:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = 1
hG0 : ¬Nat.card G = 0
hG1 : Nat.card G = 1
⊢ H.Normal

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
⊢ H.normalCore.index ∣ H.index

Tactic:
rwa [← Coprime.dvd_mul_right, mul_factorial_pred hp.pos]

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
⊢ H.normalCore.index.Coprime (H.index - 1)!

Proof state:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
⊢ H.normalCore.index = H.index

Tactic:
have hp : Nat.Prime H.index := hHp ▸ minFac_prime hG1

Result:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
⊢ H.normalCore.index = H.index

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
⊢ H.normalCore.index.Coprime (H.index - 1)!

Tactic:
have hr1 : H.normalCore.index ≠ 1 := fun hr1 ↦ hp.ne_one <|
  Nat.eq_one_of_dvd_one (hr1 ▸ H.normalCore.index_dvd_of_le H.normalCore_le)

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : ¬Nat.card G = 1
this : Finite G
index_ne_zero : H.index ≠ 0
hp : Nat.Prime H.index
h : H.normalCore.index ∣ H.index !
hr1 : H.normalCore.index ≠ 1
⊢ H.normalCore.index.Coprime (H.index - 1)!