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

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

Tactic:
by_cases hn : Nat.card G = 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
⊢ (↑P).normalizer ≤ centralizer ↑P

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
⊢ (↑P).normalizer ≤ centralizer ↑P

Proof state:
case neg.intro.inl
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 : k = 0
⊢ ((centralizer ↑P).relindex (↑P).normalizer).Coprime 1

Tactic:
apply Nat.coprime_one_right

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
h2 : (Nat.card G).gcd ((Nat.card G).minFac - 1) ≤ (Nat.card G).minFac - 1
⊢ (Nat.card G).Coprime ((Nat.card G).minFac - 1)

Tactic:
contrapose! h2

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)
⊢ (Nat.card G).minFac - 1 < (Nat.card G).gcd ((Nat.card G).minFac - 1)

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)
⊢ (↑P).normalizer ≤ centralizer ↑P

Tactic:
have key := card_dvd_of_injective _ (QuotientGroup.kerLift_injective P.normalizerMonoidHom)

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 : Nat.card (↥(↑P).normalizer ⧸ (↑P).normalizerMonoidHom.ker) ∣ Nat.card (MulAut ↥↑P)
⊢ (↑P).normalizer ≤ centralizer ↑P

Proof state:
case neg.intro
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
⊢ ((centralizer ↑P).relindex (↑P).normalizer).Coprime (Nat.card (MulAut ↥↑P))

Tactic:
rcases eq_zero_or_pos k with h0 | h0

Result:
case neg.intro.inl
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 : k = 0
⊢ ((centralizer ↑P).relindex (↑P).normalizer).Coprime (Nat.card (MulAut ↥↑P))

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))

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 : (centralizer ↑↑P).relindex (↑P).normalizer ∣ Nat.card (MulAut ↥↑P)
⊢ ((centralizer ↑P).relindex (↑P).normalizer).Coprime (Nat.card (MulAut ↥↑P))

Tactic:
obtain ⟨k, hk⟩ := P.2.exists_card_eq

Result:
case neg.intro
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
⊢ ((centralizer ↑P).relindex (↑P).normalizer).Coprime (Nat.card (MulAut ↥↑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 G).Coprime ((Nat.card G).minFac - 1)

Tactic:
have h1 := Nat.gcd_dvd_left (Nat.card G) ((Nat.card G).minFac - 1)

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
⊢ (Nat.card G).Coprime ((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
⊢ ((centralizer ↑P).relindex (↑P).normalizer).Coprime (Nat.card G).minFac

Tactic:
apply Nat.Coprime.coprime_dvd_left (relindex_dvd_of_le_left P.normalizer P.le_centralizer)

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
⊢ ((↑P).relindex (↑P).normalizer).Coprime (Nat.card G).minFac

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

Tactic:
subst hp

Result:
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑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
⊢ ((centralizer ↑P).relindex (↑P).normalizer).Coprime ((Nat.card G).minFac - 1)

Tactic:
apply Nat.Coprime.coprime_dvd_left (relindex_dvd_card (centralizer P) 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 ↥(↑P).normalizer).Coprime ((Nat.card G).minFac - 1)