-- Mathlib/GroupTheory/Transfer.lean
theorem normalizer_le_centralizer (hP : IsCyclic P) : P.normalizer ≤ centralizer (P : Set G)

Proof state:
case neg
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : Nat.card (↥(↑P).normalizer ⧸ (↑P).normalizerMonoidHom.ker) ∣ Nat.card (MulAut ↥↑P)
⊢ (↑P).normalizer ≤ centralizer ↑P

Tactic:
rw [normalizerMonoidHom_ker, ← index, ← relindex] at key

Result:
case neg
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relindex (↑P).normalizer ∣ Nat.card (MulAut ↥↑P)
⊢ (↑P).normalizer ≤ centralizer ↑P

Proof state:
case neg.intro.inr.refine_2
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relindex (↑P).normalizer ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ (Nat.card ↥(↑P).normalizer).Coprime ((Nat.card G).minFac - 1)

Tactic:
apply Nat.Coprime.coprime_dvd_left (card_subgroup_dvd_card P.normalizer)

Result:
case neg.intro.inr.refine_2
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relindex (↑P).normalizer ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ (Nat.card G).Coprime ((Nat.card G).minFac - 1)

Proof state:
case pos
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : Nat.card G = 1
⊢ (↑P).normalizer ≤ centralizer ↑P

Tactic:
have := (Nat.card_eq_one_iff_unique.mp hn).1

Result:
case pos
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : Nat.card G = 1
this : Subsingleton G
⊢ (↑P).normalizer ≤ centralizer ↑P

Proof state:
case neg.intro.inr.refine_2
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relindex (↑P).normalizer ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
h1 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ∣ Nat.card G
h2 : ¬(Nat.card G).Coprime ((Nat.card G).minFac - 1)
⊢ 2 ≤ (Nat.card G).gcd ((Nat.card G).minFac - 1)

Tactic:
exact (Nat.two_le_iff _).mpr ⟨ne_zero_of_dvd_ne_zero Nat.card_pos.ne' h1, h2⟩

Result:
no goals

Proof state:
case neg.intro.inr.refine_2
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relindex (↑P).normalizer ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
h1 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ∣ Nat.card G
⊢ (Nat.card G).Coprime ((Nat.card G).minFac - 1)

Tactic:
have h2 := Nat.gcd_le_right (m := Nat.card G) ((Nat.card G).minFac - 1)
  (tsub_pos_iff_lt.mpr (Nat.minFac_prime hn).one_lt)

Result:
case neg.intro.inr.refine_2
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relindex (↑P).normalizer ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
h1 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ∣ Nat.card G
h2 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ≤ (Nat.card G).minFac - 1
⊢ (Nat.card G).Coprime ((Nat.card G).minFac - 1)

Proof state:
case neg.intro.inr
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relindex (↑P).normalizer ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ ((centralizer ↑P).relindex (↑P).normalizer).Coprime ((Nat.card G).minFac ^ (k - 1) * ((Nat.card G).minFac - 1))

Tactic:
refine (Nat.Coprime.pow_right _ ?_).mul_right ?_

Result:
case neg.intro.inr.refine_1
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relindex (↑P).normalizer ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ ((centralizer ↑P).relindex (↑P).normalizer).Coprime (Nat.card G).minFac

case neg.intro.inr.refine_2
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relindex (↑P).normalizer ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ ((centralizer ↑P).relindex (↑P).normalizer).Coprime ((Nat.card G).minFac - 1)

Proof state:
case neg.intro.inr.refine_2
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relindex (↑P).normalizer ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
h1 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ∣ Nat.card G
h2 : ¬(Nat.card G).Coprime ((Nat.card G).minFac - 1)
⊢ (Nat.card G).minFac - 1 < (Nat.card G).gcd ((Nat.card G).minFac - 1)

Tactic:
refine Nat.sub_one_lt_of_le (Nat.card G).minFac_pos (Nat.minFac_le_of_dvd ?_ h1)

Result:
case neg.intro.inr.refine_2
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relindex (↑P).normalizer ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
h1 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ∣ Nat.card G
h2 : ¬(Nat.card G).Coprime ((Nat.card G).minFac - 1)
⊢ 2 ≤ (Nat.card G).gcd ((Nat.card G).minFac - 1)

Proof state:
case neg.intro.inr
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relindex (↑P).normalizer ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ ((centralizer ↑P).relindex (↑P).normalizer).Coprime (Nat.card (MulAut ↥↑P))

Tactic:
rw [hP.card_mulAut, hk, Nat.totient_prime_pow Fact.out h0]

Result:
case neg.intro.inr
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relindex (↑P).normalizer ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ ((centralizer ↑P).relindex (↑P).normalizer).Coprime ((Nat.card G).minFac ^ (k - 1) * ((Nat.card G).minFac - 1))

Proof state:
case neg.intro.inr.refine_1
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relindex (↑P).normalizer ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ ¬(Nat.card G).minFac ∣ (↑P).index

Tactic:
exact P.not_dvd_index

Result:
no goals